The Coq mailing list

[Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz>]

Thank you for the feedback. Now, it looks like I have figured out what happened and have made quick fix.

Kind regards,

Rustam

On Wed, Nov 22, 2017 at 2:15 PM, Merlin Göttlinger <megoettlinger AT gmail.com> wrote:

It seems I crashed the bot or something when entering my theorem... It replied to the initial "/help" and "/start" but then stopped responding.

Cheers,

Merlin

Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz> schrieb am Mi., 22. Nov. 2017 um 09:05 Uhr:

It was quick hot bug fixing. Could, please, try it now?

Kind regards,

Rustam

On Wed, Nov 22, 2017 at 1:51 PM, Merlin Göttlinger <megoettlinger AT gmail.com> wrote:

Hi Rustam,

is the bot currently offline? Because it doesn't seem to respond to anything at the moment.

Cheers,

Merlin

Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz> schrieb am Mi., 22. Nov. 2017 um 06:33 Uhr:

Dear all,

I want to present a new solution for running Coq on Android devices - Coq Telegram bot. 

It allows you to continue working on proofs even on the go. 

Link to the bot: http://t.me/CoqProofbot

This is part of an undergraduate research project.

The only data we collect - number of unique users.

After using the bot, we kindly ask you to take the survey to gather feedback and identify the need of such bot for the community. As this is public beta we want to attract attention from the community, gathering your feedback on what features bot should possess. Currently we also have single user bot that can be run from any machine that have Coq and Java in it. 

Link to the survey: https://goo.gl/forms/E3cEDvnM7KFYB4AP2

Here is an example of proving a simple theorem:

It also supports loading of external files, just drop them into the bot (.v files).

Screenshot: https://image.ibb.co/kuVecm/chat_screenshot.png

Kind regards,

Rustam Zhumagambetov