See also 796ae338eb9d: use z3-4.4.1 for arm64-linux, which often works like pre-4.4.0 and sometimes crashes.

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.

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.

Also missing: arm64-linux, arm64-darwin (relavant for native JDK on macOS).

See Isabelle/162b71f7e554 and Isabelle/11de287ed481.

Isabelle/4a652d3f4522 provides isabelle build_zipperposition for 2.0 from OPAM. It works uniformly for Linux, macOS, Windows/Cygwin.

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);
      |           ^~~~~~~~~

Isabelle/dcc0022f0179 provides a manually assembled component, without isabelle build_cvc4 tool.

The veriT version is sufficient for the next release.