Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: update of external provers

Email Gateway (Oct 19 2020 at 15:34):

From: Makarius <makarius@sketis.net>
* 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

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 19 2020 at 15:40):

From: Makarius <makarius@sketis.net>
Meta question: should we advertize these prover changes/updates more
prominently? What are really the NEWS for end-users? Is there anything in
particular to say about the brand-new "verit" vs. the old "z3"?

(The z3 component unlikely to be updated for the Isabelle2021 release, unless
Sascha Boehme finishes his long-standing effort to follow the z3 release cycle
again.)

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 19 2020 at 15:50):

From: Lawrence Paulson <lp15@cam.ac.uk>
I was wanting to know exactly the same thing. In particular, will sledgehammer suggest it now? And does it give us a version of the smt method more robust than the existing one?

Larry

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Email Gateway (Oct 29 2020 at 16:51):

From: Makarius <makarius@sketis.net>
The general situation of external provers, notably for the coming Isabelle
release, is now formally documented here:
https://isabelle-dev.sketis.net/maniphest/query/wmDbg8skd7cl

A less cryptic path to this information is https://isabelle-dev.sketis.net /
"Tasks" / "Tag: provers".

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Dec 21 2024 at 16:20 UTC