--- 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