merged
authorhaftmann
Tue, 18 Jan 2011 09:44:29 +0100
changeset 41653 3b81d1d1f0d0
parent 41651 c78b786fe060 (diff)
parent 41652 4f4336e730b9 (current diff)
child 41655 95f851027a59
child 41656 011fcb70e32f
merged
--- a/Admin/CHECKLIST	Tue Jan 18 09:44:23 2011 +0100
+++ b/Admin/CHECKLIST	Tue Jan 18 09:44:29 2011 +0100
@@ -3,7 +3,7 @@
 
 - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
 
-- test Proof General 4.1;
+- test Proof General 4.1, 4.0, 3.7.1.1;
 
 - test Scala wrapper;
 
@@ -45,3 +45,15 @@
 - makebundle (multiplatform);
 
 - hdiutil create -srcfolder DIR DMG (Mac OS);
+
+
+Final release stage
+===================
+
+- hgrc: default = /home/isabelle-repository/repos/isabelle-release
+
+  isatest@macbroy28:hg-isabelle/.hg/hgrc
+  isatest@atbroy102:hg-isabelle/.hg/hgrc
+
+- makedist: REPOS_NAME="isabelle-release"
+
--- a/Admin/isatest/isatest-makedist	Tue Jan 18 09:44:23 2011 +0100
+++ b/Admin/isatest/isatest-makedist	Tue Jan 18 09:44:29 2011 +0100
@@ -100,9 +100,9 @@
 $SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test"
 # give test some time to copy settings and start
 sleep 15
-$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
+$SSH macbroy28 "$MAKEALL $HOME/settings/at-poly"
 sleep 15
-$SSH macbroy28 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
+$SSH macbroy22 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
 sleep 15
 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
--- a/CONTRIBUTORS	Tue Jan 18 09:44:23 2011 +0100
+++ b/CONTRIBUTORS	Tue Jan 18 09:44:29 2011 +0100
@@ -3,6 +3,10 @@
 who is listed as an author in one of the source files of this Isabelle
 distribution.
 
+Contributions to this Isabelle version
+--------------------------------------
+
+
 Contributions to Isabelle2011
 -----------------------------
 
--- a/NEWS	Tue Jan 18 09:44:23 2011 +0100
+++ b/NEWS	Tue Jan 18 09:44:29 2011 +0100
@@ -1,6 +1,11 @@
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
+New in this Isabelle version
+----------------------------
+
+
+
 New in Isabelle2011 (January 2011)
 ----------------------------------
 
@@ -279,9 +284,12 @@
 * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
 manually as command 'solve_direct'.
 
-* The default SMT solver is now CVC3.  Z3 must be enabled explicitly
-(due to licensing issues) via Z3_NON_COMMERCIAL in etc/settings of the
-component, for example.
+* The default SMT solver Z3 must be enabled explicitly (due to
+licensing issues) by setting the environment variable
+Z3_NON_COMMERCIAL in etc/settings of the component, for example.  For
+commercial applications, the SMT solver CVC3 is provided as fall-back;
+changing the SMT solver is done via the configuration option
+"smt_solver".
 
 * Remote SMT solvers need to be referred to by the "remote_" prefix,
 i.e. "remote_cvc3" and "remote_z3".
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -84,7 +84,7 @@
 
 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_vc Dijkstra
   by boogie
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -41,7 +41,7 @@
 
 declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_vc max
   by boogie
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -49,7 +49,7 @@
 
 declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 boogie_status
 
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -12,7 +12,7 @@
 
 declare [[smt_certificates="Integration.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 
 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
 
@@ -5527,6 +5527,5 @@
 
 declare [[smt_certificates=""]]
 declare [[smt_fixed=false]]
-declare [[smt_solver=cvc3]]
 
 end
--- a/src/HOL/SMT.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/SMT.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -185,7 +185,7 @@
 @{text yes}.
 *}
 
-declare [[ smt_solver = cvc3 ]]
+declare [[ smt_solver = z3 ]]
 
 text {*
 Since SMT solvers are potentially non-terminating, there is a timeout
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 declare [[smt_certificates="SMT_Examples.certs"]]
 declare [[smt_fixed=true]]
 
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
 declare [[smt_certificates="SMT_Tests.certs"]]
 declare [[smt_fixed=true]]
 
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Tue Jan 18 09:44:29 2011 +0100
@@ -8,7 +8,7 @@
 imports Word
 begin
 
-declare [[smt_solver=z3, smt_oracle=true]]
+declare [[smt_oracle=true]]
 declare [[smt_certificates="SMT_Word_Examples.certs"]]
 declare [[smt_fixed=true]]
 
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Jan 18 09:44:29 2011 +0100
@@ -93,6 +93,15 @@
 (* Z3 *)
 
 local
+  val flagN = "Z3_NON_COMMERCIAL"
+
+  fun z3_make_command is_remote name () =
+    if getenv flagN = "yes" then make_command is_remote name ()
+    else
+      error ("The SMT solver Z3 is not enabled. To enable it, set " ^
+        "the environment variable " ^ quote flagN ^ " to " ^ quote ("yes") ^
+        ".")
+
   fun z3_options ctxt =
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
       "MODEL=true", "-smt"]
@@ -117,7 +126,7 @@
     name = make_name is_remote "z3",
     class = Z3_Interface.smtlib_z3C,
     avail = make_avail is_remote "Z3",
-    command = make_command is_remote "Z3",
+    command = z3_make_command is_remote "Z3",
     options = z3_options,
     default_max_relevant = 225,
     supports_filter = true,
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Jan 18 09:44:23 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Jan 18 09:44:29 2011 +0100
@@ -55,7 +55,7 @@
 local
 
 fun make_cmd command options problem_path proof_path = space_implode " " (
-  map File.shell_quote (command @ options) @
+  map File.shell_quote (command () @ options) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
 fun trace_and ctxt msg f x =
@@ -136,7 +136,7 @@
       |> tap (trace_assms ctxt)
       |> SMT_Translate.translate ctxt comments
       ||> tap trace_recon_data
-  in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end
+  in (run_solver ctxt' name (make_cmd command options) str, recon) end
 
 end