# HG changeset patch
# User wenzelm
# Date 1608555491 -3600
# Node ID 162b71f7e55427e4fe4f65874d1f8f4768642cda
# Parent  06e5ba0d1d2cc25c34dc45b32c5b6152a720e9ea
rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;

diff -r 06e5ba0d1d2c -r 162b71f7e554 Admin/components/components.sha1
--- 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
diff -r 06e5ba0d1d2c -r 162b71f7e554 Admin/components/main
--- 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
diff -r 06e5ba0d1d2c -r 162b71f7e554 CONTRIBUTORS
--- 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
 
diff -r 06e5ba0d1d2c -r 162b71f7e554 NEWS
--- 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.
 
diff -r 06e5ba0d1d2c -r 162b71f7e554 src/Pure/Admin/build_zipperposition.scala
--- 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"
 """)