[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