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,158 +1,153 @@ (* 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; -fun bash_output_error s = - let val {out, err, rc, ...} = Bash.process s in - ((out, err), rc) - end; - 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 ((output, error), code) = bash_output_error bash_cmd; + val {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd; val backend = (case map_filter (try (unprefix "{backend:")) (split_lines output) of [s] => hd (space_explode "," s) | _ => unknown_solver); in if String.isPrefix "SAT" output then (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []}) else if String.isPrefix "UNSAT" output then if complete then Unsat backend else Unknown NONE else if String.isSubstring "TIMEOUT" output (* FIXME: temporary *) orelse String.isSubstring "kodkod failed (errcode 152)" error then Timeout else if String.isPrefix "UNKNOWN" output then Unknown NONE else if code = 126 then Nunchaku_Cannot_Execute else if code = 127 then Nunchaku_Not_Found else Unknown_Error (code, simplify_spaces (elide_string 1000 (if error <> "" then error else output))) 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/file.ML b/src/Pure/General/file.ML --- a/src/Pure/General/file.ML +++ b/src/Pure/General/file.ML @@ -1,180 +1,180 @@ (* Title: Pure/General/file.ML Author: Makarius File-system operations. *) signature FILE = sig val standard_path: Path.T -> string 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 val rm: Path.T -> unit val is_dir: Path.T -> bool val is_file: Path.T -> bool val check_dir: Path.T -> Path.T val check_file: Path.T -> Path.T val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_dir: Path.T -> string list val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_lines: Path.T -> string list val read_pages: Path.T -> string list val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit val write_buffer: Path.T -> Buffer.T -> unit val eq: Path.T * Path.T -> bool end; structure File: FILE = struct (* system path representations *) val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; -val bash_path = Bash_Syntax.string o standard_path; -val bash_paths = Bash_Syntax.strings o map standard_path; +val bash_path = Bash.string o standard_path; +val bash_paths = Bash.strings o map standard_path; -val bash_platform_path = Bash_Syntax.string o platform_path; +val bash_platform_path = Bash.string o platform_path; (* full_path *) fun full_path dir path = let val path' = Path.expand path; val _ = Path.is_current path' andalso error "Bad file specification"; val path'' = dir + path'; in if Path.is_absolute path'' then path'' else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path'' end; (* tmp_path *) fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path; (* directory entries *) val exists = can OS.FileSys.modTime o platform_path; val rm = OS.FileSys.remove o platform_path; fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); fun is_dir path = exists path andalso test_dir path; fun is_file path = exists path andalso not (test_dir path); fun check_dir path = if is_dir path then path else error ("No such directory: " ^ Path.print (Path.expand path)); fun check_file path = if is_file path then path else error ("No such file: " ^ Path.print (Path.expand path)); (* open streams *) local fun with_file open_file close_file f = Thread_Attributes.uninterruptible (fn restore_attributes => fn path => let val file = open_file path; val result = Exn.capture (restore_attributes f) file; in close_file file; Exn.release result end); in fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; end; (* directory content *) fun fold_dir f path a = check_dir path |> open_dir (fn stream => let fun read x = (case OS.FileSys.readDir stream of NONE => x | SOME entry => read (f entry x)); in read a end); fun read_dir path = sort_strings (fold_dir cons path []); (* input *) (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine . optional terminator at end-of-input *) fun fold_chunks terminator f path a = open_input (fn file => let fun read buf x = (case Byte.bytesToString (BinIO.input file) of "" => (case Buffer.content buf of "" => x | line => f line x) | input => (case String.fields (fn c => c = terminator) input of [rest] => read (Buffer.add rest buf) x | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x))) and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x | read_lines (line :: more) x = read_lines more (f line x); in read Buffer.empty a end) path; fun fold_lines f = fold_chunks #"\n" f; fun fold_pages f = fold_chunks #"\f" f; fun read_lines path = rev (fold_lines cons path []); fun read_pages path = rev (fold_pages cons path []); val read = open_input (Byte.bytesToString o BinIO.inputAll); (* output *) fun output file txt = BinIO.output (file, Byte.stringToBytes txt); fun output_list txts file = List.app (output file) txts; fun write_list path txts = open_output (output_list txts) path; fun append_list path txts = open_append (output_list txts) path; fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (Buffer.output buf o output) path; (* eq *) fun eq paths = (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); 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,356 @@ (* 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_syntax.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/bash.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/bash.ML b/src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML +++ b/src/Pure/System/bash.ML @@ -1,36 +1,35 @@ (* Title: Pure/System/bash.ML Author: Makarius -GNU bash processes, with propagation of interrupts -- POSIX version. +Syntax for GNU bash. *) signature BASH = sig val string: string -> string val strings: string list -> string - val process: string -> {out: string, err: string, rc: int} end; structure Bash: BASH = struct -val string = Bash_Syntax.string; -val strings = Bash_Syntax.strings; +fun string "" = "\"\"" + | string str = + str |> translate_string (fn ch => + let val c = ord ch in + (case ch of + "\t" => "$'\\t'" + | "\n" => "$'\\n'" + | "\f" => "$'\\f'" + | "\r" => "$'\\r'" + | _ => + if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse + exists_string (fn c => c = ch) "+,-./:_" then ch + else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" + else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" + else "\\" ^ ch) + end); -fun process script = - Scala.function_thread "bash_process" - ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) - |> YXML.parse_body - |> - let open XML.Decode in - variant - [fn ([], []) => raise Exn.Interrupt, - fn ([], a) => error (YXML.string_of_body a), - fn ([a], c) => - let - val rc = int_atom a; - val (out, err) = pair I I c |> apply2 YXML.string_of_body; - in {out = out, err = err, rc = rc} end] - end; +val strings = space_implode " " o map string; end; diff --git a/src/Pure/System/bash_syntax.ML b/src/Pure/System/bash_syntax.ML deleted file mode 100644 --- a/src/Pure/System/bash_syntax.ML +++ /dev/null @@ -1,35 +0,0 @@ -(* Title: Pure/System/bash_syntax.ML - Author: Makarius - -Syntax for GNU bash (see also Pure/System/bash.ML). -*) - -signature BASH_SYNTAX = -sig - val string: string -> string - val strings: string list -> string -end; - -structure Bash_Syntax: BASH_SYNTAX = -struct - -fun string "" = "\"\"" - | string str = - str |> translate_string (fn ch => - let val c = ord ch in - (case ch of - "\t" => "$'\\t'" - | "\n" => "$'\\n'" - | "\f" => "$'\\f'" - | "\r" => "$'\\r'" - | _ => - if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse - exists_string (fn c => c = ch) "+,-./:_" then ch - else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" - else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" - else "\\" ^ ch) - end); - -val strings = space_implode " " o map string; - -end; 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,134 +1,151 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig + val bash_process: string -> {out: string, err: string, rc: int} 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 *) +fun bash_process script = + Scala.function_thread "bash_process" + ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) + |> YXML.parse_body + |> + let open XML.Decode in + variant + [fn ([], []) => raise Exn.Interrupt, + fn ([], a) => error (YXML.string_of_body a), + fn ([a], c) => + let + val rc = int_atom a; + val (out, err) = pair I I c |> apply2 YXML.string_of_body; + in {out = out, err = err, rc = rc} end] + end; + fun bash_output_check s = - (case Bash.process s of + (case bash_process s of {rc = 0, out, ...} => trim_line out | {err, ...} => error (trim_line err)); fun bash_output s = let - val {out, err, rc, ...} = Bash.process s; + val {out, err, rc, ...} = bash_process s; val _ = warning (trim_line err); in (out, rc) 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 + |> bash_process |> (fn {rc = 0, ...} => File.read path | {err, ...} => cat_error ("Failed to download " ^ quote url) err)); end; diff --git a/src/Pure/Tools/ghc.ML b/src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML +++ b/src/Pure/Tools/ghc.ML @@ -1,91 +1,92 @@ (* Title: Pure/Tools/ghc.ML Author: Makarius Support for GHC: Glasgow Haskell Compiler. *) signature GHC = sig val print_codepoint: UTF8.codepoint -> string val print_symbol: Symbol.symbol -> string val print_string: string -> string val project_template: {depends: string list, modules: string list} -> string val new_project: Path.T -> {name: string, depends: string list, modules: string list} -> unit end; structure GHC: GHC = struct (** string literals **) fun print_codepoint c = (case c of 34 => "\\\"" | 39 => "\\'" | 92 => "\\\\" | 7 => "\\a" | 8 => "\\b" | 9 => "\\t" | 10 => "\\n" | 11 => "\\v" | 12 => "\\f" | 13 => "\\r" | c => if c >= 32 andalso c < 127 then chr c else "\\" ^ string_of_int c ^ "\\&"); fun print_symbol sym = (case Symbol.decode sym of Symbol.Char s => print_codepoint (ord s) | Symbol.UTF8 s => UTF8.decode_permissive s |> map print_codepoint |> implode | Symbol.Sym s => "\\092<" ^ s ^ ">" | Symbol.Control s => "\\092<^" ^ s ^ ">" | _ => translate_string (print_codepoint o ord) sym); val print_string = quote o implode o map print_symbol o Symbol.explode; (** project setup **) fun project_template {depends, modules} = \<^verbatim>\{-# START_FILE {{name}}.cabal #-} name: {{name}} version: 0.1.0.0 homepage: default license: BSD3 author: default maintainer: default category: default build-type: Simple cabal-version: >=1.10 executable {{name}} hs-source-dirs: src main-is: Main.hs default-language: Haskell2010 build-depends: \ ^ commas ("base >= 4.7 && < 5" :: depends) ^ \<^verbatim>\ other-modules: \ ^ commas modules ^ \<^verbatim>\ {-# START_FILE Setup.hs #-} import Distribution.Simple main = defaultMain {-# START_FILE src/Main.hs #-} module Main where main :: IO () main = return () \; fun new_project dir {name, depends, modules} = let val template_path = dir + (Path.basic name |> Path.ext "hsfiles"); 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 " ^ File.bash_platform_path template_path); + Isabelle_System.bash_process + ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ + " --bare " ^ File.bash_platform_path template_path); in if rc = 0 then () else error err end; end;