We are happy to announce the release of CoqHammer 1.1.1 for Coq 8.9.
CoqHammer is a general-purpose automated reasoning tool that combines learning from previous proofs with the translation of problems to the logics of automated provers and the reconstruction of successfully found proofs via tactics.
In a typical workflow, the user first tries the
hammer tactic which invokes one or more automated provers, and, if successful, prints a sequence of calls to custom reconstruction tactics bundled with CoqHammer. The user can then substitute this sequence for the
hammer invocation. The reconstruction tactics can also be used standalone.
The key changes in this version are as follows:
- Separate packaging in OPAM of the reconstruction tactics (
coq-hammer-tactics) and the Coq plugin (
- Quick plugin and tactics tests which do not require automated provers installed (
- Machine-learning features now take into account the polarity (positive/negative) of symbol occurrences (
- Opaqueness information now taken into account with constant unfolding.
The easiest way to install CoqHammer is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-hammer
Note that for the best experience using the hammer, users should install all supported automated provers (Vampire, CVC4, Eprover, and Z3) according to the instructions.