[isabelle-dev] NEWS: update of external provers
Makarius
makarius at sketis.net
Mon Oct 19 17:34:29 CEST 2020
*** HOL ***
* An updated version of the veriT solver is now included as Isabelle
component. It can be used in the "smt" proof method via "smt (verit)" or
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.
*** System ***
* Update/rebuild external provers on currently supported OS platforms,
notably E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
This refers to various changes in the past few weeks, culminating in current
Isabelle/b5f7fc7d2323.
We still have until approx. 15-Dec-2020 to include/update more external
provers. Due to some new "isabelle build_XYZ" tools this is getting more and
more robust and reproducibly, on an increasing number of platforms:
arm64-linux already works for many things (even though it is strictly speaking
a toy right now).
Makarius
More information about the isabelle-dev
mailing list