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:
searchtactic has been renamed to
synthto avoid confusion with Coq’s internal
Suggestcommand remains the same.)
Starting from Coq v8.17, the standard library has been split from Coq’s core, resulting in the packages
coq-tacticianpackage now depends only on
coq-core. This allows Tactician to instrument
coq-stdlibwhile it is being installed in order to learn from it, obviating the need for the
coq-tactician-stdlibpackage. (See the manual for
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 codeis unavailable.
- VsCoq Legacy: Supported. Support for launching VsCode through
tactician exec codeis 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.
Any feedback on this beta release is appreciated. Do not hesitate to open an issue.