moved bash operations to Isabelle_System (cf. Scala version);
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Sat Jul 16 20:52:41 2011 +0200
@@ -50,7 +50,7 @@
(* call solver *)
val output_file = filename dir "sos_out"
val (output, rv) =
- bash_output
+ Isabelle_System.bash_output
(if File.exists exe then
space_implode " " (map File.shell_path [exe, input_file, output_file])
else error ("Bad executable: " ^ File.platform_path exe))
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sat Jul 16 20:52:41 2011 +0200
@@ -227,7 +227,7 @@
val module_file = tmp_file (module^".hs")
val object_file = tmp_file (module^".o")
val _ = writeTextFile module_file source
- val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
+ val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
val _ =
if not (fileExists object_file) then
raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -311,7 +311,7 @@
val term = print_term arity_of 0 t
val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
val _ = writeTextFile call_file call_source
- val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
+ val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
val result = readResultFile result_file handle IO.Io _ =>
raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
val t' = parse_result arity_of result
--- a/src/HOL/Matrix/Cplex_tools.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Matrix/Cplex_tools.ML Sat Jul 16 20:52:41 2011 +0200
@@ -1141,7 +1141,7 @@
val cplex_path = getenv "GLPK_PATH"
val cplex = if cplex_path = "" then "glpsol" else cplex_path
val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
- val answer = #1 (bash_output command)
+ val answer = #1 (Isabelle_System.bash_output command)
in
let
val result = load_glpkResult resultname
@@ -1174,7 +1174,7 @@
val cplex = if cplex_path = "" then "cplex" else cplex_path
val _ = write_script scriptname lpname resultname
val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
- val answer = "return code " ^ string_of_int (bash command)
+ val answer = "return code " ^ string_of_int (Isabelle_System.bash command)
in
let
val result = load_cplexResult resultname
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Sat Jul 16 20:52:41 2011 +0200
@@ -13,7 +13,8 @@
(warning "No prolog system found - skipping some example theories"; ())
else
if not (getenv "ISABELLE_SWIPL" = "") orelse
- #1 (bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = "5.10.1"
+ #1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") =
+ "5.10.1"
then
(use_thys [
"Code_Prolog_Examples",
--- a/src/HOL/TPTP/atp_export.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Sat Jul 16 20:52:41 2011 +0200
@@ -122,7 +122,7 @@
" " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
File.shell_path prob_file
in
- TimeLimit.timeLimit (seconds 0.3) bash_output command
+ TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
|> fst
|> extract_tstplike_proof_and_outcome false true proof_delims
known_failures
--- a/src/HOL/Tools/ATP/atp_systems.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Jul 16 20:52:41 2011 +0200
@@ -339,7 +339,7 @@
val systems = Synchronized.var "atp_systems" ([] : string list)
fun get_systems () =
- case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
+ case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
(output, 0) => split_lines output
| (output, _) =>
error (case extract_known_failure known_perl_failures output of
--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Jul 16 20:52:41 2011 +0200
@@ -1034,7 +1034,7 @@
val outcome =
let
val code =
- bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
+ Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
\\"$KODKODI\"/bin/kodkodi" ^
(if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sat Jul 16 20:52:41 2011 +0200
@@ -792,7 +792,7 @@
in
if getenv env_var = "" then
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
- else fst (bash_output (cmd ^ File.shell_path file))
+ else fst (Isabelle_System.bash_output (cmd ^ File.shell_path file))
end
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Jul 16 20:52:41 2011 +0200
@@ -253,9 +253,10 @@
val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
" -o " ^ executable ^ ";"
- val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd)
+ val (result, compilation_time) =
+ elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
val _ = Quickcheck.add_timing compilation_time current_result
- val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
+ val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
fun with_size k =
if k > size then
(NONE, !current_result)
@@ -264,7 +265,7 @@
val _ = message ("Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
- (fn () => bash_output (executable ^ " " ^ string_of_int k))
+ (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
val _ = Quickcheck.add_timing timing current_result
in
if response = "NONE\n" then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Jul 16 20:52:41 2011 +0200
@@ -682,7 +682,7 @@
upto conjecture_offset + length hyp_ts + 1
|> map single
val ((output, msecs), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout bash_output command
+ TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
|>> (if overlord then
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
--- a/src/HOL/Tools/sat_solver.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sat Jul 16 20:52:41 2011 +0200
@@ -280,7 +280,7 @@
(* ------------------------------------------------------------------------- *)
fun make_external_solver cmd writefn readfn fm =
- (writefn fm; bash cmd; readfn ());
+ (writefn fm; Isabelle_System.bash cmd; readfn ());
(* ------------------------------------------------------------------------- *)
(* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
--- a/src/HOL/ex/svc_funcs.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/HOL/ex/svc_funcs.ML Sat Jul 16 20:52:41 2011 +0200
@@ -64,7 +64,7 @@
val svc_output_file = File.tmp_path (Path.basic "SVM_out");
val _ = File.write svc_input_file svc_input;
val _ =
- bash_output (check_valid ^ " -dump-result " ^
+ Isabelle_System.bash_output (check_valid ^ " -dump-result " ^
File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
">/dev/null 2>&1")
val svc_output =
--- a/src/Pure/Concurrent/bash.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML Sat Jul 16 20:52:41 2011 +0200
@@ -4,7 +4,10 @@
GNU bash processes, with propagation of interrupts.
*)
-val bash_process = uninterruptible (fn restore_attributes => fn script =>
+structure Bash =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
@@ -83,3 +86,5 @@
handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
end);
+end;
+
--- a/src/Pure/Concurrent/bash_ops.ML Sat Jul 16 20:14:58 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/Concurrent/bash_ops.ML
- Author: Makarius
-
-Derived operations for bash_process.
-*)
-
-fun bash_output s =
- let val {output, rc, ...} = bash_process s
- in (output, rc) end;
-
-fun bash s =
- (case bash_output s of
- ("", rc) => rc
- | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
-
--- a/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 20:52:41 2011 +0200
@@ -5,7 +5,10 @@
could work via the controlling tty).
*)
-fun bash_process script =
+structure Bash =
+struct
+
+fun process script =
let
val id = serial_string ();
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
@@ -32,3 +35,5 @@
handle exn => (cleanup (); reraise exn)
end;
+end;
+
--- a/src/Pure/IsaMakefile Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/IsaMakefile Sat Jul 16 20:52:41 2011 +0200
@@ -53,7 +53,6 @@
$(OUT)/Pure: $(BOOTSTRAP_FILES) \
Concurrent/bash.ML \
- Concurrent/bash_ops.ML \
Concurrent/bash_sequential.ML \
Concurrent/cache.ML \
Concurrent/future.ML \
--- a/src/Pure/ROOT.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/ROOT.ML Sat Jul 16 20:52:41 2011 +0200
@@ -79,7 +79,6 @@
if Multithreading.available
then use "Concurrent/bash.ML"
else use "Concurrent/bash_sequential.ML";
-use "Concurrent/bash_ops.ML";
use "Concurrent/mailbox.ML";
use "Concurrent/task_queue.ML";
--- a/src/Pure/System/isabelle_system.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/System/isabelle_system.ML Sat Jul 16 20:52:41 2011 +0200
@@ -15,11 +15,25 @@
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
val with_tmp_fifo: (Path.T -> 'a) -> 'a
val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
+ val bash_output: string -> string * int
+ val bash: string -> int
end;
structure Isabelle_System: ISABELLE_SYSTEM =
struct
+(* bash *)
+
+fun bash_output s =
+ let val {output, rc, ...} = Bash.process s
+ in (output, rc) end;
+
+fun bash s =
+ (case bash_output s of
+ ("", rc) => rc
+ | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
+
+
(* system commands *)
fun isabelle_tool name args =
@@ -72,6 +86,9 @@
val _ = mkdirs path;
in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
+
+(* process output stream *)
+
fun with_tmp_fifo f =
with_tmp_file "isabelle-fifo-" ""
(fn path =>
@@ -79,13 +96,10 @@
(_, 0) => f path
| (out, _) => error (perhaps (try (unsuffix "\n")) out)));
-
-(* process output stream *)
-
fun bash_output_stream script f =
with_tmp_fifo (fn fifo =>
uninterruptible (fn restore_attributes => fn () =>
- (case bash_process (script ^ " > " ^ File.shell_path fifo ^ " &") of
+ (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
{rc = 0, terminate, ...} =>
Exn.release
(Exn.capture (restore_attributes (fn () => File.open_input f fifo)) ()
--- a/src/Pure/Thy/present.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Pure/Thy/present.ML Sat Jul 16 20:52:41 2011 +0200
@@ -324,7 +324,7 @@
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
val doc_path = Path.append result_path (Path.ext format (Path.basic name));
val _ = if verbose then writeln s else ();
- val (out, rc) = bash_output s;
+ val (out, rc) = Isabelle_System.bash_output s;
val _ =
if not (File.exists doc_path) orelse rc <> 0 then
cat_error out ("Failed to build document " ^ quote (show_path doc_path))
--- a/src/Tools/Code/code_target.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Tools/Code/code_target.ML Sat Jul 16 20:52:41 2011 +0200
@@ -403,11 +403,13 @@
val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
module_name args naming program names_cs);
val cmd = make_command module_name;
- in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+ in
+ if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target ^ ": " ^ cmd)
else ()
end;
- in if getenv env_var = ""
+ in
+ if getenv env_var = ""
then if strict
then error (env_var ^ " not set; cannot check code for " ^ target)
else warning (env_var ^ " not set; skipped checking code for " ^ target)
--- a/src/Tools/cache_io.ML Sat Jul 16 20:14:58 2011 +0200
+++ b/src/Tools/cache_io.ML Sat Jul 16 20:52:41 2011 +0200
@@ -40,7 +40,7 @@
fun raw_run make_cmd str in_path out_path =
let
val _ = File.write in_path str
- val (out2, rc) = bash_output (make_cmd in_path out_path)
+ val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
in {output=split_lines out2, redirected_output=out1, return_code=rc} end