External provers for Sledgehammer, SMT etc.
Details
Nov 27 2021
See also 796ae338eb9d: use z3-4.4.1 for arm64-linux, which often works like pre-4.4.0 and sometimes crashes.
Oct 19 2021
Not ready for the Isabelle2021-1 release, approx. 15-Dec-2021. Note that veriT is more and more taking over.
See Isabelle/d4c2a9191cd1
See also Isabelle/74a36aae067a and Isabelle/2d089ff0e03b --- minisat is provided as external executable on all platforms.
Mar 17 2021
Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.
Jan 7 2021
Also missing: arm64-linux, arm64-darwin (relavant for native JDK on macOS).
See Isabelle/162b71f7e554 and Isabelle/11de287ed481.
Dec 18 2020
Isabelle/4a652d3f4522 provides isabelle build_zipperposition for 2.0 from OPAM. It works uniformly for Linux, macOS, Windows/Cygwin.
Dec 13 2020
Isabelle/6751057a64b1 provides isabelle build_vampire for two versions: regular (stable) vampire, and experimental (latest) vampire_polymorphic. The latter does not build on Windows/Cygwin, though:
scope 489 | case DT_REG: | ^~~~~~ /tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/System.cpp:492:14: error: ÔÇÿDT_DIRÔÇÖ was not declared in this scope 492 | case DT_DIR: | ^~~~~~ make[2]: *** [CMakeFiles/obj.dir/build.make:304: CMakeFiles/obj.dir/Lib/System.cpp.o] Error 1 make[2]: *** Waiting for unfinished jobs.... /tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/Timer.cpp: In static member function ÔÇÿstatic void Lib::Timer::suspendTimerBeforeFork()ÔÇÖ: /tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/Timer.cpp:155:11: error: ÔÇÿsetitimerÔÇÖ was not declared in this scope 155 | int res=setitimer(ITIMER_REAL, &tv1, &tv2); | ^~~~~~~~~
Dec 4 2020
Nov 22 2020
Isabelle/dcc0022f0179 provides a manually assembled component, without isabelle build_cvc4 tool.
Oct 31 2020
The veriT version is sufficient for the next release.