--- a/Admin/components/components.sha1 Mon Dec 21 13:03:23 2020 +0100
+++ b/Admin/components/components.sha1 Mon Dec 21 13:58:11 2020 +0100
@@ -369,4 +369,5 @@
4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
+9dfeb39c87393af7b6a34118507637aa53aca05e zipperposition-2.0-1.tar.gz
b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
--- a/Admin/components/main Mon Dec 21 13:03:23 2020 +0100
+++ b/Admin/components/main Mon Dec 21 13:58:11 2020 +0100
@@ -24,4 +24,4 @@
verit-2020.10-rmx-1
xz-java-1.8
z3-4.4.0pre-3
-zipperposition-2.0
+zipperposition-2.0-1
--- a/CONTRIBUTORS Mon Dec 21 13:03:23 2020 +0100
+++ b/CONTRIBUTORS Mon Dec 21 13:58:11 2020 +0100
@@ -5,6 +5,10 @@
Contributions to this Isabelle version
--------------------------------------
+
+* December 2020: Martin Desharnais
+ Zipperposition 2.0 as external prover for Sledgehammer (experimental).
+
* December 2020 Walter Guttmann
Extension of session HOL/Hoare with total correctness proof system
--- a/NEWS Mon Dec 21 13:03:23 2020 +0100
+++ b/NEWS Mon Dec 21 13:58:11 2020 +0100
@@ -110,6 +110,9 @@
via "declare [[smt_solver = verit]]" in the context; see also session
HOL-Word-SMT_Examples.
+* Zipperposition 2.0 is included as Isabelle component for
+experimentation, e.g. in "sledgehammer [prover = zipperposition]".
+
* Nitpick/Kodkod may be invoked directly within the running
Isabelle/Scala session (instead of an external Java process): this
improves reactivity and saves resources. This experimental feature is
@@ -246,9 +249,6 @@
* Update/rebuild external provers on currently supported OS platforms,
notably CVC4 1.8, E prover 2.5, SPASS 3.8ds, CSDP 6.1.1.
-* External prover Zipperposition 2.0 is available as component for
-experimentation.
-
* Discontinued obsolete isabelle display tool, and DVI_VIEWER settings
variable.
--- a/src/Pure/Admin/build_zipperposition.scala Mon Dec 21 13:03:23 2020 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala Mon Dec 21 13:58:11 2020 +0100
@@ -72,7 +72,7 @@
File.write(etc_dir + Path.basic("settings"),
"""# -*- shell-script -*- :mode=shellscript:
-ISABELLE_ZIPPERPOSITION="$COMPONENT/$ISABELLE_PLATFORM64/zipperposition"
+ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
""")