diff --git a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML +++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML @@ -1,153 +1,156 @@ (* Title: HOL/Tools/Nunchaku/nunchaku_tool.ML Author: Jasmin Blanchette, VU Amsterdam Copyright 2015, 2016, 2017 Interface to the external "nunchaku" tool. *) signature NUNCHAKU_TOOL = sig type ty = Nunchaku_Problem.ty type tm = Nunchaku_Problem.tm type nun_problem = Nunchaku_Problem.nun_problem type tool_params = {solvers: string list, overlord: bool, min_bound: int, max_bound: int option, bound_increment: int, debug: bool, specialize: bool, timeout: Time.time} type nun_solution = {tys: (ty * tm list) list, tms: (tm * tm) list} datatype nun_outcome = Unsat of string | Sat of string * string * nun_solution | Unknown of (string * string * nun_solution) option | Timeout | Nunchaku_Var_Not_Set | Nunchaku_Cannot_Execute | Nunchaku_Not_Found | CVC4_Cannot_Execute | CVC4_Not_Found | Unknown_Error of int * string val nunchaku_home_env_var: string val solve_nun_problem: tool_params -> nun_problem -> nun_outcome end; structure Nunchaku_Tool : NUNCHAKU_TOOL = struct open Nunchaku_Util; open Nunchaku_Problem; type tool_params = {solvers: string list, overlord: bool, min_bound: int, max_bound: int option, bound_increment: int, debug: bool, specialize: bool, timeout: Time.time}; type nun_solution = {tys: (ty * tm list) list, tms: (tm * tm) list}; datatype nun_outcome = Unsat of string | Sat of string * string * nun_solution | Unknown of (string * string * nun_solution) option | Timeout | Nunchaku_Var_Not_Set | Nunchaku_Cannot_Execute | Nunchaku_Not_Found | CVC4_Cannot_Execute | CVC4_Not_Found | Unknown_Error of int * string; val nunchaku_home_env_var = "NUNCHAKU_HOME"; val unknown_solver = "unknown"; val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome" (NONE : ((tool_params * nun_problem) * nun_outcome) option); fun uncached_solve_nun_problem ({solvers, overlord, min_bound, max_bound, bound_increment, specialize, timeout, ...} : tool_params) (problem as {sound, complete, ...}) = with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path => if getenv nunchaku_home_env_var = "" then Nunchaku_Var_Not_Set else let val bash_cmd = "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^ nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^ (if specialize then "" else "--no-specialize ") ^ "--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^ "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^ "--kodkod-min-bound " ^ string_of_int min_bound ^ " " ^ (case max_bound of NONE => "" | SOME n => "--kodkod-max-bound " ^ string_of_int n ^ " ") ^ "--kodkod-bound-increment " ^ string_of_int bound_increment ^ " " ^ File.bash_path prob_path; val comments = [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; val _ = File.write prob_path prob_str; - val {out, err, rc, ...} = Isabelle_System.bash_process bash_cmd; + val res = Isabelle_System.bash_process bash_cmd; + val rc = Process_Result.rc res; + val out = Process_Result.out res; + val err = Process_Result.err res; val backend = (case map_filter (try (unprefix "{backend:")) (split_lines out) of [s] => hd (space_explode "," s) | _ => unknown_solver); in if String.isPrefix "SAT" out then (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []}) else if String.isPrefix "UNSAT" out then if complete then Unsat backend else Unknown NONE else if String.isSubstring "TIMEOUT" out (* FIXME: temporary *) orelse String.isSubstring "kodkod failed (errcode 152)" err then Timeout else if String.isPrefix "UNKNOWN" out then Unknown NONE else if rc = 126 then Nunchaku_Cannot_Execute else if rc = 127 then Nunchaku_Not_Found else Unknown_Error (rc, simplify_spaces (elide_string 1000 (if err <> "" then err else out))) end); fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem = let val key = (params, problem) in (case (overlord orelse debug, AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of (false, SOME outcome) => outcome | _ => let val outcome = uncached_solve_nun_problem params problem; fun update_cache () = Synchronized.change cached_outcome (K (SOME (key, outcome))); in (case outcome of Unsat _ => update_cache () | Sat _ => update_cache () | Unknown _ => update_cache () | _ => ()); outcome end) end; end; diff --git a/src/Pure/General/exn.ML b/src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML +++ b/src/Pure/General/exn.ML @@ -1,129 +1,132 @@ (* Title: Pure/General/exn.ML Author: Makarius Support for exceptions. *) signature BASIC_EXN = sig exception ERROR of string val error: string -> 'a val cat_error: string -> string -> 'a end; signature EXN = sig include BASIC_EXN val polyml_location: exn -> PolyML.location option val reraise: exn -> 'a datatype 'a result = Res of 'a | Exn of exn val get_res: 'a result -> 'a option val get_exn: 'a result -> exn option val capture: ('a -> 'b) -> 'a -> 'b result val release: 'a result -> 'a val map_res: ('a -> 'b) -> 'a result -> 'b result val maps_res: ('a -> 'b result) -> 'a result -> 'b result val map_exn: (exn -> exn) -> 'a result -> 'a result exception Interrupt val interrupt: unit -> 'a val is_interrupt: exn -> bool val interrupt_exn: 'a result val is_interrupt_exn: 'a result -> bool val interruptible_capture: ('a -> 'b) -> 'a -> 'b result + val interrupt_return_code: int val return_code: exn -> int -> int val capture_exit: int -> ('a -> 'b) -> 'a -> 'b exception EXCEPTIONS of exn list val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a end; structure Exn: EXN = struct (* location *) val polyml_location = PolyML.Exception.exceptionLocation; val reraise = PolyML.Exception.reraise; (* user errors *) exception ERROR of string; fun error msg = raise ERROR msg; fun cat_error "" msg = error msg | cat_error msg "" = error msg | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2); (* exceptions as values *) datatype 'a result = Res of 'a | Exn of exn; fun get_res (Res x) = SOME x | get_res _ = NONE; fun get_exn (Exn exn) = SOME exn | get_exn _ = NONE; fun capture f x = Res (f x) handle e => Exn e; fun release (Res y) = y | release (Exn e) = reraise e; fun map_res f (Res x) = Res (f x) | map_res f (Exn e) = Exn e; fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f; fun map_exn f (Res x) = Res x | map_exn f (Exn e) = Exn (f e); (* interrupts *) exception Interrupt = Thread.Thread.Interrupt; fun interrupt () = raise Interrupt; fun is_interrupt Interrupt = true | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause | is_interrupt _ = false; val interrupt_exn = Exn Interrupt; fun is_interrupt_exn (Exn exn) = is_interrupt exn | is_interrupt_exn _ = false; fun interruptible_capture f x = Res (f x) handle e => if is_interrupt e then reraise e else Exn e; (* POSIX return code *) +val interrupt_return_code : int = 130; + fun return_code exn rc = - if is_interrupt exn then (130: int) else rc; + if is_interrupt exn then interrupt_return_code else rc; fun capture_exit rc f x = f x handle exn => exit (return_code exn rc); (* concatenated exceptions *) exception EXCEPTIONS of exn list; (* low-level trace *) fun trace exn_message output e = PolyML.Exception.traceException (e, fn (trace, exn) => let val title = "Exception trace - " ^ exn_message exn; val () = output (String.concatWith "\n" (title :: trace)); in reraise exn end); end; diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,357 +1,358 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; ML_file "ML/ml_pid.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; +ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala_compiler.ML"; ML_file "System/isabelle_tool.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/doc.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,172 +1,159 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig - type process_result = - {rc: int, - out_lines: string list, - err_lines: string list, - out: string, - err: string, - timing: Timing.timing} - val bash_process: string -> process_result + val bash_process: string -> Process_Result.T val bash_output_check: string -> string val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val rm_tree: Path.T -> unit val make_directory: Path.T -> Path.T val mkdir: Path.T -> unit val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> string end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) -type process_result = - {rc: int, - out_lines: string list, - err_lines: string list, - out: string, - err: string, - timing: Timing.timing}; - -fun bash_process script : process_result = +fun bash_process script = Scala.function_thread "bash_process" ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> space_explode "\000" |> (fn [] => raise Exn.Interrupt | [err] => error err | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); - val ((out, err), (out_lines, err_lines)) = - chop (Value.parse_int d) lines |> `(apply2 cat_lines); + val (out_lines, err_lines) = chop (Value.parse_int d) lines; in - {rc = rc, - out_lines = out_lines, - err_lines = err_lines, - out = out, - err = err, - timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} + Process_Result.make + {rc = rc, + out_lines = out_lines, + err_lines = err_lines, + timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end | _ => raise Fail "Malformed Isabelle/Scala result"); fun bash_output_check s = - (case bash_process s of - {rc = 0, out, ...} => trim_line out - | {err, ...} => error (trim_line err)); + let val res = bash_process s in + if Process_Result.ok res then trim_line (Process_Result.out res) + else error (trim_line (Process_Result.err res)) + end; fun bash_output s = let - val {out, err, rc, ...} = bash_process s; - val _ = warning (trim_line err); - in (out, rc) end; + val res = bash_process s; + val _ = warning (trim_line (Process_Result.err res)); + in (Process_Result.out res, Process_Result.rc res) end; fun bash s = let val (out, rc) = bash_output s; val _ = writeln (trim_line out); in rc end; (* bash functions *) fun bash_functions () = bash_output_check "declare -Fx" |> split_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory operations *) fun system_command cmd = if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); fun make_directory path = let val _ = if File.is_dir path then () else (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); in path end; fun mkdir path = if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); fun copy_dir src dst = if File.eq (src, dst) then () else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); fun copy_file src0 dst0 = let val src = Path.expand src0; val dst = Path.expand dst0; val target = if File.is_dir dst then dst + Path.base src else dst; in if File.eq (src, target) then () else ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) end; fun copy_file_base (base_dir, src0) target_dir = let val src = Path.expand src0; val src_dir = Path.dir src; val _ = if Path.starts_basic src then () else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); in copy_file (base_dir + src) (make_directory (target_dir + src_dir)) end; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun with_tmp_dir name f = let val path = create_tmp_path name "" in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; (* download file *) fun download url = with_tmp_file "download" "" (fn path => - ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path) - |> bash_process - |> (fn {rc = 0, ...} => File.read path - | {err, ...} => cat_error ("Failed to download " ^ quote url) err)); + let + val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path; + val res = bash_process s; + in + if Process_Result.ok res then File.read path + else cat_error ("Failed to download " ^ quote url) (Process_Result.err res) + end); end; diff --git a/src/Pure/System/process_result.ML b/src/Pure/System/process_result.ML new file mode 100644 --- /dev/null +++ b/src/Pure/System/process_result.ML @@ -0,0 +1,61 @@ +(* Title: Pure/System/process_result.scala + Author: Makarius + +Result of system process. +*) + +signature PROCESS_RESULT = +sig + type T + val make: + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} -> T + val rc: T -> int + val out_lines: T -> string list + val err_lines: T -> string list + val timing: T -> Timing.timing + val out: T -> string + val err: T -> string + val ok: T -> bool + val interrupted: T -> bool + val check_rc: (int -> bool) -> T -> T + val check: T -> T +end; + +structure Process_Result: PROCESS_RESULT = +struct + +abstype T = + Process_Result of + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} +with + +val make = Process_Result; +fun rep (Process_Result args) = args; + +val rc = #rc o rep; +val out_lines = #out_lines o rep; +val err_lines = #err_lines o rep; +val timing = #timing o rep; + +val out = cat_lines o out_lines; +val err = cat_lines o err_lines; + +fun ok result = rc result = 0; +fun interrupted result = rc result = Exn.interrupt_return_code; + +fun check_rc pred result = + if pred (rc result) then result + else if interrupted result then raise Exn.Interrupt + else error (err result); + +val check = check_rc (fn rc => rc = 0); + +end; + +end;