clarified ISABELLE_POLYML;
authorwenzelm
Mon Sep 22 10:18:41 2014 +0200 (2014-09-22)
changeset 584158392d221bd91
parent 58413 22dd971f6938
child 58416 d94ec306b7a8
clarified ISABELLE_POLYML;
added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;
Admin/isatest/settings/mac-poly-M4
Admin/isatest/settings/mac-poly-M8
src/HOL/Codegenerator_Test/code_test.ML
src/HOL/ROOT
     1.1 --- a/Admin/isatest/settings/mac-poly-M4	Sun Sep 21 20:22:12 2014 +0200
     1.2 +++ b/Admin/isatest/settings/mac-poly-M4	Mon Sep 22 10:18:41 2014 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     1.5    ML_OPTIONS="-H 500 --gcthreads 4"
     1.6  
     1.7 -ISABELLE_GHC=ghc
     1.8 -
     1.9  ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
    1.10  
    1.11  # Where to look for isabelle tools (multiple dirs separated by ':').
    1.12 @@ -30,5 +28,13 @@
    1.13  
    1.14  ISABELLE_FULL_TEST=true
    1.15  
    1.16 +ISABELLE_GHC=ghc
    1.17 +ISABELLE_MLTON=mlton
    1.18 +ISABELLE_OCAML=ocaml
    1.19 +ISABELLE_OCAMLC=ocamlc
    1.20 +ISABELLE_POLYML="$ML_HOME/poly"
    1.21 +#ISABELLE_SCALA="$SCALA_HOME/bin"
    1.22 +ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
    1.23 +
    1.24  Z3_NON_COMMERCIAL="yes"
    1.25  
     2.1 --- a/Admin/isatest/settings/mac-poly-M8	Sun Sep 21 20:22:12 2014 +0200
     2.2 +++ b/Admin/isatest/settings/mac-poly-M8	Mon Sep 22 10:18:41 2014 +0200
     2.3 @@ -8,8 +8,6 @@
     2.4    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
     2.5    ML_OPTIONS="-H 500 --gcthreads 8"
     2.6  
     2.7 -ISABELLE_GHC=ghc
     2.8 -
     2.9  ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
    2.10  
    2.11  # Where to look for isabelle tools (multiple dirs separated by ':').
    2.12 @@ -30,5 +28,13 @@
    2.13  
    2.14  ISABELLE_FULL_TEST=true
    2.15  
    2.16 +ISABELLE_GHC=ghc
    2.17 +ISABELLE_MLTON=mlton
    2.18 +ISABELLE_OCAML=ocaml
    2.19 +ISABELLE_OCAMLC=ocamlc
    2.20 +ISABELLE_POLYML="$ML_HOME/poly"
    2.21 +#ISABELLE_SCALA="$SCALA_HOME/bin"
    2.22 +ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
    2.23 +
    2.24  Z3_NON_COMMERCIAL="yes"
    2.25  
     3.1 --- a/src/HOL/Codegenerator_Test/code_test.ML	Sun Sep 21 20:22:12 2014 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/code_test.ML	Mon Sep 22 10:18:41 2014 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4     -> string -> string -> string
     3.5     -> theory -> (string * string) list * string -> Path.T -> string
     3.6  
     3.7 -  val ISABELLE_POLYML_PATH : string
     3.8 +  val ISABELLE_POLYML : string
     3.9    val polymlN : string
    3.10    val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
    3.11  
    3.12 @@ -316,7 +316,7 @@
    3.13  
    3.14  (* Driver for PolyML *)
    3.15  
    3.16 -val ISABELLE_POLYML_PATH = "ISABELLE_POLYML_PATH"
    3.17 +val ISABELLE_POLYML = "ISABELLE_POLYML"
    3.18  val polymlN = "PolyML";
    3.19  
    3.20  fun mk_driver_polyml _ path _ value_name =
    3.21 @@ -343,12 +343,12 @@
    3.22      val cmd =
    3.23        "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
    3.24        Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
    3.25 -      Path.implode (Path.variable ISABELLE_POLYML_PATH)
    3.26 +      Path.implode (Path.variable ISABELLE_POLYML)
    3.27    in
    3.28      {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
    3.29    end
    3.30  
    3.31 -val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML_PATH "PolyML executable" polymlN
    3.32 +val evaluate_in_polyml = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN
    3.33  
    3.34  (* Driver for mlton *)
    3.35  
     4.1 --- a/src/HOL/ROOT	Sun Sep 21 20:22:12 2014 +0200
     4.2 +++ b/src/HOL/ROOT	Mon Sep 22 10:18:41 2014 +0200
     4.3 @@ -242,17 +242,17 @@
     4.4      Generate_Efficient_Datastructures
     4.5      Generate_Pretty_Char
     4.6      Code_Test
     4.7 -  theories[condition = ISABELLE_GHC]
     4.8 +  theories [condition = ISABELLE_GHC]
     4.9      Code_Test_GHC
    4.10 -  theories[condition = ISABELLE_MLTON]
    4.11 +  theories [condition = ISABELLE_MLTON]
    4.12      Code_Test_MLton
    4.13 -  theories[condition = ISABELLE_OCAMLC]
    4.14 +  theories [condition = ISABELLE_OCAMLC]
    4.15      Code_Test_OCaml
    4.16 -  theories[condition = ISABELLE_POLYML_PATH]
    4.17 +  theories [condition = ISABELLE_POLYML]
    4.18      Code_Test_PolyML
    4.19 -  theories[condition = ISABELLE_SCALA]
    4.20 +  theories [condition = ISABELLE_SCALA]
    4.21      Code_Test_Scala
    4.22 -  theories[condition = ISABELLE_SMLNJ]
    4.23 +  theories [condition = ISABELLE_SMLNJ]
    4.24      Code_Test_SMLNJ
    4.25  
    4.26  session "HOL-Metis_Examples" in Metis_Examples = HOL +