Stream: Mirror: Isabelle Development Mailing List

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


view this post on Zulip Email Gateway (Oct 19 2020 at 15:34):

From: Makarius <makarius@sketis.net>
* HOL *

* System *

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC