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
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
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
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 07 2024 at 16:22 UTC