Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Announcing Tactician version 1.0 beta2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Announcing Tactician version 1.0 beta2


Chronological Thread 
  • From: Lasse Blaauwbroek <lasse AT blaauwbroek.eu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Announcing Tactician version 1.0 beta2
  • Date: Mon, 23 Oct 2023 05:50:30 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lasse AT blaauwbroek.eu; spf=Pass smtp.mailfrom=lasse AT blaauwbroek.eu; spf=None smtp.helo=postmaster AT mail.blaauwbroek.eu
  • Ironport-data: A9a23:i4pJxKIepbGrlb3EFE+RFZElxSXFcZb7ZxGr2PjKsXjdYENSgzYOn TAYWWCBbvmMYmKgfI8jYYvjoEIGuZfXxoMxTAod+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf+s9JIGjhMsfna8Ek15K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LueSDo7dhUNlEND7Ij499sO0N3z aw3AWVYBvyDr7reLLOTT+BtgoIpKMDiIZwVoHZtznfUEJ7KQ7iaE/iMv4Mehm1owJ8XdRrdT 5JxhT5HaB3beBBnMFMeAY8hlv2vi3q5fiAwRFe9+/trvzCLkFEZPL7FH4qJJISYbuhvxXnE/ j6FoGL/OylFK4nKodaC2in03bORzH2TtJgpPLa/77thhECZ7ncCDQUfE1q9u/iwzECkM++zM GQR8ysq66I2/UW2UdPnWBC75nOZ1vIBZzZOO+dh7C+g8JDE2DSmPXE9VQRjUeR2m+ZjEFTGy WS1t9/uADVutpicRnSc6qqYoFuOBMQFEYMRTXJeFltfv7EPtKlv3kOeEr6PBYbs1oWdJN3m/ 9ydhA4a74j/YOYO3qS/u1rDijuxuZLTSQM2oAjKNo5E0u+bTNX6D2BLwQKBhRqlEGp+ZgPZ1 EXoY+DEsIgz4WilzURggIwlRdlFHcqtPjzGmkJIFJI87Tmr8HPLVdkOsW4vdRY1aZlUKGKBj KrvVeV5uc470JyCMP4fXm5NI55CIVXITIm7D668giRmPMUsHON4wM2eTRXIhDyzwRZEfVAXJ ZafeM/kBzAET8xaIMmeGY8gPH5C7n5W+F4/sriglET2iOHCNCPIIVrHWXPXBt0EAGq/iF292 75i2wGikn2zicWvMnOFwp1ZNl0QM3kwCLb/rsEdJKbJIRNrFCtlQ7XdyK8oMd4t1alEtPb6z lfkUG9hyX37mSLmLyeOYStdc7/BZ8t0gk86Gi0OBmyW/UYfT7yh1ppCSKtvT4IbrLRi6dVWU 8g6f96xB6UTazbfpBUYQ5rPjK1jUxWJhAihESqpUDQ+dJsxQwXYp9voRSr01Sw0FiHsn9APk 76h8QL6QJQ4WAVpCvjNWs+v11+cuXs8mvp4ekn1fuloZ0Tn9bZ1JxzLjvMYJ98GLTPBzGC40 zm6LAg5p+6XhaMI6/jM2L65qrm2H9tEHkZ1G3fR6ZC0P3L4+kuh2Ypxb/aaTwvCVW/b+LSQW ssN9qvSaMY4pVdtt5ZwN51JzqhkvtvmmOJ8/zReRX7OawymN6NkLny4xvJwj6xqxIJCmA6IS 0mKq8h7O7KIBZvfK2QvBjEZN8aN6fJFvQPpz6URAF777ypJ7ra4QR1sHx2Tuhd8cppxEq0Ym NkEhuBHyjaCmiILM8mHhB96726jDGINeIR5u4A4AL3EsBsKyFZDa6PyEiXdvZCFRPtMPnkmI zSR1a7LlulYynHjaFs2L2DGhsBGtKQNuTdL7V4MHEuIkdz7nc0K3AVd3DA0bwZNxDBV+rtXF kkyEGMtPoSI3TNjpPYbblCWAwsbWSGooB3g+WUGhEjybheOVFWUCEYfJOzU3kQS01wETwhh5 LvClVrUC2f7TvrQgBk3d1Vu8cH4bNpL8QbHpsCrMuKFE7Q+YhvnmqWeXnUJmTS2HfIOgFD7m scy8NZScaHbMQsik58/AaSe1pUST0mgD05GSvdD4qgIPD/9fBef5DuwEH2yK/h9f6HyzUyFC sJVNp1uUTa6332wtTw1P/MHDIJ1u/8L3+A8XI3XC1QIiJallQoxgqnsrnD/oEQJX+RRld0ML 9KNVjCaTU2Vq3hmu07Mi8hmO2CXT9kIVAH91+Xk9OwYSpYPi8B3UEQIyrDvlW6kAAhm2BO1v Q34eK7dydJ5+7lsh4fBFqZiBR2+DNHOCNSz7wG4tupRYeP1Mcvhsx0frn/lNV90OYQ9dstWl 7PXlvLKx2LA4agLVl7Gl6m7F6Vm4du4WMxVOJnVKFhYhS6zZ9/+0SAc+myXKY17r/0F35OJH zCHUcqXccIZf/x/x3cPMihXLEs7OpTNN6zloXuwkuSIBh0jyjf4FdKA90LyTGRlZyQNaozfC Aj1hq6U3epmjr9wXT0KO/I3JKVDAg7TafNzPZm5/zyVFXKhjV6+q6Pv30hooy3CDn6fVt32+ 9TZTxz5bw6/o7zM0MofiYFpoxkLFzxotIHcpK7GFwJe0FhWzVLqLNjx9b0DA5BQ1Cb23Zjle zvXa2YhTyjgNdiBndMQ//y7NjpzxMRXUjs6GtDt10mQYi6rG4maB7ZisCp9i5uzUiW21/mpc Lny5VWpViVcAfhVqSI77PiyiPp4zOndy3FO9F2VfwkexfoBKe1i6UGN1zahmcAK/w8hWakLy aUIqbh4fXyG
  • Ironport-hdrordr: A9a23:VTSBXqmc1xa6OQkOJz2TulF9ulLpDfI33DAbv31ZSRFFG/Fw5P rOoB1773XJYVkqNE3I9erwW5VoIkmyyXcW2+Qs1N6ZNWGMhILCFvAB0WKN+V3d8mHFmNJg6Q ==
  • Ironport-phdr: A9a23:YUpoShyngN5G1jPXCzJNwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hyZtagm0gOBHd2Cra4e1ayO6+GocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalxI Ri2ognct8YbipZmJqot1xfFuHRFd/pXyG9yOV6fgxPw7dqs8ZB+9Chdp+gv/NNaX6XgeKQ4Q 71YDDA4PG0w+cbmqxrNQxaR63UFSmkZnQZGDAbD7BHhQ5f+qTD6ufZn2CmbJsL5U7Y5Uim/4 qhxSR/ojCAHNyMl8GzSl8d9gr5XrA6nqhdixIHafZyVNOFmfqzDYdwaWWRPXsFUVyNbA4O8a ZYEA+4OMOtcqoXwoUYFoxmjCgm2HO7g1jxGiHH50qI0zeovERzI0Rc6EN4SqnnZtsn5OLkQX O2z0aLGzS/Db/RT2Trl7obHaAshoeqSUrltbMfRzVMgGBnYjlSesoPlJTSV2foOs2OG6OdgU figi3U8qw5vuTWg3cMshZPTiYIIxFHL7j95wIErKt27UkJ0f8OkHYJWuiqHOIR4XtksTHt0u CYm1LIGo5i7cTAWxZkkxxPTduGLfoeM7x//SeudPzN1inJldr++iBi+70atx/HiWsSpzltEr iVIn9rMu30R1hHd5cmKRuV98Eql3zuEyg7d6uZBIU8ulKrbLYYswrExlpoPsUTDAzT5lF/3j K+Rbkkk9emo6/jnYrX7vZCQLZN7igb7Mqkoh8exAvw4PxATU2WY+emwzqPv8ELjTLlUkPE6j rPVvZLHKcgDpaO0BxVZ3ps/5xuxFTuqzdcVkHgdIF5Yeh+KiZXiNUvUL/DiF/i/hkyhkDd1y PDCOb3sGpDNIWLCkLflZ7py8EpcxxApwtBC6ZNbEasBIPXtVU/yrtDXEAI5PxS1w+bhFtp9y psTVX+MD6KZKq/er1CF6vgxL+WSeIMZojTwJ+U96/7rl3A5mFsdfaez3ZsQbXC1BvBmLF+CY Xr3nNgMCnwFvg4kQ+PwlV2DXyVcZ2y1X60i5TE3EpypDZrbSoCrm7OOxD27EYFOZmBaFlCMF m/le5icV/cWdC2SOtNhkiADVbW5V4Ah0giuuBbmxLpjM+rb4TYVtYnj1dhw/+3cjws+9T1yD 8SH0mGCVXt4nm0SR2x+4Kcqqktkj1yHzKJQgvpCFNUV6ekafB09MMv4xvdhBpjYXgvIY8iDU lGrQZ3yBTgqVd8ZydsHaltiEc+lgxOF0jf8UOxdrKCCGJFhqvGU5HP2PcsolyeuPMgJilAnR pAKLmi6nutk8BCVAYfVkkKfnqLsdKIG3SeL+n3QhXGWshR+Vwh9Gb7AQWhZflHf+NDw/VjPZ 7WqAL06LQFbzsOBbKZXOZXylVsTfP74I5zFZn6p3WK5BBKG3LSJOY7jYH4Q9C/ZAUEZjAoJ+ nuFcwUjVW+6u2yLKjtoGBr0Zl/0t+lzrHTuVkgv0wSDdFFszZKw8x8Rw/aYQvoOwbgevyoi7 ThpdLqk9/TRDdfI5w9ofaEHJMg4/E8CzmXB8Qp0Ip2nKalmwF8YaQV++U30hV1xDc1bnM4mo WlPrkI6IL+E0F5HazKT3IzhcrzRJG7o+RmzaqnQkljA2deS860L5bw2sVLm9A2uE0Mj9T1g3 bw3mzOY747RASIYVZv4T1k97R93pPfXf2h15o/Z02FtLbjhqiXLiJoiAOoozArlfs8KafPZU lWuVZdAX47xcb9P+RDhdB8PMeFM+bRhOsqnc6DDw6u3JKN7myrgi21b4Yd720bK9ixmS+eO0 YxWppPQlgaBSTr4i0+s987tnoURLzUbBXGy4SLgDYdMeadoeosIT2qzaZ7SpJ02l9v2VnhU+ UT2TVcPw9SkURCWZlXgwgdK0kkU53G603jdrXQ8g3QiqayR2zbLyuLpeU8cO2JFc2JliE/lP Ym+i91ysFGAVwEyj1Pl4E/7w/Mev6FjNyzIRl8OeSHqLmZkW6/2t7yYYscJ5ol6+SlQVe29Z xidRNuf61Me2jj4EkNUwDkyai6goJL0nFp3lSqRIW1yo3zQZcxrjU6PuZqGGbgLhGJAG3Awg CKfHlWmOti14diY8vWL+vuzUW6sTNwbcCXmy5+BqDru4GRrBROlmPXg0tbjEAU8zWr6z4wzB XiO9kq6ONOzkfvjYocFNgFyCVTx6tR3ANR7m4o039QL3GQCw46S5TwBmHvyNtNS3eT/amAMT HgF2Y2wgkCt1Ut9I3aO34+8WG+ax54rY9CheW4+0CY05t1VAr2T4b8CkDY/8T/a5UrBJONwm DsQ065k7HcBmOwhsg4kxziCCKoVEEoeMDGmxHHqp5iu6a5QYmioa7250kFzyMugAL+1qQZZQ H/le50mEHw4/oBlPVnLynG29pD8dYyac4cIrhPN2USl7aAdONcrm/ENnyYiJW/toShv1bsgl RI3lZSq9IHPPWxp+OjR7gdwEDrzaotT/zjsif0bhcOKx8W0GY0nHDwXXZzuRPbuETQItP2hO RzcWDs74myWH7bSB2r9oA9vsm7PHpa3NnqWOGhRzNNsQwOYLVBehwZcVSszn5owHASnjML7d 0Ix6jcU71/+4hxCr4AgfwH4SXvarRy0Zy0cTZGeKFxc6ghL+ljfK8uT7aR+AmAQ/5GsqhCMN n3OZwlMCjJsOATMDFTiM7+yoNjYprHIW6zkc72UO+3I9rUNMpXAjYii2YZn4TuWY8CGP305S uY+xlIGRndhXcLQhzQITSUT0SPLdc+S4hmmqUgV5oiy9urmXAX36M6BEbxXZJ9r8gutjI+JM +eZmTlzMzFV1dUB2DWbrdpXlE5XkCxoezS3RP4YsjXRSavLhqJNJxsSaic1Ps9B5r8j1BNKN M2dh86/hdsaxrYlTlxCU1LmgMSgY8cHdnq8OF3wD0GOLL2aJDfPzqkfhIu2TbRZkfperRq9u nCWDh27VtxivzzgVhTpO+VFhTyENgZZtYL7fws/UQALo/rsbhSyLcB9lzo7wvs5myGTXVM=
  • Ironport-sdr: 6535ed88_rs+pvRlnpqCAXHWwMBzOeJSMCMFU9Wl0CPkpHaNvgGb9IFC lydQmzprzDG/JDFjQ5VIjh0mK0sRvsBUxKIB0+Q==

Hello everyone,

After almost three years of development, we are happy to announce Tactician 1.0 beta2. It is available for all
Coq versions between v8.12 and v8.18. Tactician is a proof synthesis system that uses data from existing
theorems in order to help users write new proofs. It can adapt to, and learn from new developments on the fly.
For details, see the website and the list of publications.

Most of the development time in the past three years went to bug fixes, stability improvements, performance
improvements and other internal changes. No detailed changelog was kept, but we believe the usability has
improved significantly. There have also been a number of important user-facing changes:

  • The 'search' tactic has been renamed to 'synth' to avoid confusion with Coq's internal 'Search' command.
    (The 'Suggest' command remains the same.)
  • Starting from Coq v8.17, the standard library has been split from Coq's core, resulting in the packages
    'coq-core' and 'coq-stdlib'. The 'coq-tactician' package now depends only 'coq-core'. This allows
    Tactician to instrument 'coq-stdlib' while it is being installed in order to learn from it, obviating the
    need for the 'coq-tactician-stdlib' package. (See the manual for further instructions.)
  • In the past years, the landscape of available Coq editors has changed significantly. The support for the
    various editors is as follows:
  • Coqide: Fully supported.
  • Emacs with Proof General: Fully supported.
  • Coq-lsp: Partially supported. Tactician can be loaded through 'From Tactician Require Import Ltac1',
    but support for injecting Tactician through launching VsCode with 'tactician exec code' is unavailable.
  • VsCoq Legacy: Supported. Support for launching VsCode through 'tactician exec code' is available
    starting Coq v8.12.
  • VsCoq 2.0: Currently incompatible with Tactician.
            If you encounter any issues with these editors, please open an issue.
  •  Tactician is now fully open source under the MIT license. As such, this is an invitation for other researchers
    to use the data available in Tactician to build their own proof synthesizer. If you have a great idea,
    don't hesitate to reach out for a potential collaboration.

Regards,
Lasse Blaauwbroek



  • [Coq-Club] Announcing Tactician version 1.0 beta2, Lasse Blaauwbroek, 10/23/2023

Archive powered by MHonArc 2.6.19+.

Top of Page