--- a/Admin/isatest/settings/mac-poly-M4 Mon Sep 22 10:53:54 2014 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Mon Sep 22 10:55:51 2014 +0200
@@ -8,8 +8,6 @@
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500 --gcthreads 4"
-ISABELLE_GHC=ghc
-
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
# Where to look for isabelle tools (multiple dirs separated by ':').
@@ -30,5 +28,13 @@
ISABELLE_FULL_TEST=true
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
+
Z3_NON_COMMERCIAL="yes"
--- a/Admin/isatest/settings/mac-poly-M8 Mon Sep 22 10:53:54 2014 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Mon Sep 22 10:55:51 2014 +0200
@@ -8,8 +8,6 @@
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500 --gcthreads 8"
-ISABELLE_GHC=ghc
-
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
# Where to look for isabelle tools (multiple dirs separated by ':').
@@ -30,5 +28,13 @@
ISABELLE_FULL_TEST=true
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
+
Z3_NON_COMMERCIAL="yes"
--- a/src/HOL/Codegenerator_Test/code_test.ML Mon Sep 22 10:53:54 2014 +0200
+++ b/src/HOL/Codegenerator_Test/code_test.ML Mon Sep 22 10:55:51 2014 +0200
@@ -25,7 +25,7 @@
-> string -> string -> string
-> theory -> (string * string) list * string -> Path.T -> string
- val ISABELLE_POLYML_PATH : string
+ val ISABELLE_POLYML : string
val polymlN : string
val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
@@ -316,7 +316,7 @@
(* Driver for PolyML *)
-val ISABELLE_POLYML_PATH = "ISABELLE_POLYML_PATH"
+val ISABELLE_POLYML = "ISABELLE_POLYML"
val polymlN = "PolyML";
fun mk_driver_polyml _ path _ value_name =
@@ -343,12 +343,12 @@
val cmd =
"echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
Path.implode driver_path ^ "\\\"; main ();\" | " ^
- Path.implode (Path.variable ISABELLE_POLYML_PATH)
+ Path.implode (Path.variable ISABELLE_POLYML)
in
{files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
end
-val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML_PATH "PolyML executable" polymlN
+val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
(* Driver for mlton *)
--- a/src/HOL/ROOT Mon Sep 22 10:53:54 2014 +0200
+++ b/src/HOL/ROOT Mon Sep 22 10:55:51 2014 +0200
@@ -242,17 +242,17 @@
Generate_Efficient_Datastructures
Generate_Pretty_Char
Code_Test
- theories[condition = ISABELLE_GHC]
+ theories [condition = ISABELLE_GHC]
Code_Test_GHC
- theories[condition = ISABELLE_MLTON]
+ theories [condition = ISABELLE_MLTON]
Code_Test_MLton
- theories[condition = ISABELLE_OCAMLC]
+ theories [condition = ISABELLE_OCAMLC]
Code_Test_OCaml
- theories[condition = ISABELLE_POLYML_PATH]
+ theories [condition = ISABELLE_POLYML]
Code_Test_PolyML
- theories[condition = ISABELLE_SCALA]
+ theories [condition = ISABELLE_SCALA]
Code_Test_Scala
- theories[condition = ISABELLE_SMLNJ]
+ theories [condition = ISABELLE_SMLNJ]
Code_Test_SMLNJ
session "HOL-Metis_Examples" in Metis_Examples = HOL +