moved bash operations to Isabelle_System (cf. Scala version);
authorwenzelm
Sat Jul 16 20:52:41 2011 +0200 (2011-07-16)
changeset 438507f2cbc713344
parent 43849 00f4b305687d
child 43851 f7f8cf0a1536
moved bash operations to Isabelle_System (cf. Scala version);
src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
src/HOL/Matrix/Compute_Oracle/am_ghc.ML
src/HOL/Matrix/Cplex_tools.ML
src/HOL/Predicate_Compile_Examples/ROOT.ML
src/HOL/TPTP/atp_export.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/svc_funcs.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash_ops.ML
src/Pure/Concurrent/bash_sequential.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/System/isabelle_system.ML
src/Pure/Thy/present.ML
src/Tools/Code/code_target.ML
src/Tools/cache_io.ML
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 20:52:41 2011 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4      (* call solver *)
     1.5      val output_file = filename dir "sos_out"
     1.6      val (output, rv) =
     1.7 -      bash_output
     1.8 +      Isabelle_System.bash_output
     1.9         (if File.exists exe then
    1.10            space_implode " " (map File.shell_path [exe, input_file, output_file])
    1.11          else error ("Bad executable: " ^ File.platform_path exe))
     2.1 --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:14:58 2011 +0200
     2.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:52:41 2011 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4          val module_file = tmp_file (module^".hs")
     2.5          val object_file = tmp_file (module^".o")
     2.6          val _ = writeTextFile module_file source
     2.7 -        val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
     2.8 +        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
     2.9          val _ =
    2.10            if not (fileExists object_file) then
    2.11              raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    2.12 @@ -311,7 +311,7 @@
    2.13          val term = print_term arity_of 0 t
    2.14          val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
    2.15          val _ = writeTextFile call_file call_source
    2.16 -        val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    2.17 +        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    2.18          val result = readResultFile result_file handle IO.Io _ =>
    2.19            raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    2.20          val t' = parse_result arity_of result
     3.1 --- a/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:14:58 2011 +0200
     3.2 +++ b/src/HOL/Matrix/Cplex_tools.ML	Sat Jul 16 20:52:41 2011 +0200
     3.3 @@ -1141,7 +1141,7 @@
     3.4      val cplex_path = getenv "GLPK_PATH"
     3.5      val cplex = if cplex_path = "" then "glpsol" else cplex_path
     3.6      val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
     3.7 -    val answer = #1 (bash_output command)
     3.8 +    val answer = #1 (Isabelle_System.bash_output command)
     3.9      in
    3.10      let
    3.11          val result = load_glpkResult resultname
    3.12 @@ -1174,7 +1174,7 @@
    3.13      val cplex = if cplex_path = "" then "cplex" else cplex_path
    3.14      val _ = write_script scriptname lpname resultname
    3.15      val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
    3.16 -    val answer = "return code " ^ string_of_int (bash command)
    3.17 +    val answer = "return code " ^ string_of_int (Isabelle_System.bash command)
    3.18      in
    3.19      let
    3.20          val result = load_cplexResult resultname
     4.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sat Jul 16 20:14:58 2011 +0200
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Sat Jul 16 20:52:41 2011 +0200
     4.3 @@ -13,7 +13,8 @@
     4.4    (warning "No prolog system found - skipping some example theories"; ())
     4.5  else
     4.6    if not (getenv "ISABELLE_SWIPL" = "") orelse
     4.7 -    #1 (bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") = "5.10.1"
     4.8 +    #1 (Isabelle_System.bash_output "\"$ISABELLE_PREDICATE_COMPILE/lib/scripts/swipl_version\"") =
     4.9 +      "5.10.1"
    4.10    then
    4.11       (use_thys [
    4.12          "Code_Prolog_Examples",
     5.1 --- a/src/HOL/TPTP/atp_export.ML	Sat Jul 16 20:14:58 2011 +0200
     5.2 +++ b/src/HOL/TPTP/atp_export.ML	Sat Jul 16 20:52:41 2011 +0200
     5.3 @@ -122,7 +122,7 @@
     5.4        " " ^ arguments ctxt false "" (seconds 1.0) (K []) ^ " " ^
     5.5        File.shell_path prob_file
     5.6    in
     5.7 -    TimeLimit.timeLimit (seconds 0.3) bash_output command
     5.8 +    TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
     5.9      |> fst
    5.10      |> extract_tstplike_proof_and_outcome false true proof_delims
    5.11                                            known_failures
     6.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 16 20:14:58 2011 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 16 20:52:41 2011 +0200
     6.3 @@ -339,7 +339,7 @@
     6.4  val systems = Synchronized.var "atp_systems" ([] : string list)
     6.5  
     6.6  fun get_systems () =
     6.7 -  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     6.8 +  case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
     6.9      (output, 0) => split_lines output
    6.10    | (output, _) =>
    6.11      error (case extract_known_failure known_perl_failures output of
     7.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Jul 16 20:14:58 2011 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Jul 16 20:52:41 2011 +0200
     7.3 @@ -1034,7 +1034,7 @@
     7.4            val outcome =
     7.5              let
     7.6                val code =
     7.7 -                bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
     7.8 +                Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\
     7.9                        \\"$KODKODI\"/bin/kodkodi" ^
    7.10                        (if ms >= 0 then " -max-msecs " ^ string_of_int ms
    7.11                         else "") ^
     8.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 16 20:14:58 2011 +0200
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 16 20:52:41 2011 +0200
     8.3 @@ -792,7 +792,7 @@
     8.4    in
     8.5      if getenv env_var = "" then
     8.6        (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
     8.7 -    else fst (bash_output (cmd ^ File.shell_path file))
     8.8 +    else fst (Isabelle_System.bash_output (cmd ^ File.shell_path file))
     8.9    end
    8.10  
    8.11  
     9.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:14:58 2011 +0200
     9.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:52:41 2011 +0200
     9.3 @@ -253,9 +253,10 @@
     9.4          val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
     9.5            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
     9.6            " -o " ^ executable ^ ";"
     9.7 -        val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd) 
     9.8 +        val (result, compilation_time) =
     9.9 +          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    9.10          val _ = Quickcheck.add_timing compilation_time current_result
    9.11 -        val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    9.12 +        val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    9.13          fun with_size k =
    9.14            if k > size then
    9.15              (NONE, !current_result)
    9.16 @@ -264,7 +265,7 @@
    9.17                val _ = message ("Test data size: " ^ string_of_int k)
    9.18                val _ = current_size := k
    9.19                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    9.20 -                (fn () => bash_output (executable ^ " " ^ string_of_int k))
    9.21 +                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
    9.22                val _ = Quickcheck.add_timing timing current_result
    9.23              in
    9.24                if response = "NONE\n" then
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 16 20:14:58 2011 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Jul 16 20:52:41 2011 +0200
    10.3 @@ -682,7 +682,7 @@
    10.4                      upto conjecture_offset + length hyp_ts + 1
    10.5                    |> map single
    10.6                  val ((output, msecs), (atp_proof, outcome)) =
    10.7 -                  TimeLimit.timeLimit generous_slice_timeout bash_output command
    10.8 +                  TimeLimit.timeLimit generous_slice_timeout Isabelle_System.bash_output command
    10.9                    |>> (if overlord then
   10.10                           prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   10.11                         else
    11.1 --- a/src/HOL/Tools/sat_solver.ML	Sat Jul 16 20:14:58 2011 +0200
    11.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Jul 16 20:52:41 2011 +0200
    11.3 @@ -280,7 +280,7 @@
    11.4  (* ------------------------------------------------------------------------- *)
    11.5  
    11.6    fun make_external_solver cmd writefn readfn fm =
    11.7 -    (writefn fm; bash cmd; readfn ());
    11.8 +    (writefn fm; Isabelle_System.bash cmd; readfn ());
    11.9  
   11.10  (* ------------------------------------------------------------------------- *)
   11.11  (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
    12.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Jul 16 20:14:58 2011 +0200
    12.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Jul 16 20:52:41 2011 +0200
    12.3 @@ -64,7 +64,7 @@
    12.4        val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    12.5        val _ = File.write svc_input_file svc_input;
    12.6        val _ =
    12.7 -        bash_output (check_valid ^ " -dump-result " ^
    12.8 +        Isabelle_System.bash_output (check_valid ^ " -dump-result " ^
    12.9            File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
   12.10            ">/dev/null 2>&1")
   12.11        val svc_output =
    13.1 --- a/src/Pure/Concurrent/bash.ML	Sat Jul 16 20:14:58 2011 +0200
    13.2 +++ b/src/Pure/Concurrent/bash.ML	Sat Jul 16 20:52:41 2011 +0200
    13.3 @@ -4,7 +4,10 @@
    13.4  GNU bash processes, with propagation of interrupts.
    13.5  *)
    13.6  
    13.7 -val bash_process = uninterruptible (fn restore_attributes => fn script =>
    13.8 +structure Bash =
    13.9 +struct
   13.10 +
   13.11 +val process = uninterruptible (fn restore_attributes => fn script =>
   13.12    let
   13.13      datatype result = Wait | Signal | Result of int;
   13.14      val result = Synchronized.var "bash_result" Wait;
   13.15 @@ -83,3 +86,5 @@
   13.16      handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
   13.17    end);
   13.18  
   13.19 +end;
   13.20 +
    14.1 --- a/src/Pure/Concurrent/bash_ops.ML	Sat Jul 16 20:14:58 2011 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,15 +0,0 @@
    14.4 -(*  Title:      Pure/Concurrent/bash_ops.ML
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -Derived operations for bash_process.
    14.8 -*)
    14.9 -
   14.10 -fun bash_output s =
   14.11 -  let val {output, rc, ...} = bash_process s
   14.12 -  in (output, rc) end;
   14.13 -
   14.14 -fun bash s =
   14.15 -  (case bash_output s of
   14.16 -    ("", rc) => rc
   14.17 -  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
   14.18 -
    15.1 --- a/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:14:58 2011 +0200
    15.2 +++ b/src/Pure/Concurrent/bash_sequential.ML	Sat Jul 16 20:52:41 2011 +0200
    15.3 @@ -5,7 +5,10 @@
    15.4  could work via the controlling tty).
    15.5  *)
    15.6  
    15.7 -fun bash_process script =
    15.8 +structure Bash =
    15.9 +struct
   15.10 +
   15.11 +fun process script =
   15.12    let
   15.13      val id = serial_string ();
   15.14      val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
   15.15 @@ -32,3 +35,5 @@
   15.16      handle exn => (cleanup (); reraise exn)
   15.17    end;
   15.18  
   15.19 +end;
   15.20 +
    16.1 --- a/src/Pure/IsaMakefile	Sat Jul 16 20:14:58 2011 +0200
    16.2 +++ b/src/Pure/IsaMakefile	Sat Jul 16 20:52:41 2011 +0200
    16.3 @@ -53,7 +53,6 @@
    16.4  
    16.5  $(OUT)/Pure: $(BOOTSTRAP_FILES)				\
    16.6    Concurrent/bash.ML 					\
    16.7 -  Concurrent/bash_ops.ML				\
    16.8    Concurrent/bash_sequential.ML				\
    16.9    Concurrent/cache.ML					\
   16.10    Concurrent/future.ML					\
    17.1 --- a/src/Pure/ROOT.ML	Sat Jul 16 20:14:58 2011 +0200
    17.2 +++ b/src/Pure/ROOT.ML	Sat Jul 16 20:52:41 2011 +0200
    17.3 @@ -79,7 +79,6 @@
    17.4  if Multithreading.available
    17.5  then use "Concurrent/bash.ML"
    17.6  else use "Concurrent/bash_sequential.ML";
    17.7 -use "Concurrent/bash_ops.ML";
    17.8  
    17.9  use "Concurrent/mailbox.ML";
   17.10  use "Concurrent/task_queue.ML";
    18.1 --- a/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:14:58 2011 +0200
    18.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Jul 16 20:52:41 2011 +0200
    18.3 @@ -15,11 +15,25 @@
    18.4    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    18.5    val with_tmp_fifo: (Path.T -> 'a) -> 'a
    18.6    val bash_output_stream: string -> (TextIO.instream -> 'a) -> 'a
    18.7 +  val bash_output: string -> string * int
    18.8 +  val bash: string -> int
    18.9  end;
   18.10  
   18.11  structure Isabelle_System: ISABELLE_SYSTEM =
   18.12  struct
   18.13  
   18.14 +(* bash *)
   18.15 +
   18.16 +fun bash_output s =
   18.17 +  let val {output, rc, ...} = Bash.process s
   18.18 +  in (output, rc) end;
   18.19 +
   18.20 +fun bash s =
   18.21 +  (case bash_output s of
   18.22 +    ("", rc) => rc
   18.23 +  | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc));
   18.24 +
   18.25 +
   18.26  (* system commands *)
   18.27  
   18.28  fun isabelle_tool name args =
   18.29 @@ -72,6 +86,9 @@
   18.30      val _ = mkdirs path;
   18.31    in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
   18.32  
   18.33 +
   18.34 +(* process output stream *)
   18.35 +
   18.36  fun with_tmp_fifo f =
   18.37    with_tmp_file "isabelle-fifo-" ""
   18.38      (fn path =>
   18.39 @@ -79,13 +96,10 @@
   18.40          (_, 0) => f path
   18.41        | (out, _) => error (perhaps (try (unsuffix "\n")) out)));
   18.42  
   18.43 -
   18.44 -(* process output stream *)
   18.45 -
   18.46  fun bash_output_stream script f =
   18.47    with_tmp_fifo (fn fifo =>
   18.48      uninterruptible (fn restore_attributes => fn () =>
   18.49 -      (case bash_process (script ^ " > " ^ File.shell_path fifo ^ " &") of
   18.50 +      (case Bash.process (script ^ " > " ^ File.shell_path fifo ^ " &") of
   18.51          {rc = 0, terminate, ...} =>
   18.52            Exn.release
   18.53              (Exn.capture (restore_attributes (fn () => File.open_input f fifo)) ()
    19.1 --- a/src/Pure/Thy/present.ML	Sat Jul 16 20:14:58 2011 +0200
    19.2 +++ b/src/Pure/Thy/present.ML	Sat Jul 16 20:52:41 2011 +0200
    19.3 @@ -324,7 +324,7 @@
    19.4        \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
    19.5      val doc_path = Path.append result_path (Path.ext format (Path.basic name));
    19.6      val _ = if verbose then writeln s else ();
    19.7 -    val (out, rc) = bash_output s;
    19.8 +    val (out, rc) = Isabelle_System.bash_output s;
    19.9      val _ =
   19.10        if not (File.exists doc_path) orelse rc <> 0 then
   19.11          cat_error out ("Failed to build document " ^ quote (show_path doc_path))
    20.1 --- a/src/Tools/Code/code_target.ML	Sat Jul 16 20:14:58 2011 +0200
    20.2 +++ b/src/Tools/Code/code_target.ML	Sat Jul 16 20:52:41 2011 +0200
    20.3 @@ -403,11 +403,13 @@
    20.4          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    20.5            module_name args naming program names_cs);
    20.6          val cmd = make_command module_name;
    20.7 -      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    20.8 +      in
    20.9 +        if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   20.10          then error ("Code check failed for " ^ target ^ ": " ^ cmd)
   20.11          else ()
   20.12        end;
   20.13 -  in if getenv env_var = ""
   20.14 +  in
   20.15 +    if getenv env_var = ""
   20.16      then if strict
   20.17        then error (env_var ^ " not set; cannot check code for " ^ target)
   20.18        else warning (env_var ^ " not set; skipped checking code for " ^ target)
    21.1 --- a/src/Tools/cache_io.ML	Sat Jul 16 20:14:58 2011 +0200
    21.2 +++ b/src/Tools/cache_io.ML	Sat Jul 16 20:52:41 2011 +0200
    21.3 @@ -40,7 +40,7 @@
    21.4  fun raw_run make_cmd str in_path out_path =
    21.5    let
    21.6      val _ = File.write in_path str
    21.7 -    val (out2, rc) = bash_output (make_cmd in_path out_path)
    21.8 +    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
    21.9      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
   21.10    in {output=split_lines out2, redirected_output=out1, return_code=rc} end
   21.11