coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq on Android as Telegram Chatbot - First release

From: Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq on Android as Telegram Chatbot - First release
Date: Fri, 16 Mar 2018 16:34:23 +0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rustam.zhumagambetov AT nu.edu.kz; spf=Pass smtp.mailfrom=rustam.zhumagambetov AT nu.edu.kz; spf=None smtp.helo=postmaster AT mail-io0-f194.google.com
Ironport-phdr: 9a23:hyHg/xOGvlqx4IwWcM4l6mtUPXoX/o7sNwtQ0KIMzox0IvrzrarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr8zRDqi8rxrSAf2hygbKz43/mbXislqg6JaphKquhhzzoHQbY2QMvd1Y6HTcs4ARWdZXshfWS9PDJ6iYYQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33fg8EQHdwAwvBdcOu2nXo9X1KacSVPq6zKbSwjXGdPxZxyv96I/Wchs8pvyMR69wcdHNyUY1EgPJlFSRqYz4PzOQzOsNvHKU7+97Wu2xl24nrB9xryOpxscxkIXGmJ8ayk3e+SV6wYc4PNu1Q1N1b96jFZtfrSCaN41uT8M+WW1ovTg1xqUJuZ66YCgKzI4oyAXFZ/ObdIiI5wrvVOmWITd/nn5ld7a/ihCv+kaj0u3xTte43EpOoyZfkdTBtmoB2wLN5sWJUPdx40Os1DmJ2gvO8O9LO1o0mrDeK5M5wr4/iJ4TsUPbEy/zgkr2jauWelwl+uiv9+jre7vmqoKYOoJ7kA3+PaMumsuwAeQ8LAcCRXSU+eO51LH7/E35RqtFjuEun6XHrJzXId4Xq625DgNPzIov9RiyAy273NkcknQLNFdFdwiGj4jtNVHOOvf4DfKnjlS2jTdr3OzGMafkApnXL3nDkKrhfbNn5E5T0gUzyMtQ6IxICrEGPvL+QUnxtMHCAhAnLgO03vzrCNZ8148GQ2KAHreZML/OsV+P/u8gP+6MZJYMtDnhL/gl+uXhgGQimV4deKmpxYEYZGq5HvRgOUWZYGDjjs0PEWcQ7UICS7nhj0THWjpObV6zWbg973c1EtGIF4DGE7qwm6CI2W+JHoBTb29PD1qBDXD2P9GeRuwQYSfUMM98lzULXL2rRpMmyzmoqUn3x6chLfiCqX5Qjo7qyNUgv76brho17zEhU5XEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPEqheEeGNBOofBbAF5jaczsitdiAtW3YTrvO8+TQQ//ENO7Rzw9U5Qy0Y1WOhsvK5CZlhnGmhGSLfoVmriMXsJm96vd2z3wIJ44xS+XiO8uiF4pRsYJPmqj1PZy

Dear all,

In the November, we have announced the beta version of the Coq Telegram bot, that is a part of an undergraduate research project. Currently we are glad to announce the first version of the bot, which supports following features:

Prove theorems, lemmas, etc
Query coqbot about previously defined entities
Load files (just drop them)

Changes compared to beta version:

State is now saved in the database, so previously defined proofs will not be lost
All errors are now reported back to the user
Added new tactic button - apply
Added button to enter custom tactic

Bot is written in Java, using Spring (dependency injection)

Two flavors of the bot are distributed - private and public (private - requires less dependencies and is locked for specific user, public - report metrics, such as total update count and number of online users to the database, uses mongo database to store state of the coq, can shutdown timed out instances to save memory)

Source code is available - GitLab (https://gitlab.com/rustamzh/telegramcoqbot)

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

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.

Link to the survey: https://goo.gl/forms/3kfmJiOJTcXkrkM93

Kind regards,

Rustam Zhumagambetov

[Coq-Club] Coq on Android as Telegram Chatbot - First release, Rustam Zhumagambetov, 03/16/2018