# HG changeset patch # User wenzelm # Date 1600628980 -7200 # Node ID ae89eac1d332a685a974a4592db6ba167bded9bc # Parent 7e90e1d178b52db53c3eb147dd3e5bff9a5cf83a# Parent 199dc903131b8744416d4b3d50a4b86b651c3784 merged diff -r 7e90e1d178b5 -r ae89eac1d332 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sun Sep 20 21:09:40 2020 +0200 @@ -41,8 +41,8 @@ val (output, rc) = Isabelle_System.bash_output ("\"$ISABELLE_CSDP\" " ^ - Bash.string (File.platform_path in_path) ^ " " ^ - Bash.string (File.platform_path out_path)); + File.bash_platform_path in_path ^ " " ^ + File.bash_platform_path out_path); val _ = Sum_of_Squares.debug_message ctxt (fn () => "Solver output:\n" ^ output) val result = if File.exists out_path then File.read out_path else "" diff -r 7e90e1d178b5 -r ae89eac1d332 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/HOL/Library/code_test.ML Sun Sep 20 21:09:40 2020 +0200 @@ -18,13 +18,9 @@ val test_targets: Proof.context -> term list -> string list -> unit val test_code_cmd: string list -> string list -> Proof.context -> unit val eval_term: string -> Proof.context -> term -> term - val evaluate: - (theory -> Path.T -> string list -> string -> - {files: (Path.T * string) list, - compile_cmd: string option, - run_cmd: string, - mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory -> - (string * string) list * string -> Path.T -> string + val check_settings: string -> string -> string -> unit + val compile: string -> string -> unit + val evaluate: string -> string -> string val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string @@ -120,7 +116,7 @@ fun parse_result target out = (case split_first_last start_markerN end_markerN out of - NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out) + NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out) | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line) @@ -136,9 +132,9 @@ (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = - Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") - @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] - @ pretty_eval ctxt evals eval_ts) + Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ + [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @ + pretty_eval ctxt evals eval_ts) fun pretty_failures ctxt target failures = Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) @@ -150,10 +146,10 @@ fun with_overlord_dir name f = let - val path = + val dir = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) - val _ = Isabelle_System.mkdirs path - in Exn.release (Exn.capture f path) end + val _ = Isabelle_System.mkdirs dir + in Exn.release (Exn.capture f dir) end fun dynamic_value_strict ctxt t compiler = let @@ -161,14 +157,14 @@ val (driver, target) = (case get_driver thy compiler of NONE => error ("No driver for target " ^ compiler) - | SOME f => f) + | SOME drv => drv) val debug = Config.get (Proof_Context.init_global thy) overlord val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir - fun evaluate result = + fun eval result = with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result)) |> parse_result compiler fun evaluator program _ vs_ty deps = - Exn.interruptible_capture evaluate + Exn.interruptible_capture eval (Code_Target.compilation_text ctxt target program deps true vs_ty) fun postproc f = map (apsnd (Option.map (map f))) in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end @@ -229,10 +225,10 @@ val failed = filter_out (fst o fst o fst) (result ~~ ts ~~ evals) handle ListPair.UnequalLengths => - error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result)) + error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result)) in - (case failed of [] => - () + (case failed of + [] => () | _ => error (Pretty.string_of (pretty_failures ctxt target failed))) end @@ -275,61 +271,39 @@ in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end -(* generic driver *) +(* check and invoke compiler *) -fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) = - let - val _ = - (case opt_env_var of - NONE => () - | SOME (env_var, env_var_dest) => - (case getenv env_var of - "" => - error (Pretty.string_of (Pretty.para - ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^ - compilerN ^ ", set this variable to your " ^ env_var_dest ^ - " in the $ISABELLE_HOME_USER/etc/settings file."))) - | _ => ())) +fun check_settings compiler var descr = + if getenv var = "" then + error (Pretty.string_of (Pretty.para + ("Environment variable " ^ var ^ " is not set. To test code generation with " ^ + compiler ^ ", set this variable to your " ^ descr ^ + " in the $ISABELLE_HOME_USER/etc/settings file."))) + else (); - fun compile NONE = () - | compile (SOME cmd) = - let - val (out, ret) = Isabelle_System.bash_output cmd - in - if ret = 0 then () - else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out) - end +fun compile compiler cmd = + let val (out, ret) = Isabelle_System.bash_output cmd in + if ret = 0 then () + else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out) + end - fun run path = - let - val modules = map fst code_files - val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name - - val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files - val _ = List.app (fn (name, content) => File.write name content) files - - val _ = compile compile_cmd - - val (out, res) = Isabelle_System.bash_output run_cmd - val _ = - if res = 0 then () - else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ - Int.toString res ^ "\nBash output:\n" ^ out) - in out end - in run end +fun evaluate compiler cmd = + let val (out, res) = Isabelle_System.bash_output cmd in + if res = 0 then out + else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^ + string_of_int res ^ "\nCompiler output:\n" ^ out) + end (* driver for PolyML *) val polymlN = "PolyML" -fun mk_driver_polyml _ path _ value_name = +fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir = let - val generatedN = "generated.sml" - val driverN = "driver.sml" - - val code_path = Path.append path (Path.basic generatedN) - val driver_path = Path.append path (Path.basic driverN) + val compiler = polymlN + val code_path = Path.append dir (Path.basic "generated.sml") + val driver_path = Path.append dir (Path.basic "driver.sml") val driver = "fun main prog_name = \n" ^ " let\n" ^ @@ -343,33 +317,33 @@ " val _ = print \"" ^ end_markerN ^ "\";\n" ^ " in\n" ^ " ()\n" ^ - " end;\n" + " end;\n"; val cmd = - "\"$POLYML_EXE\" --use " ^ Bash.string (File.platform_path code_path) ^ - " --use " ^ Bash.string (File.platform_path driver_path) ^ + "\"$POLYML_EXE\" --use " ^ File.bash_platform_path code_path ^ + " --use " ^ File.bash_platform_path driver_path ^ " --eval " ^ Bash.string "main ()" in - {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + evaluate compiler cmd end -fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt - (* driver for mlton *) val mltonN = "MLton" val ISABELLE_MLTON = "ISABELLE_MLTON" -fun mk_driver_mlton _ path _ value_name = +fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir = let + val compiler = mltonN val generatedN = "generated.sml" val driverN = "driver.sml" val projectN = "test" - val ml_basisN = projectN ^ ".mlb" - val code_path = Path.append path (Path.basic generatedN) - val driver_path = Path.append path (Path.basic driverN) - val ml_basis_path = Path.append path (Path.basic ml_basisN) + val code_path = Path.append dir (Path.basic generatedN) + val driver_path = Path.append dir (Path.basic driverN) + val basis_path = Path.append dir (Path.basic (projectN ^ ".mlb")) val driver = "fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ @@ -379,36 +353,30 @@ "val _ = print \"" ^ start_markerN ^ "\";\n" ^ "val _ = map (print o format) result;\n" ^ "val _ = print \"" ^ end_markerN ^ "\";\n" - val ml_basis = - "$(SML_LIB)/basis/basis.mlb\n" ^ - generatedN ^ "\n" ^ - driverN - - val compile_cmd = - File.bash_path (Path.variable ISABELLE_MLTON) ^ - " -default-type intinf " ^ File.bash_path ml_basis_path - val run_cmd = File.bash_path (Path.append path (Path.basic projectN)) + val cmd = "\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path in - {files = [(driver_path, driver), (ml_basis_path, ml_basis)], - compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + check_settings compiler ISABELLE_MLTON "MLton executable"; + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN); + compile compiler cmd; + evaluate compiler (File.bash_path (Path.append dir (Path.basic projectN))) end -fun evaluate_in_mlton ctxt = - evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt - (* driver for SML/NJ *) val smlnjN = "SMLNJ" val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" -fun mk_driver_smlnj _ path _ value_name = +fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir = let + val compiler = smlnjN val generatedN = "generated.sml" val driverN = "driver.sml" - val code_path = Path.append path (Path.basic generatedN) - val driver_path = Path.append path (Path.basic driverN) + val code_path = Path.append dir (Path.basic generatedN) + val driver_path = Path.append dir (Path.basic driverN) val driver = "structure Test = struct\n" ^ "fun main prog_name =\n" ^ @@ -427,30 +395,28 @@ "end;" val ml_source = "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^ - "use " ^ ML_Syntax.print_string (Bash.string (File.platform_path code_path)) ^ - "; use " ^ ML_Syntax.print_string (Bash.string (File.platform_path driver_path)) ^ + "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^ + "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^ "; Test.main ();" - val cmd = "echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"" in - {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} + check_settings compiler ISABELLE_SMLNJ "SMLNJ executable"; + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") end -fun evaluate_in_smlnj ctxt = - evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt - (* driver for OCaml *) val ocamlN = "OCaml" val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND" -fun mk_driver_ocaml _ path _ value_name = +fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir = let - val generatedN = "generated.ml" - val driverN = "driver.ml" + val compiler = ocamlN - val code_path = Path.append path (Path.basic generatedN) - val driver_path = Path.append path (Path.basic driverN) + val code_path = Path.append dir (Path.basic "generated.ml") + val driver_path = Path.append dir (Path.basic "driver.ml") val driver = "let format_term = function\n" ^ " | None -> \"\"\n" ^ @@ -464,22 +430,19 @@ " let _ = List.map (fun x -> print_string (format x)) result in\n" ^ " print_string \"" ^ end_markerN ^ "\";;\n" ^ "main ();;" - - val compiled_path = Path.append path (Path.basic "test") - val compile_cmd = + val compiled_path = Path.append dir (Path.basic "test") + val cmd = "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^ - " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^ + " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " \code_test_ghc\ (K "") -fun mk_driver_ghc ctxt path modules value_name = +fun evaluate_in_ghc ctxt (code_files, value_name) dir = let - val driverN = "Main.hs" + val compiler = ghcN + val modules = map fst code_files - fun mk_code_file name = Path.append path (Path.basic name) - val driver_path = Path.append path (Path.basic driverN) + val driver_path = Path.append dir (Path.basic "Main.hs") val driver = "module Main where {\n" ^ - String.concat (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ + implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^ "main = do {\n" ^ " let {\n" ^ " format_term Nothing = \"\";\n" ^ @@ -511,33 +474,34 @@ " }\n" ^ "}\n" - val compiled_path = Path.append path (Path.basic "test") - val compile_cmd = + val compiled_path = Path.append dir (Path.basic "test") + val cmd = "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ - Config.get ctxt ghc_options ^ " -o " ^ Bash.string (File.platform_path compiled_path) ^ " " ^ - Bash.string (File.platform_path driver_path) ^ " -i" ^ Bash.string (File.platform_path path) - - val run_cmd = File.bash_path compiled_path + Config.get ctxt ghc_options ^ " -o " ^ + File.bash_platform_path compiled_path ^ " " ^ + File.bash_platform_path driver_path ^ " -i" ^ + File.bash_platform_path dir in - {files = [(driver_path, driver)], - compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = mk_code_file} + check_settings compiler ISABELLE_GHC "GHC executable"; + List.app (fn (name, code) => File.write (Path.append dir (Path.basic name)) code) code_files; + File.write driver_path driver; + compile compiler cmd; + evaluate compiler (File.bash_path compiled_path) end -fun evaluate_in_ghc ctxt = - evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt - (* driver for Scala *) val scalaN = "Scala" -fun mk_driver_scala _ path _ value_name = +fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir = let + val compiler = scalaN val generatedN = "Generated_Code" val driverN = "Driver.scala" - val code_path = Path.append path (Path.basic (generatedN ^ ".scala")) - val driver_path = Path.append path (Path.basic driverN) + val code_path = Path.append dir (Path.basic (generatedN ^ ".scala")) + val driver_path = Path.append dir (Path.basic driverN) val driver = "import " ^ generatedN ^ "._\n" ^ "object Test {\n" ^ @@ -556,21 +520,18 @@ " print(\"" ^ end_markerN ^ "\");\n" ^ " }\n" ^ "}\n" - val compile_cmd = - "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ Bash.string (File.platform_path path) ^ - " -classpath " ^ Bash.string (File.platform_path path) ^ " " ^ - Bash.string (File.platform_path code_path) ^ " " ^ - Bash.string (File.platform_path driver_path) - - val run_cmd = "isabelle_scala scala -cp " ^ Bash.string (File.platform_path path) ^ " Test" + "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d " ^ File.bash_platform_path dir ^ + " -classpath " ^ File.bash_platform_path dir ^ " " ^ + File.bash_platform_path code_path ^ " " ^ File.bash_platform_path driver_path + val run_cmd = "isabelle_scala scala -cp " ^ File.bash_platform_path dir ^ " Test" in - {files = [(driver_path, driver)], - compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path} + List.app (File.write code_path o snd) code_files; + File.write driver_path driver; + compile compiler compile_cmd; + evaluate compiler run_cmd end -fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt - (* command setup *) @@ -583,7 +544,7 @@ val target_Scala = "Scala_eval" val target_Haskell = "Haskell_eval" -val _ = Theory.setup +val _ = Theory.setup (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)])) diff -r 7e90e1d178b5 -r ae89eac1d332 src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Sun Sep 20 21:09:40 2020 +0200 @@ -223,8 +223,7 @@ val object_file = tmp_file (module^".o") val _ = File.write module_file source val _ = - Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ - Bash.string (File.platform_path module_file)) + Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ File.bash_platform_path module_file) val _ = if not (File.exists object_file) then raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") @@ -310,8 +309,7 @@ val _ = File.write call_file call_source val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^ - Bash.string (File.platform_path module_file) ^ " " ^ - Bash.string (File.platform_path call_file)) + File.bash_platform_path module_file ^ " " ^ File.bash_platform_path call_file) val result = File.read result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')") val t' = parse_result arity_of result diff -r 7e90e1d178b5 -r ae89eac1d332 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Sep 20 21:09:40 2020 +0200 @@ -263,9 +263,9 @@ val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^ (space_implode " " - (map (Bash.string o File.platform_path) + (map File.bash_platform_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ - " -o " ^ Bash.string (File.platform_path executable) ^ ";" + " -o " ^ File.bash_platform_path executable ^ ";" val (_, compilation_time) = elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) val _ = Quickcheck.add_timing compilation_time current_result diff -r 7e90e1d178b5 -r ae89eac1d332 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Sun Sep 20 21:09:40 2020 +0200 @@ -50,7 +50,7 @@ fun make_command command options problem_path proof_path = Bash.strings (command () @ options) ^ " " ^ - Bash.string (File.platform_path problem_path) ^ + File.bash_platform_path problem_path ^ " > " ^ File.bash_path proof_path ^ " 2>&1" fun with_trace ctxt msg f x = diff -r 7e90e1d178b5 -r ae89eac1d332 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/Pure/General/file.ML Sun Sep 20 21:09:40 2020 +0200 @@ -10,6 +10,7 @@ val platform_path: Path.T -> string val bash_path: Path.T -> string val bash_paths: Path.T list -> string + val bash_platform_path: Path.T -> string val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool @@ -50,6 +51,8 @@ val bash_path = Bash_Syntax.string o standard_path; val bash_paths = Bash_Syntax.strings o map standard_path; +val bash_platform_path = Bash_Syntax.string o platform_path; + (* full_path *) diff -r 7e90e1d178b5 -r ae89eac1d332 src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML Sun Sep 20 15:45:25 2020 +0100 +++ b/src/Pure/Tools/ghc.ML Sun Sep 20 21:09:40 2020 +0200 @@ -85,7 +85,7 @@ val _ = File.write template_path (project_template {depends = depends, modules = modules}); val {rc, err, ...} = Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ Bash.string (File.platform_path template_path)); + " --bare " ^ File.bash_platform_path template_path); in if rc = 0 then () else error err end; end;