# HG changeset patch
# User wenzelm
# Date 1602761056 -7200
# Node ID b452242dce3603d23fdf5ddaa27c1e0c77d5affd
# Parent  56ef403eab15c4ccf6c05dcda59f880f273e3b1c
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;

diff -r 56ef403eab15 -r b452242dce36 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Oct 14 22:30:18 2020 +0200
+++ b/Admin/components/components.sha1	Thu Oct 15 13:24:16 2020 +0200
@@ -330,6 +330,7 @@
 869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd  vampire-1.0.tar.gz
 399f687b56575b93e730f68c91c989cb48aa34d8  vampire-4.2.2.tar.gz
 98c5c79fef7256db9f64c8feea2edef0a789ce46  verit-2016post.tar.gz
+52ba18a6c96b53c5ae9b179d5a805a0c08f1da6d  verit-2020.10-rmx-1.tar.gz
 b6706e74e20e14038e9b38f0acdb5639a134246a  verit-2020.10-rmx.tar.gz
 81d21dfd0ea5c58f375301f5166be9dbf8921a7a  windows_app-20130716.tar.gz
 fe15e1079cf5ad86f3cbab4553722a0d20002d11  windows_app-20130905.tar.gz
diff -r 56ef403eab15 -r b452242dce36 Admin/components/main
--- a/Admin/components/main	Wed Oct 14 22:30:18 2020 +0200
+++ b/Admin/components/main	Thu Oct 15 13:24:16 2020 +0200
@@ -21,5 +21,6 @@
 ssh-java-20190323
 stack-2.1.3
 vampire-4.2.2
+verit-2020.10-rmx-1
 xz-java-1.8
 z3-4.4.0pre-3
diff -r 56ef403eab15 -r b452242dce36 CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Oct 14 22:30:18 2020 +0200
+++ b/CONTRIBUTORS	Thu Oct 15 13:24:16 2020 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* October 2020: Mathias Fleury
+  Updated proof reconstruction for the SMT solver veriT in the smt method.
+
 * August 2020: Makarius Wenzel
   Improved monitoring of runtime statistics: ML GC progress and Java.
 
diff -r 56ef403eab15 -r b452242dce36 NEWS
--- a/NEWS	Wed Oct 14 22:30:18 2020 +0200
+++ b/NEWS	Thu Oct 15 13:24:16 2020 +0200
@@ -70,6 +70,11 @@
 
 *** HOL ***
 
+* An updated version of the veriT solver is now included as Isabelle
+component. It can be used in the "smt" proof method via "smt (verit)" or
+via "declare [[smt_solver = verit]]" in the context; see also session
+HOL-Word-SMT_Examples.
+
 * 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
@@ -158,9 +163,6 @@
 are in working order again, as opposed to outputting "GaveUp" on nearly
 all problems.
 
-* SMT reconstruction: It is now possible to reconstruct proofs from the
-SMT solver veriT by calling "smt (verit)".
-
 
 *** FOL ***
 
diff -r 56ef403eab15 -r b452242dce36 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Oct 14 22:30:18 2020 +0200
+++ b/src/HOL/ROOT	Thu Oct 15 13:24:16 2020 +0200
@@ -932,7 +932,7 @@
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests
-  theories[condition=VERIT_SOLVER]
+  theories [condition = ISABELLE_VERIT]
     SMT_Tests_Verit
     SMT_Examples_Verit
 
diff -r 56ef403eab15 -r b452242dce36 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Oct 14 22:30:18 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Oct 15 13:24:16 2020 +0200
@@ -15,6 +15,11 @@
 
 (* helper functions *)
 
+fun check_tool var () =
+  (case getenv var of
+    "" => NONE
+  | s => if File.is_file (Path.variable var) then SOME [s] else NONE);
+
 fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
 
 fun make_command name () = [getenv (name ^ "_SOLVER")]
@@ -117,8 +122,8 @@
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
   class = select_class,
-  avail = make_avail "VERIT",
-  command = make_command "VERIT",
+  avail = is_some o check_tool "ISABELLE_VERIT",
+  command = the o check_tool "ISABELLE_VERIT",
   options = (fn ctxt => [
     "--proof-with-sharing",
     "--proof-define-skolems",
diff -r 56ef403eab15 -r b452242dce36 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Wed Oct 14 22:30:18 2020 +0200
+++ b/src/Pure/Admin/build_verit.scala	Thu Oct 15 13:24:16 2020 +0200
@@ -97,15 +97,7 @@
       File.write(etc_dir + Path.basic("settings"),
         """# -*- shell-script -*- :mode=shellscript:
 
-VERIT_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
-VERIT_VERSION=""" + quote(version) + """
-
-VERIT_SOLVER="$VERIT_HOME/veriT"
-
-if [ -e "$VERIT_HOME" ]
-then
-  VERIT_INSTALLED="yes"
-fi
+ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
 """)