# HG changeset patch # User wenzelm # Date 1621111147 -7200 # Node ID c74e25de3c0092ab5e69d4f52900ca6412414995 # Parent 60a7884676399cdfa78d031f42cf8d1564b7e774# Parent 3d0952893db8897068975dda7b14a6708f9495e8 merged diff -r 60a788467639 -r c74e25de3c00 etc/components --- a/etc/components Fri May 14 12:43:19 2021 +0100 +++ b/etc/components Sat May 15 22:39:07 2021 +0200 @@ -2,7 +2,6 @@ src/Tools/jEdit src/Tools/Graphview src/Tools/VSCode -src/HOL/Mirabelle src/HOL/Mutabelle src/HOL/Library/Sum_of_Squares src/HOL/SPARK diff -r 60a788467639 -r c74e25de3c00 etc/options --- a/etc/options Fri May 14 12:43:19 2021 +0100 +++ b/etc/options Sat May 15 22:39:07 2021 +0200 @@ -83,6 +83,8 @@ -- "level of parallel proof checking: 0, 1, 2" option parallel_subproofs_threshold : real = 0.01 -- "lower bound of timing estimate for forked nested proofs (seconds)" +option parallel_presentation : bool = true + -- "parallel theory presentation" option command_timing_threshold : real = 0.1 -- "default threshold for persistent command timing (seconds)" diff -r 60a788467639 -r c74e25de3c00 src/HOL/Main.thy --- a/src/HOL/Main.thy Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/Main.thy Sat May 15 22:39:07 2021 +0200 @@ -9,6 +9,7 @@ imports Predicate_Compile Quickcheck_Narrowing + Mirabelle Extraction Nunchaku BNF_Greatest_Fixpoint diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle.thy Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,18 @@ +(* Title: HOL/Mirabelle.thy + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius +*) + +theory Mirabelle + imports Sledgehammer Predicate_Compile +begin + +ML_file \Tools/Mirabelle/mirabelle.ML\ +ML_file \Tools/Mirabelle/mirabelle_arith.ML\ +ML_file \Tools/Mirabelle/mirabelle_metis.ML\ +ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ +ML_file \Tools/Mirabelle/mirabelle_sledgehammer.ML\ +ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ +ML_file \Tools/Mirabelle/mirabelle_try0.ML\ + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/Mirabelle/Mirabelle.thy - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -theory Mirabelle -imports Main -begin - -ML_file \Tools/mirabelle.ML\ -ML_file \../TPTP/sledgehammer_tactics.ML\ - -ML \Toplevel.add_hook Mirabelle.step_hook\ - -ML \ -signature MIRABELLE_ACTION = -sig - val invoke : (string * string) list -> theory -> theory -end -\ - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Mirabelle_Test.thy --- a/src/HOL/Mirabelle/Mirabelle_Test.thy Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: HOL/Mirabelle/Mirabelle_Test.thy - Author: Sascha Boehme, TU Munich -*) - -section \Simple test theory for Mirabelle actions\ - -theory Mirabelle_Test -imports Main Mirabelle -begin - -ML_file \Tools/mirabelle_arith.ML\ -ML_file \Tools/mirabelle_metis.ML\ -ML_file \Tools/mirabelle_quickcheck.ML\ -ML_file \Tools/mirabelle_refute.ML\ -ML_file \Tools/mirabelle_sledgehammer.ML\ -ML_file \Tools/mirabelle_sledgehammer_filter.ML\ -ML_file \Tools/mirabelle_try0.ML\ - -text \ - Only perform type-checking of the actions, - any reasonable test would be too complicated. -\ - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -signature MIRABELLE = -sig - (*configuration*) - val logfile : string Config.T - val timeout : int Config.T - val start_line : int Config.T - val end_line : int Config.T - - (*core*) - type init_action = int -> theory -> theory - type done_args = {last: Toplevel.state, log: string -> unit} - type done_action = int -> done_args -> unit - type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} - type run_action = int -> run_args -> unit - type action = init_action * run_action * done_action - val catch : (int -> string) -> run_action -> run_action - val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> - int -> run_args -> 'a - val register : action -> theory -> theory - val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> - unit - - (*utility functions*) - val can_apply : Time.time -> (Proof.context -> int -> tactic) -> - Proof.state -> bool - val theorems_in_proof_term : theory -> thm -> thm list - val theorems_of_sucessful_proof : Toplevel.state option -> thm list - val get_setting : (string * string) list -> string * string -> string - val get_int_setting : (string * string) list -> string * int -> int - val get_bool_setting : (string * string) list -> string * bool -> bool - val cpu_time : ('a -> 'b) -> 'a -> 'b * int -end - - - -structure Mirabelle : MIRABELLE = -struct - -(* Mirabelle configuration *) - -val logfile = Attrib.setup_config_string \<^binding>\mirabelle_logfile\ (K "") -val timeout = Attrib.setup_config_int \<^binding>\mirabelle_timeout\ (K 30) -val start_line = Attrib.setup_config_int \<^binding>\mirabelle_start_line\ (K 0) -val end_line = Attrib.setup_config_int \<^binding>\mirabelle_end_line\ (K ~1) - - -(* Mirabelle core *) - -type init_action = int -> theory -> theory -type done_args = {last: Toplevel.state, log: string -> unit} -type done_action = int -> done_args -> unit -type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T, name: string} -type run_action = int -> run_args -> unit -type action = init_action * run_action * done_action - -structure Actions = Theory_Data -( - type T = (int * run_action * done_action) list - val empty = [] - val extend = I - fun merge data = Library.merge (K true) data (* FIXME potential data loss because of (K true) *) -) - - -fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e) - -fun catch tag f id (st as {log, ...}: run_args) = (f id st; ()) - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ()) - -fun catch_result tag d f id (st as {log, ...}: run_args) = f id st - handle exn => - if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d) - -fun register (init, run, done) thy = - let val id = length (Actions.get thy) + 1 - in - thy - |> init id - |> Actions.map (cons (id, run, done)) - end - -local - -fun log thy s = - let fun append_to n = if n = "" then K () else File.append (Path.explode n) - in append_to (Config.get_global thy logfile) (s ^ "\n") end - (* FIXME: with multithreading and parallel proofs enabled, we might need to - encapsulate this inside a critical section *) - -fun log_sep thy = log thy "------------------" - -fun apply_actions thy pos name info (pre, post, time) actions = - let - fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} - fun run (id, run, _) = (apply (run id); log_sep thy) - in (log thy info; log_sep thy; List.app run actions) end - -fun in_range _ _ NONE = true - | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) - -fun only_within_range thy pos f x = - let val l = Config.get_global thy start_line and r = Config.get_global thy end_line - in if in_range l r (Position.line_of pos) then f x else () end - -in - -fun run_actions tr pre post = - let - val thy = Proof.theory_of pre - val pos = Toplevel.pos_of tr - val name = Toplevel.name_of tr - val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout)) - - val str0 = string_of_int o the_default 0 - val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) - val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" - in - only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) - end - -fun done_actions st = - let - val thy = Toplevel.theory_of st - val _ = log thy "\n\n"; - in - thy - |> Actions.get - |> List.app (fn (id, _, done) => done id {last=st, log=log thy}) - end - -end - -val whitelist = ["apply", "by", "proof"] - -fun step_hook tr pre post = - (* FIXME: might require wrapping into "interruptible" *) - if can (Proof.assert_backward o Toplevel.proof_of) pre andalso - member (op =) whitelist (Toplevel.name_of tr) - then run_actions tr (Toplevel.proof_of pre) (SOME post) - else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post - then done_actions pre - else () (* FIXME: add theory_hook here *) - - - -(* Mirabelle utility functions *) - -fun can_apply time tac st = - let - val {context = ctxt, facts, goal} = Proof.goal st - val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt) - in - (case try (Timeout.apply time (Seq.pull o full_tac)) goal of - SOME (SOME _) => true - | _ => false) - end - -local - -fun fold_body_thms f = - let - fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => - fn (x, seen) => - if Inttab.defined seen i then (x, seen) - else - let - val name = Proofterm.thm_node_name thm_node - val prop = Proofterm.thm_node_prop thm_node - val body = Future.join (Proofterm.thm_node_body thm_node) - val (x', seen') = app (n + (if name = "" then 0 else 1)) body - (x, Inttab.update (i, ()) seen) - in (x' |> n = 0 ? f (name, prop, body), seen') end) - in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end - -in - -fun theorems_in_proof_term thy thm = - let - val all_thms = Global_Theory.all_thms_of thy true - fun collect (s, _, _) = if s <> "" then insert (op =) s else I - fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE - fun resolve_thms names = map_filter (member_of names) all_thms - in - resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) - end - -end - -fun theorems_of_sucessful_proof state = - (case state of - NONE => [] - | SOME st => - if not (Toplevel.is_proof st) then [] - else - theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st)))) - -fun get_setting settings (key, default) = - the_default default (AList.lookup (op =) settings key) - -fun get_int_setting settings (key, default) = - (case Option.map Int.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | SOME NONE => error ("bad option: " ^ key) - | NONE => default) - -fun get_bool_setting settings (key, default) = - (case Option.map Bool.fromString (AList.lookup (op =) settings key) of - SOME (SOME i) => i - | SOME NONE => error ("bad option: " ^ key) - | NONE => default) - -fun cpu_time f x = - let val ({cpu, ...}, y) = Timing.timing f x - in (y, Time.toMilliseconds cpu) end - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_arith.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Arith : MIRABELLE_ACTION = -struct - -fun arith_tag id = "#" ^ string_of_int id ^ " arith: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then log (arith_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Metis : MIRABELLE_ACTION = -struct - -fun metis_tag id = "#" ^ string_of_int id ^ " metis: " - -fun init _ = I -fun done _ _ = () - -fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = - let - val thms = Mirabelle.theorems_of_sucessful_proof post - val names = map Thm.get_name_hint thms - val add_info = if null names then I else suffix (":\n" ^ commas names) - - val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))) - - fun metis ctxt = - Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt - (thms @ facts) - in - (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") - |> prefix (metis_tag id) - |> add_info - |> log - end - handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout") - | ERROR msg => log (metis_tag id ^ "error: " ^ msg) - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Quickcheck : MIRABELLE_ACTION = -struct - -fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: " - -fun init _ = I -fun done _ _ = () - -fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) = - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst - val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1 - in - (case Timeout.apply timeout quickcheck pre of - NONE => log (qc_tag id ^ "no counterexample") - | SOME _ => log (qc_tag id ^ "counterexample found")) - end - handle Timeout.TIMEOUT _ => log (qc_tag id ^ "timeout") - | ERROR msg => log (qc_tag id ^ "error: " ^ msg) - -fun invoke args = - Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_refute.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_refute.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich -*) - -structure Mirabelle_Refute : MIRABELLE_ACTION = -struct - - -(* FIXME: -fun refute_action args timeout {pre=st, ...} = - let - val subgoal = 1 - val thy = Proof.theory_of st - val thm = #goal (Proof.raw_goal st) - - val refute = Refute.refute_goal thy args thm - val _ = Timeout.apply timeout refute subgoal - in - val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) - val warn_log = Substring.full (the (Symtab.lookup tab "warning")) - - val r = - if Substring.isSubstring "model found" writ_log - then - if Substring.isSubstring "spurious" warn_log - then SOME "potential counterexample" - else SOME "real counterexample (bug?)" - else - if Substring.isSubstring "time limit" writ_log - then SOME "no counterexample (timeout)" - else if Substring.isSubstring "Search terminated" writ_log - then SOME "no counterexample (normal termination)" - else SOME "no counterexample (unknown)" - in r end -*) - -fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,658 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich -*) - -structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = -struct - -(*To facilitate synching the description of Mirabelle Sledgehammer parameters - (in ../lib/Tools/mirabelle) with the parameters actually used by this - interface, the former extracts PARAMETER and DESCRIPTION from code below which - has this pattern (provided it appears in a single line): - val .*K = "PARAMETER" (*DESCRIPTION*) -*) -(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) - -val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) -val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) -val fact_filterK = "fact_filter" (*=STRING: fact filter*) -val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) -val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) -val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) -val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) -val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) -val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) -val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) -val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) -val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) -val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) -val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) -val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) -val proverK = "prover" (*=STRING: name of the external prover to call*) -val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) -val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) -val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) -val strictK = "strict" (*=BOOL: run in strict mode*) -val strideK = "stride" (*=NUM: run every nth goal*) -val term_orderK = "term_order" (*=STRING: term order (in E)*) -val type_encK = "type_enc" (*=STRING: type encoding scheme*) -val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) - -fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: " -fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): " - -val separator = "-----" - -(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) -(*defaults used in this Mirabelle action*) -val preplay_timeout_default = "1" -val lam_trans_default = "smart" -val uncurried_aliases_default = "smart" -val fact_filter_default = "smart" -val type_enc_default = "smart" -val strict_default = "false" -val stride_default = 1 -val max_facts_default = "smart" -val slice_default = "true" -val max_calls_default = 10000000 -val check_trivial_default = false - -(*If a key is present in args then augment a list with its pair*) -(*This is used to avoid fixing default values at the Mirabelle level, and - instead use the default values of the tool (Sledgehammer in this case).*) -fun available_parameter args key label list = - let - val value = AList.lookup (op =) args key - in if is_some value then (label, the value) :: list else list end - -datatype sh_data = ShData of { - calls: int, - success: int, - nontriv_calls: int, - nontriv_success: int, - lemmas: int, - max_lems: int, - time_isa: int, - time_prover: int, - time_prover_fail: int} - -datatype re_data = ReData of { - calls: int, - success: int, - nontriv_calls: int, - nontriv_success: int, - proofs: int, - time: int, - timeout: int, - lemmas: int * int * int, - posns: (Position.T * bool) list - } - -fun make_sh_data - (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, - time_prover,time_prover_fail) = - ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, - nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, - time_isa=time_isa, time_prover=time_prover, - time_prover_fail=time_prover_fail} - -fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, - timeout,lemmas,posns) = - ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, - nontriv_success=nontriv_success, proofs=proofs, time=time, - timeout=timeout, lemmas=lemmas, posns=posns} - -val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) -val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) - -fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, - lemmas, max_lems, time_isa, - time_prover, time_prover_fail}) = (calls, success, nontriv_calls, - nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) - -fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, - proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, - nontriv_success, proofs, time, timeout, lemmas, posns) - -datatype data = Data of { - sh: sh_data, - re_u: re_data (* proof method with unminimized set of lemmas *) - } - -fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} - -val empty_data = make_data (empty_sh_data, empty_re_data) - -fun map_sh_data f (Data {sh, re_u}) = - let val sh' = make_sh_data (f (tuple_of_sh_data sh)) - in make_data (sh', re_u) end - -fun map_re_data f (Data {sh, re_u}) = - let - val f' = make_re_data o f o tuple_of_re_data - val re_u' = f' re_u - in make_data (sh, re_u') end - -fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); - -val inc_sh_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_nontriv_calls = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) - -val inc_sh_nontriv_success = map_sh_data - (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) - => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) - -fun inc_sh_lemmas n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) - -fun inc_sh_max_lems n = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) - -fun inc_sh_time_isa t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) - -fun inc_sh_time_prover t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) - -fun inc_sh_time_prover_fail t = map_sh_data - (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) - => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) - -val inc_proof_method_calls = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_success = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_nontriv_calls = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_nontriv_success = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) - -val inc_proof_method_proofs = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) - -fun inc_proof_method_time t = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) - -val inc_proof_method_timeout = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) - -fun inc_proof_method_lemmas n = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) - -fun inc_proof_method_posns pos = map_re_data - (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) - => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) - -val str0 = string_of_int o the_default 0 - -local - -val str = string_of_int -val str3 = Real.fmt (StringCvt.FIX (SOME 3)) -fun percentage a b = string_of_int (a * 100 div b) -fun time t = Real.fromInt t / 1000.0 -fun avg_time t n = - if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 - -fun log_sh_data log - (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) = - (log ("Total number of sledgehammer calls: " ^ str calls); - log ("Number of successful sledgehammer calls: " ^ str success); - log ("Number of sledgehammer lemmas: " ^ str lemmas); - log ("Max number of sledgehammer lemmas: " ^ str max_lems); - log ("Success rate: " ^ percentage success calls ^ "%"); - log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls); - log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success); - log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa)); - log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover)); - log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail)); - log ("Average time for sledgehammer calls (Isabelle): " ^ - str3 (avg_time time_isa calls)); - log ("Average time for successful sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover success)); - log ("Average time for failed sledgehammer calls (ATP): " ^ - str3 (avg_time time_prover_fail (calls - success))) - ) - -fun str_of_pos (pos, triv) = - str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ - (if triv then "[T]" else "") - -fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls, - re_nontriv_success, re_proofs, re_time, re_timeout, - (lemmas, lems_sos, lems_max), re_posns) = - (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls); - log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^ - " (proof: " ^ str re_proofs ^ ")"); - log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout); - log ("Success rate: " ^ percentage re_success sh_calls ^ "%"); - log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls); - log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^ - " (proof: " ^ str re_proofs ^ ")"); - log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas); - log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos); - log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max); - log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time)); - log ("Average time for successful " ^ tag ^ "proof method calls: " ^ - str3 (avg_time re_time re_success)); - if tag="" - then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns)) - else () - ) - -in - -fun log_data id log (Data {sh, re_u}) = - let - val ShData {calls=sh_calls, ...} = sh - - fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else () - fun log_re tag m = - log_re_data log tag sh_calls (tuple_of_re_data m) - fun log_proof_method (tag1, m1) = app_if m1 (fn () => (log_re tag1 m1; log "")) - in - if sh_calls > 0 - then - (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); - log_sh_data log (tuple_of_sh_data sh); - log ""; - log_proof_method ("", re_u)) - else () - end - -end - -(* Warning: we implicitly assume single-threaded execution here *) -val data = Unsynchronized.ref ([] : (int * data) list) - -fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy) -fun done id ({log, ...}: Mirabelle.done_args) = - AList.lookup (op =) (!data) id - |> Option.map (log_data id log) - |> K () - -fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) - -fun get_prover_name thy args = - let - fun default_prover_name () = - hd (#provers (Sledgehammer_Commands.default_params thy [])) - handle List.Empty => error "No ATP available" - in - (case AList.lookup (op =) args proverK of - SOME name => name - | NONE => default_prover_name ()) - end - -fun get_prover ctxt name params goal = - let - val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) - in - Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name - end - -type stature = ATP_Problem_Generate.stature - -fun is_good_line s = - (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) - andalso not (String.isSubstring "(> " s) - andalso not (String.isSubstring ", > " s) - andalso not (String.isSubstring "may fail" s) - -(* Fragile hack *) -fun proof_method_from_msg args msg = - (case AList.lookup (op =) args proof_methodK of - SOME name => - if name = "smart" then - if exists is_good_line (split_lines msg) then - "none" - else - "fail" - else - name - | NONE => - if exists is_good_line (split_lines msg) then - "none" (* trust the preplayed proof *) - else if String.isSubstring "metis (" msg then - msg |> Substring.full - |> Substring.position "metis (" - |> snd |> Substring.position ")" - |> fst |> Substring.string - |> suffix ")" - else if String.isSubstring "metis" msg then - "metis" - else - "smt") - -local - -datatype sh_result = - SH_OK of int * int * (string * stature) list | - SH_FAIL of int * int | - SH_ERROR - -fun run_sh prover_name fact_filter type_enc strict max_facts slice - lam_trans uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = - let - val thy = Proof.theory_of st - val {context = ctxt, facts = chained_ths, goal} = Proof.goal st - val i = 1 - fun set_file_name (SOME dir) = - Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir - #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix - ("prob_" ^ str0 (Position.line_of pos) ^ "__") - #> Config.put SMT_Config.debug_files - (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" - ^ serial_string ()) - | set_file_name NONE = I - val st' = - st - |> Proof.map_context - (set_file_name dir - #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) - e_selection_heuristic |> the_default I) - #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) - term_order |> the_default I) - #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) - force_sos |> the_default I)) - val params as {max_facts, minimize, preplay_timeout, ...} = - Sledgehammer_Commands.default_params thy - ([(* ("verbose", "true"), *) - ("fact_filter", fact_filter), - ("type_enc", type_enc), - ("strict", strict), - ("lam_trans", lam_trans |> the_default lam_trans_default), - ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), - ("max_facts", max_facts), - ("slice", slice), - ("timeout", string_of_int timeout), - ("preplay_timeout", preplay_timeout)] - |> isar_proofsLST - |> smt_proofsLST - |> minimizeLST (*don't confuse the two minimization flags*) - |> max_new_mono_instancesLST - |> max_mono_itersLST) - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt - val time_limit = - (case hard_timeout of - NONE => I - | SOME secs => Timeout.apply (Time.fromSeconds secs)) - fun failed failure = - ({outcome = SOME failure, used_facts = [], used_from = [], - preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, - message = K ""}, ~1) - val ({outcome, used_facts, preferred_methss, run_time, message, ...} - : Sledgehammer_Prover.prover_result, - time_isa) = time_limit (Mirabelle.cpu_time (fn () => - let - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - val factss = - facts - |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name - (the_default default_max_facts max_facts) - Sledgehammer_Fact.no_fact_override hyp_ts concl_t - |> tap (fn factss => - "Line " ^ str0 (Position.line_of pos) ^ ": " ^ - Sledgehammer.string_of_factss factss - |> writeln) - val prover = get_prover ctxt prover_name params goal - val problem = - {comment = "", state = st', goal = goal, subgoal = i, - subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} - in prover params problem end)) () - handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut - | Fail "inappropriate" => failed ATP_Proof.Inappropriate - val time_prover = run_time |> Time.toMilliseconds - val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts - st' i preferred_methss) - in - (case outcome of - NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) - | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) - end - handle ERROR msg => ("error: " ^ msg, SH_ERROR) - -in - -fun run_sledgehammer trivial args proof_method named_thms id - ({pre=st, log, pos, ...}: Mirabelle.run_args) = - let - val thy = Proof.theory_of st - val triv_str = if trivial then "[T] " else "" - val _ = change_data id inc_sh_calls - val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val prover_name = get_prover_name thy args - val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default - val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default - val strict = AList.lookup (op =) args strictK |> the_default strict_default - val max_facts = - (case AList.lookup (op =) args max_factsK of - SOME max => max - | NONE => - (case AList.lookup (op =) args max_relevantK of - SOME max => max - | NONE => max_facts_default)) - val slice = AList.lookup (op =) args sliceK |> the_default slice_default - val lam_trans = AList.lookup (op =) args lam_transK - val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK - val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK - val term_order = AList.lookup (op =) args term_orderK - val force_sos = AList.lookup (op =) args force_sosK - |> Option.map (curry (op <>) "false") - val dir = AList.lookup (op =) args keepK - val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) - (* always use a hard timeout, but give some slack so that the automatic - minimizer has a chance to do its magic *) - val preplay_timeout = AList.lookup (op =) args preplay_timeoutK - |> the_default preplay_timeout_default - val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" - val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" - val minimizeLST = available_parameter args minimizeK "minimize" - val max_new_mono_instancesLST = - available_parameter args max_new_mono_instancesK max_new_mono_instancesK - val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK - val hard_timeout = SOME (4 * timeout) - val (msg, result) = - run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans - uncurried_aliases e_selection_heuristic term_order force_sos - hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST - minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st - in - (case result of - SH_OK (time_isa, time_prover, names) => - let - fun get_thms (name, stature) = - try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) - name - |> Option.map (pair (name, stature)) - in - change_data id inc_sh_success; - if trivial then () else change_data id inc_sh_nontriv_success; - change_data id (inc_sh_lemmas (length names)); - change_data id (inc_sh_max_lems (length names)); - change_data id (inc_sh_time_isa time_isa); - change_data id (inc_sh_time_prover time_prover); - proof_method := proof_method_from_msg args msg; - named_thms := SOME (map_filter get_thms names); - log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ - string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg) - end - | SH_FAIL (time_isa, time_prover) => - let - val _ = change_data id (inc_sh_time_isa time_isa) - val _ = change_data id (inc_sh_time_prover_fail time_prover) - in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end - | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)) - end - -end - -fun override_params prover type_enc timeout = - [("provers", prover), - ("max_facts", "0"), - ("type_enc", type_enc), - ("strict", "true"), - ("slice", "false"), - ("timeout", timeout |> Time.toSeconds |> string_of_int)] - -fun run_proof_method trivial full name meth named_thms id - ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = - let - fun do_method named_thms ctxt = - let - val ref_of_str = (* FIXME proper wrapper for parser combinators *) - suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none - #> Parse.thm #> fst - val thms = named_thms |> maps snd - val facts = named_thms |> map (ref_of_str o fst o fst) - val fact_override = {add = facts, del = [], only = true} - fun my_timeout time_slice = - timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal - fun sledge_tac time_slice prover type_enc = - Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (override_params prover type_enc (my_timeout time_slice)) fact_override [] - in - if !meth = "sledgehammer_tac" then - sledge_tac 0.2 ATP_Proof.vampireN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" - ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" - ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" - ORELSE' SMT_Solver.smt_tac ctxt thms - else if !meth = "smt" then - SMT_Solver.smt_tac ctxt thms - else if full then - Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] - ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if String.isPrefix "metis (" (!meth) then - let - val (type_encs, lam_trans) = - !meth - |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start - |> filter Token.is_proper |> tl - |> Metis_Tactic.parse_metis_options |> fst - |>> the_default [ATP_Proof_Reconstruct.partial_typesN] - ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans - in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end - else if !meth = "metis" then - Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if !meth = "none" then - K all_tac - else if !meth = "fail" then - K no_tac - else - (warning ("Unknown method " ^ quote (!meth)); K no_tac) - end - fun apply_method named_thms = - Mirabelle.can_apply timeout (do_method named_thms) st - - fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" - | with_time (true, t) = (change_data id inc_proof_method_success; - if trivial then () - else change_data id inc_proof_method_nontriv_success; - change_data id (inc_proof_method_lemmas (length named_thms)); - change_data id (inc_proof_method_time t); - change_data id (inc_proof_method_posns (pos, trivial)); - if name = "proof" then change_data id inc_proof_method_proofs else (); - "succeeded (" ^ string_of_int t ^ ")") - fun timed_method named_thms = - (with_time (Mirabelle.cpu_time apply_method named_thms), true) - handle Timeout.TIMEOUT _ => (change_data id inc_proof_method_timeout; ("timeout", false)) - | ERROR msg => ("error: " ^ msg, false) - - val _ = log separator - val _ = change_data id inc_proof_method_calls - val _ = if trivial then () else change_data id inc_proof_method_nontriv_calls - in - named_thms - |> timed_method - |>> log o prefix (proof_method_tag meth id) - |> snd - end - -val try_timeout = seconds 5.0 - -(* crude hack *) -val num_sledgehammer_calls = Unsynchronized.ref 0 -val remaining_stride = Unsynchronized.ref stride_default - -fun sledgehammer_action args = - let - val stride = Mirabelle.get_int_setting args (strideK, stride_default) - val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default) - val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default) - in - fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) => - let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in - if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then - () - else if !remaining_stride > 1 then - (* We still have some steps to do *) - (remaining_stride := !remaining_stride - 1; - log "Skipping because of stride") - else - (* This was the last step, now run the action *) - let - val _ = remaining_stride := stride - val _ = num_sledgehammer_calls := !num_sledgehammer_calls + 1 - in - if !num_sledgehammer_calls > max_calls then - log "Skipping because max number of calls reached" - else - let - val meth = Unsynchronized.ref "" - val named_thms = - Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) - val trivial = - if check_trivial then - Try0.try0 (SOME try_timeout) ([], [], [], []) pre - handle Timeout.TIMEOUT _ => false - else false - fun apply_method () = - (Mirabelle.catch_result (proof_method_tag meth) false - (run_proof_method trivial false name meth (these (!named_thms))) id st; ()) - in - Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st; - if is_some (!named_thms) then apply_method () else () - end - end - end - end - -fun invoke args = - Mirabelle.register (init, sledgehammer_action args, done) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,178 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML - Author: Jasmin Blanchette, TU Munich -*) - -structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION = -struct - -fun get args name default_value = - case AList.lookup (op =) args name of - SOME value => Value.parse_real value - | NONE => default_value - -fun extract_relevance_fudge args - {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, - abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight, - chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus, - chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} = - {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier, - worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, - higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight, - abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, - abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, - theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight, - theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight, - chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight, - intro_bonus = get args "intro_bonus" intro_bonus, - elim_bonus = get args "elim_bonus" elim_bonus, - simp_bonus = get args "simp_bonus" simp_bonus, - local_bonus = get args "local_bonus" local_bonus, - assum_bonus = get args "assum_bonus" assum_bonus, - chained_bonus = get args "chained_bonus" chained_bonus, - max_imperfect = get args "max_imperfect" max_imperfect, - max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, - threshold_divisor = get args "threshold_divisor" threshold_divisor, - ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} - -structure Prooftab = - Table(type key = int * int val ord = prod_ord int_ord int_ord) - -val proof_table = Unsynchronized.ref (Prooftab.empty: string list list Prooftab.table) - -val num_successes = Unsynchronized.ref ([] : (int * int) list) -val num_failures = Unsynchronized.ref ([] : (int * int) list) -val num_found_proofs = Unsynchronized.ref ([] : (int * int) list) -val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list) -val num_found_facts = Unsynchronized.ref ([] : (int * int) list) -val num_lost_facts = Unsynchronized.ref ([] : (int * int) list) - -fun get id c = the_default 0 (AList.lookup (op =) (!c) id) -fun add id c n = - c := (case AList.lookup (op =) (!c) id of - SOME m => AList.update (op =) (id, m + n) (!c) - | NONE => (id, n) :: !c) - -fun init proof_file _ thy = - let - fun do_line line = - (case line |> space_explode ":" of - [line_num, offset, proof] => - SOME (apply2 (the o Int.fromString) (line_num, offset), - proof |> space_explode " " |> filter_out (curry (op =) "")) - | _ => NONE) - val proofs = File.read (Path.explode proof_file) - val proof_tab = - proofs |> space_explode "\n" - |> map_filter do_line - |> AList.coalesce (op =) - |> Prooftab.make - in proof_table := proof_tab; thy end - -fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b) -fun percentage_alt a b = percentage a (a + b) - -fun done id ({log, ...} : Mirabelle.done_args) = - if get id num_successes + get id num_failures > 0 then - (log ""; - log ("Number of overall successes: " ^ string_of_int (get id num_successes)); - log ("Number of overall failures: " ^ string_of_int (get id num_failures)); - log ("Overall success rate: " ^ - percentage_alt (get id num_successes) (get id num_failures) ^ "%"); - log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs)); - log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs)); - log ("Proof found rate: " ^ - percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^ "%"); - log ("Number of found facts: " ^ string_of_int (get id num_found_facts)); - log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts)); - log ("Fact found rate: " ^ - percentage_alt (get id num_found_facts) (get id num_lost_facts) ^ "%")) - else - () - -val default_prover = ATP_Proof.eN (* arbitrary ATP *) - -fun with_index (i, s) = s ^ "@" ^ string_of_int i - -fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) = - case (Position.line_of pos, Position.offset_of pos) of - (SOME line_num, SOME offset) => - (case Prooftab.lookup (!proof_table) (line_num, offset) of - SOME proofs => - let - val thy = Proof.theory_of pre - val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre - val prover = AList.lookup (op =) args "prover" |> the_default default_prover - val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover - val relevance_fudge = - extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge - val subgoal = 1 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - |> Sledgehammer_Fact.drop_duplicate_facts - |> Sledgehammer_MePo.mepo_suggested_facts ctxt params - (the_default default_max_facts max_facts) (SOME relevance_fudge) hyp_ts concl_t - |> map (fst o fst) - val (found_facts, lost_facts) = - flat proofs |> sort_distinct string_ord - |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) - |> List.partition (curry (op <=) 0 o fst) - |>> sort (prod_ord int_ord string_ord) ||> map snd - val found_proofs = filter (forall (member (op =) facts)) proofs - val n = length found_proofs - val _ = - if n = 0 then - (add id num_failures 1; log "Failure") - else - (add id num_successes 1; - add id num_found_proofs n; - log ("Success (" ^ string_of_int n ^ " of " ^ - string_of_int (length proofs) ^ " proofs)")) - val _ = add id num_lost_proofs (length proofs - n) - val _ = add id num_found_facts (length found_facts) - val _ = add id num_lost_facts (length lost_facts) - val _ = - if null found_facts then - () - else - let - val found_weight = - Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) - / Real.fromInt (length found_facts) - |> Math.sqrt |> Real.ceil - in - log ("Found facts (among " ^ string_of_int (length facts) ^ - ", weight " ^ string_of_int found_weight ^ "): " ^ - commas (map with_index found_facts)) - end - val _ = if null lost_facts then - () - else - log ("Lost facts (among " ^ string_of_int (length facts) ^ - "): " ^ commas lost_facts) - in () end - | NONE => log "No known proof") - | _ => () - -val proof_fileK = "proof_file" - -fun invoke args = - let - val (pf_args, other_args) = args |> List.partition (curry (op =) proof_fileK o fst) - val proof_file = - (case pf_args of - [] => error "No \"proof_file\" specified" - | (_, s) :: _ => s) - in Mirabelle.register (init proof_file, action other_args, done) end - -end; - -(* Workaround to keep the "mirabelle.pl" script happy *) -structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter; diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/Tools/mirabelle_try0.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML - Author: Jasmin Blanchette, TU Munich -*) - -structure Mirabelle_Try0 : MIRABELLE_ACTION = -struct - -fun try0_tag id = "#" ^ string_of_int id ^ " try0: " - -fun init _ = I -fun done _ _ = () - -fun times_ten time = Time.fromMilliseconds (10 * Time.toMilliseconds time) - -fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) = - if Timeout.apply (times_ten timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre - then log (try0_tag id ^ "succeeded") - else () - handle Timeout.TIMEOUT _ => log (try0_tag id ^ "timeout") - -fun invoke _ = Mirabelle.register (init, Mirabelle.catch try0_tag run, done) - -end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/etc/settings --- a/src/HOL/Mirabelle/etc/settings Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -MIRABELLE_HOME="$COMPONENT" - -MIRABELLE_LOGIC=HOL -MIRABELLE_THEORY=Main -MIRABELLE_TIMEOUT=30 - -ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools" diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/ex/Ex.thy --- a/src/HOL/Mirabelle/ex/Ex.thy Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -theory Ex imports Pure -begin - -ML \ - val rc = Isabelle_System.bash - "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; if isabelle build -n \"$MIRABELLE_LOGIC\"; then isabelle mirabelle arith Inner_Product.thy; fi"; - if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc) - else (); -\ \ \some arbitrary small test case\ - -end - diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,136 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Sascha Boehme -# -# DESCRIPTION: testing tool for automated proof tools - - -PRG="$(basename "$0")" - -function print_action_names() -{ - for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML - do - echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' - done -} - -function print_sledgehammer_options() { - grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ - perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' -} - -function usage() { - # Do not forget to update the Sledgehammer documentation to reflect changes here. - [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" - timeout="$MIRABELLE_TIMEOUT" - echo - echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" - echo - echo " Options are:" - echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" - echo " -O DIR output directory for test data (default $out)" - echo " -S FILE user-provided setup file (no actions required)" - echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" - echo " -d DIR include session directory" - echo " -q be quiet (suppress output of Isabelle process)" - echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo - echo " Apply the given actions at all proof steps in the given theory files." - echo - echo " ACTIONS is a colon-separated list of actions, where each action is" - echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" - print_action_names - echo - echo " Available OPTIONs for the ACTION sledgehammer:" - print_sledgehammer_options - echo - echo " FILES is a list of theory files, where each file is either NAME.thy" - echo " or NAME.thy[START:END] and START and END are numbers indicating the" - echo " range the given actions are to be applied." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -[ $# -eq 0 ] && usage - -MIRABELLE_DIR= -MIRABELLE_SETUP_FILE= - -while getopts "L:T:O:d:t:S:q?" OPT -do - case "$OPT" in - L) - MIRABELLE_LOGIC="$OPTARG" - ;; - T) - MIRABELLE_THEORY="$OPTARG" - ;; - O) - MIRABELLE_OUTPUT_PATH="$OPTARG" - ;; - d) - MIRABELLE_DIR="$OPTARG" - ;; - t) - MIRABELLE_TIMEOUT="$OPTARG" - ;; - S) - MIRABELLE_SETUP_FILE="$OPTARG" - ;; - q) - MIRABELLE_QUIET="true" - ;; - \?) - usage - ;; - esac -done - -export MIRABELLE_DIR -export MIRABELLE_SETUP_FILE -export MIRABELLE_QUIET - -shift $(($OPTIND - 1)) - -export MIRABELLE_ACTIONS="$1" - -shift - - -# setup - -if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then - MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$" - PURGE_OUTPUT="true" -fi - -mkdir -p "$MIRABELLE_OUTPUT_PATH" - -export MIRABELLE_OUTPUT_PATH - - -## main - -for FILE in "$@" -do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." -done - - -## cleanup - -if [ -n "$PURGE_OUTPUT" ]; then - rm -rf "$MIRABELLE_OUTPUT_PATH" -fi diff -r 60a788467639 -r c74e25de3c00 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,182 +0,0 @@ -# -# Author: Jasmin Blanchette and Sascha Boehme -# -# Testing tool for automated proof tools. -# - -use File::Basename; - -# environment - -my $isabelle_home = $ENV{'ISABELLE_HOME'}; -my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; -my $mirabelle_dir = $ENV{'MIRABELLE_DIR'}; -my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; -my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; -my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; -my $be_quiet = $ENV{'MIRABELLE_QUIET'}; -my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'}; -my $actions = $ENV{'MIRABELLE_ACTIONS'}; - -my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; - - -# argument - -my $thy_file = $ARGV[0]; - -my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); -my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10); -my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix; -my $new_thy_file = $path . "/" . $new_thy_name . $ext; - - -# setup - -my $setup_file; -my $setup_full_name; - -if (-e $user_setup_file) { - $setup_file = undef; - my ($name, $path, $ext) = fileparse($user_setup_file, ".thy"); - $setup_full_name = $path . "/" . $name; -} -else { - -my $start_line = "0"; -my $end_line = "~1"; -if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { - $thy_file = $1; - $start_line = $2; - $end_line = $3; -} - -my $setup_thy_name = $thy_name . "_Setup"; -my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; -my $log_file = $output_path . "/" . $thy_name . ".log"; - -my @action_files; -my @action_names; -foreach (split(/:/, $actions)) { - if (m/([^[]*)/) { - push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; - push @action_names, $1; - } -} -my $tools = ""; -if ($#action_files >= 0) { - # uniquify - my $s = join ("\n", @action_files); - my @action_files = split(/\n/, $s . "\n" . $s); - %action_files = sort(@action_files); - $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files)))); -} - -open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; - -print SETUP_FILE < - Config.put_global Mirabelle.timeout $timeout #> - Config.put_global Mirabelle.start_line $start_line #> - Config.put_global Mirabelle.end_line $end_line -*} - -END - -@action_list = split(/:/, $actions); - -foreach (reverse(@action_list)) { - if (m/([^[]*)(?:\[(.*)\])?/) { - my ($name, $settings_str) = ($1, $2 || ""); - $name =~ s/^([a-z])/\U$1/; - print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; - my $sep = ""; - foreach (split(/,/, $settings_str)) { - if (m/\s*([^=]*)\s*=\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"$2\")"; - $sep = ", "; - } - elsif (m/\s*(.*)\s*/) { - print SETUP_FILE "$sep(\"$1\", \"\")"; - $sep = ", "; - } - } - print SETUP_FILE "] *}\n"; - } -} - -print SETUP_FILE "\nend"; -close SETUP_FILE; - -$setup_full_name = $output_path . "/" . $setup_thy_name; - -open(LOG_FILE, ">$log_file"); -print LOG_FILE "Run of $new_thy_file with:\n"; -foreach $action (@action_list) { - print LOG_FILE " $action\n"; -} -close(LOG_FILE); - -} - - -# modify target theory file - -open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; -my @lines = ; -close(OLD_FILE); - -my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); - -my $thy_text = join("", @lines); -my $old_len = length($thy_text); -$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; -$thy_text =~ s/\b$thy_name\./$new_thy_name./g; -$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g; -die "No 'imports' found" if length($thy_text) == $old_len; - -open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; -print NEW_FILE $thy_text; -close(NEW_FILE); - - -# run isabelle - -my $quiet = ""; -my $output_log = 1; -if (defined $be_quiet and $be_quiet ne "") { - $quiet = " > /dev/null 2>&1"; - $output_log = 0; -} - -if ($output_log) { print "Mirabelle: $thy_file\n"; } - -my $cmd = - "isabelle process -o quick_and_dirty -o threads=1" . - " -T \"$path/$new_thy_name\" " . - ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") . - "-l $mirabelle_logic" . $quiet; -my $result = system "bash", "-c", $cmd; - -if ($output_log) { - my $outcome = ($result ? "failure" : "success"); - print "\nFinished: $thy_file [$outcome]\n"; -} - - -# cleanup - -if (defined $setup_file) { - unlink $setup_file; -} -unlink $new_thy_file; - -exit ($result ? 1 : 0); diff -r 60a788467639 -r c74e25de3c00 src/HOL/ROOT --- a/src/HOL/ROOT Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/ROOT Sat May 15 22:39:07 2021 +0200 @@ -937,12 +937,13 @@ theories NSPrimes -session "HOL-Mirabelle" in Mirabelle = HOL + - theories Mirabelle_Test - -session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + - options [timeout = 60] - theories Ex +session "HOL-Mirabelle-ex" in "Tools/Mirabelle" = HOL + + description "Some arbitrary small test case for Mirabelle." + options [timeout = 60, mirabelle_actions = "arith"] + sessions + "HOL-Analysis" + theories + "HOL-Analysis.Inner_Product" session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL + options [quick_and_dirty] diff -r 60a788467639 -r c74e25de3c00 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/Sledgehammer.thy Sat May 15 22:39:07 2021 +0200 @@ -33,5 +33,6 @@ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ ML_file \Tools/Sledgehammer/sledgehammer.ML\ ML_file \Tools/Sledgehammer/sledgehammer_commands.ML\ +ML_file \Tools/Sledgehammer/sledgehammer_tactics.ML\ end diff -r 60a788467639 -r c74e25de3c00 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sat May 15 22:39:07 2021 +0200 @@ -8,8 +8,6 @@ imports Complex_Main TPTP_Interpret "HOL-Library.Refute" begin -ML_file \sledgehammer_tactics.ML\ - ML \Proofterm.proofs := 0\ declare [[show_consts]] (* for Refute *) diff -r 60a788467639 -r c74e25de3c00 src/HOL/TPTP/TPTP_Parser_Example.thy --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Sat May 15 22:39:07 2021 +0200 @@ -8,8 +8,6 @@ imports TPTP_Parser TPTP_Interpret begin -ML_file "sledgehammer_tactics.ML" - import_tptp "$TPTP/Problems/LCL/LCL414+1.p" ML \ diff -r 60a788467639 -r c74e25de3c00 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Fri May 14 12:43:19 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -(* Title: HOL/TPTP/sledgehammer_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2010, 2011 - -Sledgehammer as a tactic. -*) - -signature SLEDGEHAMMER_TACTICS = -sig - type fact_override = Sledgehammer_Fact.fact_override - - val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> - thm list -> int -> tactic - val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> - thm list -> int -> tactic -end; - -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = -struct - -open Sledgehammer_Util -open Sledgehammer_Fact -open Sledgehammer_Prover -open Sledgehammer_Prover_ATP -open Sledgehammer_Prover_Minimize -open Sledgehammer_MaSh -open Sledgehammer_Commands - -fun run_prover override_params fact_override chained i n ctxt goal = - let - val thy = Proof_Context.theory_of ctxt - val mode = Normal - val params as {provers, max_facts, ...} = default_params thy override_params - val name = hd provers - val prover = get_prover ctxt mode name - val default_max_facts = default_max_facts_of_prover ctxt name - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt - val ho_atp = exists (is_ho_atp ctxt) provers - val keywords = Thy_Header.get_keywords' ctxt - val css_table = clasimpset_rule_table_of ctxt - val facts = - nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t - |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override - hyp_ts concl_t - |> hd |> snd - val problem = - {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_proof = I} - in - (case prover params problem of - {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME - | _ => NONE) - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) - end - -fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = - let val override_params = override_params @ [("preplay_timeout", "0")] in - (case run_prover override_params fact_override chained i i ctxt th of - SOME facts => - Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt - (maps (thms_of_name ctxt) facts) i th - | NONE => Seq.empty) - end - -fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = - let - val override_params = - override_params @ - [("preplay_timeout", "0"), - ("minimize", "false")] - val xs = run_prover override_params fact_override chained i i ctxt th - in - if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty - end - -end; diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,252 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius +*) + +signature MIRABELLE = +sig + (*core*) + val print_name: string -> string + val print_properties: Properties.T -> string + type context = + {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} + type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} + val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory + val log_command: command -> XML.body -> XML.tree + val log_report: Properties.T -> XML.body -> XML.tree + val print_exn: exn -> string + val command_action: binding -> (context -> command -> string) -> theory -> theory + + (*utility functions*) + val can_apply : Time.time -> (Proof.context -> int -> tactic) -> + Proof.state -> bool + val theorems_in_proof_term : theory -> thm -> thm list + val theorems_of_sucessful_proof: Toplevel.state -> thm list + val get_argument : (string * string) list -> string * string -> string + val get_int_argument : (string * string) list -> string * int -> int + val get_bool_argument : (string * string) list -> string * bool -> bool + val cpu_time : ('a -> 'b) -> 'a -> 'b * int +end + +structure Mirabelle : MIRABELLE = +struct + +(** Mirabelle core **) + +(* concrete syntax *) + +val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); + +val print_name = Token.print_name keywords; +val print_properties = Token.print_properties keywords; + +fun read_actions str = + Token.read_body keywords + (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) + (Symbol_Pos.explode0 str); + + +(* actions *) + +type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; +type context = + {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; + +structure Data = Theory_Data +( + type T = (context -> command list -> XML.body) Name_Space.table; + val empty = Name_Space.empty_table "mirabelle_action"; + val extend = I; + val merge = Name_Space.merge_tables; +); + +fun theory_action binding action thy = + let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); + in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; + + +(* log content *) + +fun log_action name arguments = + XML.Elem (("action", (Markup.nameN, name) :: arguments), + [XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); + +fun log_command ({name, pos, ...}: command) body = + XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); + +fun log_report props body = + XML.Elem (("report", props), body); + + +(* apply actions *) + +fun apply_action index name arguments timeout commands thy = + let + val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); + val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; + val context = {index = index, tag = tag, arguments = arguments, timeout = timeout, theory = thy}; + val export_body = action context commands; + val export_head = log_action name arguments; + val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); + in + if null export_body then () + else Export.export thy export_name (export_head :: export_body) + end; + +fun print_exn exn = + (case exn of + Timeout.TIMEOUT _ => "timeout" + | ERROR msg => "error: " ^ msg + | exn => "exception:\n" ^ General.exnMessage exn); + +fun command_action binding action = + let + fun apply context command = + let val s = + action context command handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else #tag context ^ print_exn exn; + in + if s = "" then NONE + else SOME (log_command command [XML.Text s]) end; + in theory_action binding (map_filter o apply) end; + + +(* theory line range *) + +local + +val theory_name = + Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) + >> Symbol_Pos.content; + +val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); +val end_line = Symbol_Pos.$$ ":" |-- line; +val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; + +in + +fun read_theory_range str = + (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of + SOME res => res + | NONE => error ("Malformed specification of theory line range: " ^ quote str)); + +end; + +fun check_theories strs = + let + val theories = map read_theory_range strs; + fun get_theory name = + if null theories then SOME NONE + else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; + fun check_line NONE _ = false + | check_line _ NONE = true + | check_line (SOME NONE) _ = true + | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i + | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; + fun check_pos range = check_line range o Position.line_of; + in check_pos o get_theory end; + + +(* presentation hook *) + +val whitelist = ["apply", "by", "proof"]; + +val _ = + Theory.setup (Thy_Info.add_presentation (fn context => fn thy => + let + val {options, adjust_pos, segments, ...} = context; + val mirabelle_timeout = Options.seconds options \<^system_option>\mirabelle_timeout\; + val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; + val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; + + val actions = + (case read_actions mirabelle_actions of + SOME actions => actions + | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); + val check = check_theories (space_explode "," mirabelle_theories); + val commands = + segments |> map_filter (fn {command = tr, prev_state = st, state = st', ...} => + let + val name = Toplevel.name_of tr; + val pos = adjust_pos (Toplevel.pos_of tr); + in + if can (Proof.assert_backward o Toplevel.proof_of) st andalso + member (op =) whitelist name andalso + check (Context.theory_long_name thy) pos + then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'} + else NONE + end); + + fun apply (i, (name, arguments)) () = + apply_action (i + 1) name arguments mirabelle_timeout commands thy; + in if null commands then () else fold_index apply actions () end)); + + +(* Mirabelle utility functions *) + +fun can_apply time tac st = + let + val {context = ctxt, facts, goal} = Proof.goal st; + val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); + in + (case try (Timeout.apply time (Seq.pull o full_tac)) goal of + SOME (SOME _) => true + | _ => false) + end; + +local + +fun fold_body_thms f = + let + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => + fn (x, seen) => + if Inttab.defined seen i then (x, seen) + else + let + val name = Proofterm.thm_node_name thm_node; + val prop = Proofterm.thm_node_prop thm_node; + val body = Future.join (Proofterm.thm_node_body thm_node); + val (x', seen') = + app (n + (if name = "" then 0 else 1)) body + (x, Inttab.update (i, ()) seen); + in (x' |> n = 0 ? f (name, prop, body), seen') end); + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; + +in + +fun theorems_in_proof_term thy thm = + let + val all_thms = Global_Theory.all_thms_of thy true; + fun collect (s, _, _) = if s <> "" then insert (op =) s else I; + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; + fun resolve_thms names = map_filter (member_of names) all_thms; + in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; + +end; + +fun theorems_of_sucessful_proof st = + (case try Toplevel.proof_of st of + NONE => [] + | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); + +fun get_argument arguments (key, default) = + the_default default (AList.lookup (op =) arguments key); + +fun get_int_argument arguments (key, default) = + (case Option.map Int.fromString (AList.lookup (op =) arguments key) of + SOME (SOME i) => i + | SOME NONE => error ("bad option: " ^ key) + | NONE => default); + +fun get_bool_argument arguments (key, default) = + (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of + SOME (SOME i) => i + | SOME NONE => error ("bad option: " ^ key) + | NONE => default); + +fun cpu_time f x = + let val ({cpu, ...}, y) = Timing.timing f x + in (y, Time.toMilliseconds cpu) end; + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,273 @@ +/* Title: HOL/Tools/Mirabelle/mirabelle.scala + Author: Makarius + +Isabelle/Scala front-end for Mirabelle. +*/ + +package isabelle.mirabelle + +import isabelle._ + + +object Mirabelle +{ + /* actions and options */ + + def action_names(): List[String] = + { + val Pattern = """Mirabelle action: "(\w+)".*""".r + (for { + file <- + File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, + pred = _.getName.endsWith(".ML")) + line <- split_lines(File.read(file)) + name <- line match { case Pattern(a) => Some(a) case _ => None } + } yield name).sorted + } + + def sledgehammer_options(): List[String] = + { + val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r + split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). + flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) + } + + + /* exported log content */ + + object Log + { + def export_name(index: Int, theory: String = ""): String = + Export.compound_name(theory, "mirabelle/" + index) + + val separator = "\n------------------\n" + + sealed abstract class Entry { def print: String } + + case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry + { + def print: String = "action: " + XML.content(body) + separator + } + case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry + { + def print: String = "\n" + print_head + separator + Pretty.string_of(body) + def print_head: String = + { + val line = Position.Line.get(position) + val offset = Position.Offset.get(position) + val loc = line.toString + ":" + offset.toString + "at " + loc + " (" + name + "):" + } + } + case class Report(result: Properties.T, body: XML.Body) extends Entry + { + override def print: String = "\n" + separator + Pretty.string_of(body) + } + + def entry(export_name: String, xml: XML.Tree): Entry = + xml match { + case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) => + Action(name, props, body) + case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) => + Command(name, props.filter(Markup.position_property), body) + case XML.Elem(Markup("report", props), body) => Report(props, body) + case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml) + } + } + + + /* main mirabelle */ + + def mirabelle( + options: Options, + actions: List[String], + output_dir: Path, + theories: List[String] = Nil, + selection: Sessions.Selection = Sessions.Selection.empty, + progress: Progress = new Progress, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + numa_shuffling: Boolean = false, + max_jobs: Int = 1, + verbose: Boolean = false): Build.Results = + { + require(!selection.requirements) + + progress.echo("Building required heaps ...") + val build_results0 = + Build.build(options, build_heap = true, + selection = selection.copy(requirements = true), progress = progress, dirs = dirs, + select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, + verbose = verbose) + + if (build_results0.ok) { + val build_options = + options + "parallel_presentation=false" + + ("mirabelle_actions=" + actions.mkString(";")) + + ("mirabelle_theories=" + theories.mkString(",")) + + progress.echo("Running Mirabelle ...") + val build_results = + Build.build(build_options, clean_build = true, + selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, + numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) + + if (build_results.ok) { + val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) + val store = Sessions.store(build_options) + + using(store.open_database_context())(db_context => + { + var seen_theories = Set.empty[String] + for { + session <- structure.imports_selection(selection).iterator + session_hierarchy = structure.hierarchy(session) + theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) + theory <- theories + if !seen_theories(theory) + index <- 1 to actions.length + export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index)) + body = export.uncompressed_yxml + if body.nonEmpty + } { + seen_theories += theory + val export_name = Log.export_name(index, theory = theory) + val log = body.map(Log.entry(export_name, _)) + val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) + val log_file = log_dir + Path.basic("mirabelle" + index).log + progress.echo("Writing " + log_file) + File.write(log_file, terminate_lines(log.map(_.print))) + } + }) + } + + build_results + } + else build_results0 + } + + + /* Isabelle tool wrapper */ + + val default_output_dir: Path = Path.explode("mirabelle") + + val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", + Scala_Project.here, args => + { + val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) + + var actions: List[String] = Nil + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var numa_shuffling = false + var output_dir = default_output_dir + var requirements = false + var theories: List[String] = Nil + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var max_jobs = 1 + var options = Options.init(opts = build_options) + var verbose = false + var exclude_sessions: List[String] = Nil + + val default_timeout = options.seconds("mirabelle_timeout") + + val getopts = Getopts(""" +Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...] + + Options are: + -A ACTION add to list of actions + -B NAME include session NAME and all descendants + -D DIR include session directory and select its sessions + -N cyclic shuffling of NUMA CPU nodes (performance tuning) + -O DIR output directory for log files (default: """ + default_output_dir + """, + -R refer to requirements of selected sessions + -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -j INT maximum number of parallel jobs (default 1) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -t SECONDS timeout for each action (default """ + default_timeout + """) + -v verbose + -x NAME exclude session NAME and all descendants + + Apply the given actions at all theories and proof steps of the + specified sessions. + + The absence of theory restrictions (option -T) means to check all + theories fully. Otherwise only the named theories are checked. + + Each ACTION is either of the form NAME or NAME [OPTION, ...] + following Isabelle/Isar outer syntax. + + Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """ + + For the ACTION "sledgehammer", the following OPTIONs are available:""" + + sledgehammer_options().mkString("\n ", "\n ", "\n"), + "A:" -> (arg => actions = actions ::: List(arg)), + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "N" -> (_ => numa_shuffling = true), + "O:" -> (arg => output_dir = Path.explode(arg)), + "R" -> (_ => requirements = true), + "T:" -> (arg => theories = theories ::: List(arg)), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "j:" -> (arg => max_jobs = Value.Int.parse(arg)), + "o:" -> (arg => options = options + arg), + "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + if (actions.isEmpty) getopts.usage() + + val progress = new Console_Progress(verbose = verbose) + + val start_date = Date.now() + + if (verbose) { + progress.echo("Started at " + Build_Log.print_date(start_date)) + } + + val results = + progress.interrupt_handler { + mirabelle(options, actions, output_dir, + theories = theories, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions), + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), + max_jobs = max_jobs, + verbose = verbose) + } + + val end_date = Date.now() + val elapsed_time = end_date.time - start_date.time + + if (verbose) { + progress.echo("\nFinished at " + Build_Log.print_date(end_date)) + } + + val total_timing = + results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) + + sys.exit(results.rc) + }) +} diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,17 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Makarius + +Mirabelle action: "arith". +*) + +structure Mirabelle_Arith: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\arith\ + (fn {timeout, ...} => fn {pre, ...} => + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre + then "succeeded" else "")); + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,23 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "metis". +*) + +structure Mirabelle_Metis: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\metis\ + (fn {timeout, ...} => fn {pre, post, ...} => + let + val thms = Mirabelle.theorems_of_sucessful_proof post; + val names = map Thm.get_name_hint thms; + val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre))); + fun metis ctxt = Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt (thms @ facts); + in + (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") + |> not (null names) ? suffix (":\n" ^ commas names) + end)); + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,23 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML + Author: Jasmin Blanchette and Sascha Boehme, TU Munich + +Mirabelle action: "quickcheck". +*) + +structure Mirabelle_Quickcheck: sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\quickcheck\ + (fn {arguments, timeout, ...} => fn {pre, ...} => + let + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst; + val quickcheck = + Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1; + in + (case Timeout.apply timeout quickcheck pre of + NONE => "no counterexample" + | SOME _ => "counterexample found") + end)); + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,684 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML + Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich + Author: Makarius + +Mirabelle action: "sledgehammer". +*) + +structure Mirabelle_Sledgehammer: sig end = +struct + +(*To facilitate synching the description of Mirabelle Sledgehammer parameters + (in ../lib/Tools/mirabelle) with the parameters actually used by this + interface, the former extracts PARAMETER and DESCRIPTION from code below which + has this pattern (provided it appears in a single line): + val .*K = "PARAMETER" (*DESCRIPTION*) +*) +(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) + +val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) +val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) +val fact_filterK = "fact_filter" (*=STRING: fact filter*) +val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) +val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) +val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) +val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) +val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) +val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) +val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) +val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) +val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) +val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) +val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) +val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) +val proverK = "prover" (*=STRING: name of the external prover to call*) +val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) +val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) +val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) +val strictK = "strict" (*=BOOL: run in strict mode*) +val strideK = "stride" (*=NUM: run every nth goal*) +val term_orderK = "term_order" (*=STRING: term order (in E)*) +val type_encK = "type_enc" (*=STRING: type encoding scheme*) +val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) + +val separator = "-----" + +(*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) +(*defaults used in this Mirabelle action*) +val preplay_timeout_default = "1" +val lam_trans_default = "smart" +val uncurried_aliases_default = "smart" +val fact_filter_default = "smart" +val type_enc_default = "smart" +val strict_default = "false" +val stride_default = 1 +val max_facts_default = "smart" +val slice_default = "true" +val max_calls_default = 10000000 +val check_trivial_default = false + +(*If a key is present in args then augment a list with its pair*) +(*This is used to avoid fixing default values at the Mirabelle level, and + instead use the default values of the tool (Sledgehammer in this case).*) +fun available_parameter args key label list = + let + val value = AList.lookup (op =) args key + in if is_some value then (label, the value) :: list else list end + +datatype sh_data = ShData of { + calls: int, + success: int, + nontriv_calls: int, + nontriv_success: int, + lemmas: int, + max_lems: int, + time_isa: int, + time_prover: int, + time_prover_fail: int} + +datatype re_data = ReData of { + calls: int, + success: int, + nontriv_calls: int, + nontriv_success: int, + proofs: int, + time: int, + timeout: int, + lemmas: int * int * int, + posns: (Position.T * bool) list + } + +fun make_sh_data + (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, + time_prover,time_prover_fail) = + ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, + nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, + time_isa=time_isa, time_prover=time_prover, + time_prover_fail=time_prover_fail} + +fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, + timeout,lemmas,posns) = + ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, + nontriv_success=nontriv_success, proofs=proofs, time=time, + timeout=timeout, lemmas=lemmas, posns=posns} + +val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) +val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) + +fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, + lemmas, max_lems, time_isa, + time_prover, time_prover_fail}) = (calls, success, nontriv_calls, + nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) + +fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, + proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, + nontriv_success, proofs, time, timeout, lemmas, posns) + +datatype data = Data of { + sh: sh_data, + re_u: re_data (* proof method with unminimized set of lemmas *) + } + +type change_data = (data -> data) -> unit + +fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} + +val empty_data = make_data (empty_sh_data, empty_re_data) + +fun map_sh_data f (Data {sh, re_u}) = + let val sh' = make_sh_data (f (tuple_of_sh_data sh)) + in make_data (sh', re_u) end + +fun map_re_data f (Data {sh, re_u}) = + let + val f' = make_re_data o f o tuple_of_re_data + val re_u' = f' re_u + in make_data (sh, re_u') end + +fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); + +val inc_sh_calls = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_success = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_nontriv_calls = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) + +val inc_sh_nontriv_success = map_sh_data + (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) + => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) + +fun inc_sh_lemmas n = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) + +fun inc_sh_max_lems n = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) + +fun inc_sh_time_isa t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) + +fun inc_sh_time_prover t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) + +fun inc_sh_time_prover_fail t = map_sh_data + (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) + => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) + +val inc_proof_method_calls = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_success = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_nontriv_calls = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_nontriv_success = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) + +val inc_proof_method_proofs = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) + +fun inc_proof_method_time t = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) + +val inc_proof_method_timeout = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) + +fun inc_proof_method_lemmas n = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) + +fun inc_proof_method_posns pos = map_re_data + (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) + => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) + +val str0 = string_of_int o the_default 0 + +local + +val str = string_of_int +val str3 = Real.fmt (StringCvt.FIX (SOME 3)) +fun percentage a b = string_of_int (a * 100 div b) +fun ms t = Real.fromInt t / 1000.0 +fun avg_time t n = + if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 + +fun log_sh_data (ShData + {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = + let + val props = + [("sh_calls", str calls), + ("sh_success", str success), + ("sh_nontriv_calls", str nontriv_calls), + ("sh_nontriv_success", str nontriv_success), + ("sh_lemmas", str lemmas), + ("sh_max_lems", str max_lems), + ("sh_time_isa", str3 (ms time_isa)), + ("sh_time_prover", str3 (ms time_prover)), + ("sh_time_prover_fail", str3 (ms time_prover_fail))] + val text = + "\nTotal number of sledgehammer calls: " ^ str calls ^ + "\nNumber of successful sledgehammer calls: " ^ str success ^ + "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ + "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ + "\nSuccess rate: " ^ percentage success calls ^ "%" ^ + "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ + "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ + "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ + "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^ + "\nAverage time for sledgehammer calls (Isabelle): " ^ + str3 (avg_time time_isa calls) ^ + "\nAverage time for successful sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover success) ^ + "\nAverage time for failed sledgehammer calls (ATP): " ^ + str3 (avg_time time_prover_fail (calls - success)) + in (props, text) end + +fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, + nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = + let + val proved = + posns |> map (fn (pos, triv) => + str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ + (if triv then "[T]" else "")) + val props = + [("re_calls", str calls), + ("re_success", str success), + ("re_nontriv_calls", str nontriv_calls), + ("re_nontriv_success", str nontriv_success), + ("re_proofs", str proofs), + ("re_time", str3 (ms time)), + ("re_timeout", str timeout), + ("re_lemmas", str lemmas), + ("re_lems_sos", str lems_sos), + ("re_lems_max", str lems_max), + ("re_proved", space_implode "," proved)] + val text = + "\nTotal number of proof method calls: " ^ str calls ^ + "\nNumber of successful proof method calls: " ^ str success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of proof method timeouts: " ^ str timeout ^ + "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ + "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ + "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ + " (proof: " ^ str proofs ^ ")" ^ + "\nNumber of successful proof method lemmas: " ^ str lemmas ^ + "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ + "\nMax number of successful proof method lemmas: " ^ str lems_max ^ + "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ + "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ + "\nProved: " ^ space_implode " " proved + in (props, text) end + +in + +fun log_data index (Data {sh, re_u}) = + let + val ShData {calls=sh_calls, ...} = sh + val ReData {calls=re_calls, ...} = re_u + in + if sh_calls > 0 then + let + val (props1, text1) = log_sh_data sh + val (props2, text2) = log_re_data sh_calls re_u + val text = + "\n\nReport #" ^ string_of_int index ^ ":\n" ^ + (if re_calls > 0 then text1 ^ "\n" ^ text2 else text1) + in [Mirabelle.log_report (props1 @ props2) [XML.Text text]] end + else [] + end + +end + +fun get_prover_name thy args = + let + fun default_prover_name () = + hd (#provers (Sledgehammer_Commands.default_params thy [])) + handle List.Empty => error "No ATP available" + in + (case AList.lookup (op =) args proverK of + SOME name => name + | NONE => default_prover_name ()) + end + +fun get_prover ctxt name params goal = + let + val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) + in + Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name + end + +type stature = ATP_Problem_Generate.stature + +fun is_good_line s = + (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) + andalso not (String.isSubstring "(> " s) + andalso not (String.isSubstring ", > " s) + andalso not (String.isSubstring "may fail" s) + +(* Fragile hack *) +fun proof_method_from_msg args msg = + (case AList.lookup (op =) args proof_methodK of + SOME name => + if name = "smart" then + if exists is_good_line (split_lines msg) then + "none" + else + "fail" + else + name + | NONE => + if exists is_good_line (split_lines msg) then + "none" (* trust the preplayed proof *) + else if String.isSubstring "metis (" msg then + msg |> Substring.full + |> Substring.position "metis (" + |> snd |> Substring.position ")" + |> fst |> Substring.string + |> suffix ")" + else if String.isSubstring "metis" msg then + "metis" + else + "smt") + +local + +datatype sh_result = + SH_OK of int * int * (string * stature) list | + SH_FAIL of int * int | + SH_ERROR + +fun run_sh prover_name fact_filter type_enc strict max_facts slice + lam_trans uncurried_aliases e_selection_heuristic term_order force_sos + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = + let + val thy = Proof.theory_of st + val {context = ctxt, facts = chained_ths, goal} = Proof.goal st + val i = 1 + fun set_file_name (SOME dir) = + Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir + #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix + ("prob_" ^ str0 (Position.line_of pos) ^ "__") + #> Config.put SMT_Config.debug_files + (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" + ^ serial_string ()) + | set_file_name NONE = I + val st' = + st + |> Proof.map_context + (set_file_name dir + #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) + e_selection_heuristic |> the_default I) + #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) + term_order |> the_default I) + #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) + force_sos |> the_default I)) + val params as {max_facts, minimize, preplay_timeout, ...} = + Sledgehammer_Commands.default_params thy + ([(* ("verbose", "true"), *) + ("fact_filter", fact_filter), + ("type_enc", type_enc), + ("strict", strict), + ("lam_trans", lam_trans |> the_default lam_trans_default), + ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), + ("max_facts", max_facts), + ("slice", slice), + ("timeout", string_of_int timeout), + ("preplay_timeout", preplay_timeout)] + |> isar_proofsLST + |> smt_proofsLST + |> minimizeLST (*don't confuse the two minimization flags*) + |> max_new_mono_instancesLST + |> max_mono_itersLST) + val default_max_facts = + Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt + val time_limit = + (case hard_timeout of + NONE => I + | SOME secs => Timeout.apply (Time.fromSeconds secs)) + fun failed failure = + ({outcome = SOME failure, used_facts = [], used_from = [], + preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, + message = K ""}, ~1) + val ({outcome, used_facts, preferred_methss, run_time, message, ...} + : Sledgehammer_Prover.prover_result, + time_isa) = time_limit (Mirabelle.cpu_time (fn () => + let + val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name + val keywords = Thy_Header.get_keywords' ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_fact_override keywords css_table chained_ths + hyp_ts concl_t + val factss = + facts + |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name + (the_default default_max_facts max_facts) + Sledgehammer_Fact.no_fact_override hyp_ts concl_t + |> tap (fn factss => + "Line " ^ str0 (Position.line_of pos) ^ ": " ^ + Sledgehammer.string_of_factss factss + |> writeln) + val prover = get_prover ctxt prover_name params goal + val problem = + {comment = "", state = st', goal = goal, subgoal = i, + subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} + in prover params problem end)) () + handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut + | Fail "inappropriate" => failed ATP_Proof.Inappropriate + val time_prover = run_time |> Time.toMilliseconds + val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts + st' i preferred_methss) + in + (case outcome of + NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) + | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) + end + handle ERROR msg => ("error: " ^ msg, SH_ERROR) + +in + +fun run_sledgehammer change_data trivial args proof_method named_thms pos st = + let + val thy = Proof.theory_of st + val triv_str = if trivial then "[T] " else "" + val _ = change_data inc_sh_calls + val _ = if trivial then () else change_data inc_sh_nontriv_calls + val prover_name = get_prover_name thy args + val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default + val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default + val strict = AList.lookup (op =) args strictK |> the_default strict_default + val max_facts = + (case AList.lookup (op =) args max_factsK of + SOME max => max + | NONE => + (case AList.lookup (op =) args max_relevantK of + SOME max => max + | NONE => max_facts_default)) + val slice = AList.lookup (op =) args sliceK |> the_default slice_default + val lam_trans = AList.lookup (op =) args lam_transK + val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK + val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK + val term_order = AList.lookup (op =) args term_orderK + val force_sos = AList.lookup (op =) args force_sosK + |> Option.map (curry (op <>) "false") + val dir = AList.lookup (op =) args keepK + val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30) + (* always use a hard timeout, but give some slack so that the automatic + minimizer has a chance to do its magic *) + val preplay_timeout = AList.lookup (op =) args preplay_timeoutK + |> the_default preplay_timeout_default + val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" + val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" + val minimizeLST = available_parameter args minimizeK "minimize" + val max_new_mono_instancesLST = + available_parameter args max_new_mono_instancesK max_new_mono_instancesK + val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK + val hard_timeout = SOME (4 * timeout) + val (msg, result) = + run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans + uncurried_aliases e_selection_heuristic term_order force_sos + hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST + minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st + in + (case result of + SH_OK (time_isa, time_prover, names) => + let + fun get_thms (name, stature) = + try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) + name + |> Option.map (pair (name, stature)) + in + change_data inc_sh_success; + if trivial then () else change_data inc_sh_nontriv_success; + change_data (inc_sh_lemmas (length names)); + change_data (inc_sh_max_lems (length names)); + change_data (inc_sh_time_isa time_isa); + change_data (inc_sh_time_prover time_prover); + proof_method := proof_method_from_msg args msg; + named_thms := SOME (map_filter get_thms names); + triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ + string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg + end + | SH_FAIL (time_isa, time_prover) => + let + val _ = change_data (inc_sh_time_isa time_isa) + val _ = change_data (inc_sh_time_prover_fail time_prover) + in triv_str ^ "failed: " ^ msg end + | SH_ERROR => "failed: " ^ msg) + end + +end + +fun override_params prover type_enc timeout = + [("provers", prover), + ("max_facts", "0"), + ("type_enc", type_enc), + ("strict", "true"), + ("slice", "false"), + ("timeout", timeout |> Time.toSeconds |> string_of_int)] + +fun run_proof_method change_data trivial full name meth named_thms timeout pos st = + let + fun do_method named_thms ctxt = + let + val ref_of_str = (* FIXME proper wrapper for parser combinators *) + suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none + #> Parse.thm #> fst + val thms = named_thms |> maps snd + val facts = named_thms |> map (ref_of_str o fst o fst) + val fact_override = {add = facts, del = [], only = true} + fun my_timeout time_slice = + timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal + fun sledge_tac time_slice prover type_enc = + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (override_params prover type_enc (my_timeout time_slice)) fact_override [] + in + if !meth = "sledgehammer_tac" then + sledge_tac 0.2 ATP_Proof.vampireN "mono_native" + ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" + ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" + ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" + ORELSE' SMT_Solver.smt_tac ctxt thms + else if !meth = "smt" then + SMT_Solver.smt_tac ctxt thms + else if full then + Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] + ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms + else if String.isPrefix "metis (" (!meth) then + let + val (type_encs, lam_trans) = + !meth + |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start + |> filter Token.is_proper |> tl + |> Metis_Tactic.parse_metis_options |> fst + |>> the_default [ATP_Proof_Reconstruct.partial_typesN] + ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans + in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end + else if !meth = "metis" then + Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms + else if !meth = "none" then + K all_tac + else if !meth = "fail" then + K no_tac + else + (warning ("Unknown method " ^ quote (!meth)); K no_tac) + end + fun apply_method named_thms = + Mirabelle.can_apply timeout (do_method named_thms) st + + fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" + | with_time (true, t) = (change_data inc_proof_method_success; + if trivial then () + else change_data inc_proof_method_nontriv_success; + change_data (inc_proof_method_lemmas (length named_thms)); + change_data (inc_proof_method_time t); + change_data (inc_proof_method_posns (pos, trivial)); + if name = "proof" then change_data inc_proof_method_proofs else (); + "succeeded (" ^ string_of_int t ^ ")") + fun timed_method named_thms = + with_time (Mirabelle.cpu_time apply_method named_thms) + handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout") + | ERROR msg => ("error: " ^ msg) + + val _ = change_data inc_proof_method_calls + val _ = if trivial then () else change_data inc_proof_method_nontriv_calls + in timed_method named_thms end + +val try_timeout = seconds 5.0 + +fun catch e = + e () handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else Mirabelle.print_exn exn + +(* crude hack *) +val num_sledgehammer_calls = Unsynchronized.ref 0 +val remaining_stride = Unsynchronized.ref stride_default + +val _ = + Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer\ + (fn context => fn commands => + let + val {index, tag = sh_tag, arguments = args, timeout, ...} = context + fun proof_method_tag meth = "#" ^ string_of_int index ^ " " ^ meth ^ " (sledgehammer): " + + val data = Unsynchronized.ref empty_data + val change_data = Unsynchronized.change data + + val stride = Mirabelle.get_int_argument args (strideK, stride_default) + val max_calls = Mirabelle.get_int_argument args (max_callsK, max_calls_default) + val check_trivial = Mirabelle.get_bool_argument args (check_trivialK, check_trivial_default) + + val results = + commands |> maps (fn command => + let + val {name, pos, pre = st, ...} = command + val goal = Thm.major_prem_of (#goal (Proof.goal st)) + val log = + if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then [] + else if !remaining_stride > 1 then + (* We still have some steps to do *) + (Unsynchronized.dec remaining_stride; ["Skipping because of stride"]) + else + (* This was the last step, now run the action *) + let + val _ = remaining_stride := stride + val _ = Unsynchronized.inc num_sledgehammer_calls + in + if !num_sledgehammer_calls > max_calls then + ["Skipping because max number of calls reached"] + else + let + val meth = Unsynchronized.ref "" + val named_thms = + Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) + val trivial = + if check_trivial then + Try0.try0 (SOME try_timeout) ([], [], [], []) st + handle Timeout.TIMEOUT _ => false + else false + val log1 = + sh_tag ^ catch (fn () => + run_sledgehammer change_data trivial args meth named_thms pos st) + val log2 = + (case ! named_thms of + SOME thms => + [separator, + proof_method_tag (!meth) ^ + catch (fn () => + run_proof_method change_data trivial false name meth thms + timeout pos st)] + | NONE => []) + in log1 :: log2 end + end + in + if null log then [] + else [Mirabelle.log_command command [XML.Text (cat_lines log)]] + end) + + val report = log_data index (! data) + in results @ report end)) + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,183 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML + Author: Jasmin Blanchette, TU Munich + Author: Makarius + +Mirabelle action: "sledgehammer_filter". +*) + +structure Mirabelle_Sledgehammer_Filter: sig end = +struct + +fun get args name default_value = + case AList.lookup (op =) args name of + SOME value => Value.parse_real value + | NONE => default_value + +fun extract_relevance_fudge args + {local_const_multiplier, worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight, + abs_irrel_weight, theory_const_rel_weight, theory_const_irrel_weight, + chained_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus, local_bonus, assum_bonus, + chained_bonus, max_imperfect, max_imperfect_exp, threshold_divisor, ridiculous_threshold} = + {local_const_multiplier = get args "local_const_multiplier" local_const_multiplier, + worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq, + higher_order_irrel_weight = get args "higher_order_irrel_weight" higher_order_irrel_weight, + abs_rel_weight = get args "abs_rel_weight" abs_rel_weight, + abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight, + theory_const_rel_weight = get args "theory_const_rel_weight" theory_const_rel_weight, + theory_const_irrel_weight = get args "theory_const_irrel_weight" theory_const_irrel_weight, + chained_const_irrel_weight = get args "chained_const_irrel_weight" chained_const_irrel_weight, + intro_bonus = get args "intro_bonus" intro_bonus, + elim_bonus = get args "elim_bonus" elim_bonus, + simp_bonus = get args "simp_bonus" simp_bonus, + local_bonus = get args "local_bonus" local_bonus, + assum_bonus = get args "assum_bonus" assum_bonus, + chained_bonus = get args "chained_bonus" chained_bonus, + max_imperfect = get args "max_imperfect" max_imperfect, + max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp, + threshold_divisor = get args "threshold_divisor" threshold_divisor, + ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold} + +structure Prooftab = + Table(type key = int * int val ord = prod_ord int_ord int_ord) + +fun print_int x = Value.print_int (! x) + +fun percentage a b = if b = 0 then "N/A" else Value.print_int (a * 100 div b) +fun percentage_alt a b = percentage a (a + b) + +val default_prover = ATP_Proof.eN (* arbitrary ATP *) + +fun with_index (i, s) = s ^ "@" ^ Value.print_int i + +val proof_fileK = "proof_file" + +val _ = + Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer_filter\ + (fn context => fn commands => + let + val (proof_table, args) = + let + val (pf_args, other_args) = + #arguments context |> List.partition (curry (op =) proof_fileK o fst) + val proof_file = + (case pf_args of + [] => error "No \"proof_file\" specified" + | (_, s) :: _ => s) + fun do_line line = + (case line |> space_explode ":" of + [line_num, offset, proof] => + SOME (apply2 (the o Int.fromString) (line_num, offset), + proof |> space_explode " " |> filter_out (curry (op =) "")) + | _ => NONE) + val proof_table = + File.read (Path.explode proof_file) + |> space_explode "\n" + |> map_filter do_line + |> AList.coalesce (op =) + |> Prooftab.make + in (proof_table, other_args) end + + val num_successes = Unsynchronized.ref 0 + val num_failures = Unsynchronized.ref 0 + val num_found_proofs = Unsynchronized.ref 0 + val num_lost_proofs = Unsynchronized.ref 0 + val num_found_facts = Unsynchronized.ref 0 + val num_lost_facts = Unsynchronized.ref 0 + + val results = + commands |> maps (fn {pos, pre, ...} => + (case (Position.line_of pos, Position.offset_of pos) of + (SOME line_num, SOME offset) => + (case Prooftab.lookup proof_table (line_num, offset) of + SOME proofs => + let + val thy = Proof.theory_of pre + val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre + val prover = AList.lookup (op =) args "prover" |> the_default default_prover + val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args + val default_max_facts = + Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover + val relevance_fudge = + extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge + val subgoal = 1 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt + val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover + val keywords = Thy_Header.get_keywords' ctxt + val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt + val facts = + Sledgehammer_Fact.nearly_all_facts ctxt ho_atp + Sledgehammer_Fact.no_fact_override keywords css_table chained_ths + hyp_ts concl_t + |> Sledgehammer_Fact.drop_duplicate_facts + |> Sledgehammer_MePo.mepo_suggested_facts ctxt params + (the_default default_max_facts max_facts) + (SOME relevance_fudge) hyp_ts concl_t + |> map (fst o fst) + val (found_facts, lost_facts) = + flat proofs |> sort_distinct string_ord + |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) + |> List.partition (curry (op <=) 0 o fst) + |>> sort (prod_ord int_ord string_ord) ||> map snd + val found_proofs = filter (forall (member (op =) facts)) proofs + val n = length found_proofs + val log1 = + if n = 0 then + (Unsynchronized.inc num_failures; "Failure") + else + (Unsynchronized.inc num_successes; + Unsynchronized.add num_found_proofs n; + "Success (" ^ Value.print_int n ^ " of " ^ + Value.print_int (length proofs) ^ " proofs)") + val _ = Unsynchronized.add num_lost_proofs (length proofs - n) + val _ = Unsynchronized.add num_found_facts (length found_facts) + val _ = Unsynchronized.add num_lost_facts (length lost_facts) + val log2 = + if null found_facts then [] + else + let + val found_weight = + Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) + / Real.fromInt (length found_facts) + |> Math.sqrt |> Real.ceil + in + ["Found facts (among " ^ Value.print_int (length facts) ^ + ", weight " ^ Value.print_int found_weight ^ "): " ^ + commas (map with_index found_facts)] + end + val log3 = + if null lost_facts then [] + else + ["Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ + commas lost_facts] + in [XML.Text (cat_lines (log1 :: log2 @ log3))] end + | NONE => [XML.Text "No known proof"]) + | _ => [])) + + val report = + if ! num_successes + ! num_failures > 0 then + let + val props = + [("num_successes", print_int num_successes), + ("num_failures", print_int num_failures), + ("num_found_proofs", print_int num_found_proofs), + ("num_lost_proofs", print_int num_lost_proofs), + ("num_found_facts", print_int num_found_facts), + ("num_lost_facts", print_int num_lost_facts)] + val text = + "\nNumber of overall successes: " ^ print_int num_successes ^ + "\nNumber of overall failures: " ^ print_int num_failures ^ + "\nOverall success rate: " ^ + percentage_alt (! num_successes) (! num_failures) ^ "%" ^ + "\nNumber of found proofs: " ^ print_int num_found_proofs ^ + "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ + "\nProof found rate: " ^ + percentage_alt (! num_found_proofs) (! num_lost_proofs) ^ "%" ^ + "\nNumber of found facts: " ^ print_int num_found_facts ^ + "\nNumber of lost facts: " ^ print_int num_lost_facts ^ + "\nFact found rate: " ^ + percentage_alt (! num_found_facts) (! num_lost_facts) ^ "%" + in [Mirabelle.log_report props [XML.Text text]] end + else [] + in results @ report end)) + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,17 @@ +(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML + Author: Jasmin Blanchette, TU Munich + Author: Makarius + +Mirabelle action: "try0". +*) + +structure Mirabelle_Try0 : sig end = +struct + +val _ = + Theory.setup (Mirabelle.command_action \<^binding>\try0\ + (fn {timeout, ...} => fn {pre, ...} => + if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre + then "succeeded" else "")); + +end diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat May 15 22:39:07 2021 +0200 @@ -10,6 +10,7 @@ val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params + val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = @@ -353,7 +354,8 @@ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] -val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] +val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) @@ -366,7 +368,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" - (Scan.optional Parse.name runN -- parse_params + (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof @@ -374,7 +376,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" - (parse_params >> (fn params => + (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params Normal thy) of diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Sat May 15 22:39:07 2021 +0200 @@ -0,0 +1,76 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2010, 2011 + +Sledgehammer as a tactic. +*) + +signature SLEDGEHAMMER_TACTICS = +sig + type fact_override = Sledgehammer_Fact.fact_override + + val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override -> + thm list -> int -> tactic + val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override -> + thm list -> int -> tactic +end; + +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = +struct + +open Sledgehammer_Util +open Sledgehammer_Fact +open Sledgehammer_Prover +open Sledgehammer_Prover_ATP +open Sledgehammer_Prover_Minimize +open Sledgehammer_MaSh +open Sledgehammer_Commands + +fun run_prover override_params fact_override chained i n ctxt goal = + let + val thy = Proof_Context.theory_of ctxt + val mode = Normal + val params as {provers, max_facts, ...} = default_params thy override_params + val name = hd provers + val prover = get_prover ctxt mode name + val default_max_facts = default_max_facts_of_prover ctxt name + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt + val ho_atp = exists (is_ho_atp ctxt) provers + val keywords = Thy_Header.get_keywords' ctxt + val css_table = clasimpset_rule_table_of ctxt + val facts = + nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t + |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override + hyp_ts concl_t + |> hd |> snd + val problem = + {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, + factss = [("", facts)], found_proof = I} + in + (case prover params problem of + {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME + | _ => NONE) + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) + end + +fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th = + let val override_params = override_params @ [("preplay_timeout", "0")] in + (case run_prover override_params fact_override chained i i ctxt th of + SOME facts => + Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt + (maps (thms_of_name ctxt) facts) i th + | NONE => Seq.empty) + end + +fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th = + let + val override_params = + override_params @ + [("preplay_timeout", "0"), + ("minimize", "false")] + val xs = run_prover override_params fact_override chained i i ctxt th + in + if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty + end + +end; diff -r 60a788467639 -r c74e25de3c00 src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Fri May 14 12:43:19 2021 +0100 +++ b/src/HOL/Tools/etc/options Sat May 15 22:39:07 2021 +0200 @@ -46,3 +46,15 @@ public option kodkod_max_threads : int = 0 -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" + + +section "Mirabelle" + +option mirabelle_timeout : real = 30 + -- "default timeout for Mirabelle actions" + +option mirabelle_actions : string = "" + -- "Mirabelle actions (outer syntax, separated by semicolons)" + +option mirabelle_theories : string = "" + -- "Mirabelle theories (names with optional line range, separated by commas)" diff -r 60a788467639 -r c74e25de3c00 src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Concurrent/par_list.ML Sat May 15 22:39:07 2021 +0200 @@ -16,7 +16,7 @@ signature PAR_LIST = sig - val map_name: string -> ('a -> 'b) -> 'a list -> 'b list + val map': {name: string, sequential: bool} -> ('a -> 'b) -> 'a list -> 'b list val map_independent: ('a -> 'b) -> 'a list -> 'b list val map: ('a -> 'b) -> 'a list -> 'b list val get_some: ('a -> 'b option) -> 'a list -> 'b option @@ -28,20 +28,22 @@ structure Par_List: PAR_LIST = struct -fun forked_results name f xs = - if Future.relevant xs - then Future.forked_results {name = name, deps = []} (map (fn x => fn () => f x) xs) - else map (Exn.capture f) xs; +fun managed_results {name, sequential} f xs = + if sequential orelse not (Future.relevant xs) then map (Exn.capture f) xs + else + Future.forked_results + {name = if name = "" then "Par_List.map" else name, deps = []} + (map (fn x => fn () => f x) xs); -fun map_name name f xs = Par_Exn.release_first (forked_results name f xs); -fun map f = map_name "Par_List.map" f; +fun map' params f xs = Par_Exn.release_first (managed_results params f xs); +fun map f = map' {name = "", sequential = false} f; fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all; fun get_some f xs = let exception FOUND of 'b; val results = - forked_results "Par_List.get_some" + managed_results {name = "Par_List.get_some", sequential = false} (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs; in (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of diff -r 60a788467639 -r c74e25de3c00 src/Pure/Concurrent/unsynchronized.ML --- a/src/Pure/Concurrent/unsynchronized.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Concurrent/unsynchronized.ML Sat May 15 22:39:07 2021 +0200 @@ -13,6 +13,7 @@ val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b val inc: int ref -> int val dec: int ref -> int + val add: int ref -> int -> int val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c end; @@ -29,6 +30,7 @@ fun inc i = (i := ! i + (1: int); ! i); fun dec i = (i := ! i - (1: int); ! i); +fun add i n = (i := ! i + (n: int); ! i); fun setmp flag value f x = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => diff -r 60a788467639 -r c74e25de3c00 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/General/path.scala Sat May 15 22:39:07 2021 +0200 @@ -220,6 +220,7 @@ def thy: Path = ext("thy") def tar: Path = ext("tar") def gz: Path = ext("gz") + def log: Path = ext("log") def backup: Path = { diff -r 60a788467639 -r c74e25de3c00 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Isar/parse.ML Sat May 15 22:39:07 2021 +0200 @@ -61,7 +61,6 @@ val and_list1': 'a context_parser -> 'a list context_parser val list: 'a parser -> 'a list parser val list1: 'a parser -> 'a list parser - val properties: Properties.T parser val name: string parser val name_range: (string * Position.range) parser val name_position: (string * Position.T) parser @@ -259,8 +258,6 @@ fun list1 scan = enum1 "," scan; fun list scan = enum "," scan; -val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")"); - (* names and embedded content *) diff -r 60a788467639 -r c74e25de3c00 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat May 15 22:39:07 2021 +0200 @@ -1532,15 +1532,13 @@ fun print_cases_proof ctxt0 ctxt = let - val print_name = Token.print_name (Thy_Header.get_keywords' ctxt); - fun trim_name x = if Name.is_internal x then Name.clean x else "_"; val trim_names = map trim_name #> drop_suffix (equal "_"); fun print_case name xs = (case trim_names xs of - [] => print_name name - | xs' => enclose "(" ")" (space_implode " " (map print_name (name :: xs')))); + [] => print_name ctxt name + | xs' => enclose "(" ")" (space_implode " " (map (print_name ctxt) (name :: xs')))); fun is_case x t = x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t); diff -r 60a788467639 -r c74e25de3c00 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Isar/token.ML Sat May 15 22:39:07 2021 +0200 @@ -93,6 +93,7 @@ val explode: Keyword.keywords -> Position.T -> string -> T list val explode0: Keyword.keywords -> string -> T list val print_name: Keyword.keywords -> string -> string + val print_properties: Keyword.keywords -> Properties.T -> string val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T val make_int: int -> T list @@ -698,13 +699,16 @@ fun explode0 keywords = explode keywords Position.none; -(* print name in parsable form *) +(* print names in parsable form *) fun print_name keywords name = ((case explode keywords Position.none name of [tok] => not (member (op =) [Ident, Long_Ident, Sym_Ident, Nat] (kind_of tok)) | _ => true) ? Symbol_Pos.quote_string_qq) name; +fun print_properties keywords = + map (apply2 (print_name keywords) #> (fn (a, b) => a ^ " = " ^ b)) #> commas #> enclose "[" "]"; + (* make *) diff -r 60a788467639 -r c74e25de3c00 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat May 15 22:39:07 2021 +0200 @@ -79,7 +79,6 @@ val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b - val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state @@ -88,7 +87,7 @@ val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result - val join_results: result -> (transition * state) list + val join_results: result -> (state * transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; @@ -602,19 +601,6 @@ Position.setmp_thread_data pos f x; -(* post-transition hooks *) - -local - val hooks = - Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); -in - -fun add_hook hook = Synchronized.change hooks (cons hook); -fun get_hooks () = Synchronized.value hooks; - -end; - - (* apply transitions *) local @@ -634,7 +620,6 @@ val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); - val _ = get_hooks () |> List.app (fn f => ignore \<^try>\f tr st st'\); in (st', opt_err') end; end; @@ -693,9 +678,16 @@ Result_List of result list | Result_Future of result future; -fun join_results (Result x) = [x] - | join_results (Result_List xs) = maps join_results xs - | join_results (Result_Future x) = join_results (Future.join x); +fun join_results result = + let + fun add (tr, st') res = + (case res of + [] => [(init_toplevel (), tr, st')] + | (_, _, st) :: _ => (st, tr, st') :: res); + fun acc (Result r) = add r + | acc (Result_List rs) = fold acc rs + | acc (Result_Future x) = acc (Future.join x); + in rev (acc result []) end; local diff -r 60a788467639 -r c74e25de3c00 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/PIDE/document.ML Sat May 15 22:39:07 2021 +0200 @@ -738,13 +738,18 @@ if Options.bool options "editor_presentation" then let val (_, offsets, rev_segments) = - iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => + iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) => (case opt_exec of SOME (eval, _) => let val command_id = Command.eval_command_id eval; val span = the_command_span command_id; + val st = + (case try (#1 o the o the_entry node o the) prev of + NONE => Toplevel.init_toplevel () + | SOME prev_eval => Command.eval_result_state prev_eval); + val exec_id = Command.eval_exec_id eval; val tr = Command.eval_result_command eval; val st' = Command.eval_result_state eval; @@ -753,14 +758,15 @@ val offsets' = offsets |> Inttab.update (command_id, offset) |> Inttab.update (exec_id, offset); - val segments' = (span, tr, st') :: segments; + val segments' = (span, (st, tr, st')) :: segments; in SOME (offset', offsets', segments') end | NONE => NONE)) node (0, Inttab.empty, []); val adjust = Inttab.lookup offsets; val segments = - rev rev_segments |> map (fn (span, tr, st') => - {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); + rev rev_segments |> map (fn (span, (st, tr, st')) => + {span = Command_Span.adjust_offsets adjust span, + prev_state = st, command = tr, state = st'}); val presentation_context: Thy_Info.presentation_context = {options = options, diff -r 60a788467639 -r c74e25de3c00 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Sat May 15 22:39:07 2021 +0200 @@ -421,10 +421,9 @@ (Syntax.check_term (Proof_Context.allow_dummies ctxt) (constrain t); Exn.Res t) handle exn as ERROR _ => Exn.Exn exn; + fun par_map xs = Par_List.map' {name = "Syntax_Phases.parse_term", sequential = false} xs; val results' = - if parsed_len > 1 then - (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res) - check results + if parsed_len > 1 then (grouped 10 par_map o apsnd o Exn.maps_res) check results else results; val reports' = fst (hd results'); diff -r 60a788467639 -r c74e25de3c00 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/System/isabelle_tool.scala Sat May 15 22:39:07 2021 +0200 @@ -209,6 +209,7 @@ Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, + isabelle.mirabelle.Mirabelle.isabelle_tool, isabelle.vscode.TextMate_Grammar.isabelle_tool, isabelle.vscode.Language_Server.isabelle_tool) diff -r 60a788467639 -r c74e25de3c00 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Thy/export.scala Sat May 15 22:39:07 2021 +0200 @@ -82,7 +82,8 @@ def message(msg: String, theory_name: String, name: String): String = msg + " " + quote(name) + " for theory " + quote(theory_name) - def compound_name(a: String, b: String): String = a + ":" + b + def compound_name(a: String, b: String): String = + if (a.isEmpty) b else a + ":" + b def empty_entry(theory_name: String, name: String): Entry = Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none) diff -r 60a788467639 -r c74e25de3c00 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat May 15 22:39:07 2021 +0200 @@ -55,8 +55,14 @@ fun merge data : T = Library.merge (eq_snd op =) data; ); +fun sequential_presentation options = + not (Options.bool options \<^system_option>\parallel_presentation\); + fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); + Par_List.map' + {name = "apply_presentation", sequential = sequential_presentation (#options context)} + (fn (f, _) => f context thy) (Presentation.get thy) + |> ignore; fun add_presentation f = Presentation.map (cons (f, stamp ())); @@ -257,7 +263,9 @@ val results2 = futures |> map_filter (Exn.get_res o Future.join_result) |> sort result_ord - |> Par_List.map (fn result => Exn.capture (result_present result) ()); + |> Par_List.map' + {name = "present", sequential = sequential_presentation (Options.default ())} + (fn result => Exn.capture (result_present result) ()); (* FIXME more precise commit order (!?) *) val results3 = futures @@ -311,8 +319,9 @@ fun present () = let - val segments = (spans ~~ maps Toplevel.join_results results) - |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); + val segments = + (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) => + {span = span, prev_state = st, command = tr, state = st'}); val context: presentation_context = {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; in apply_presentation context thy end; diff -r 60a788467639 -r c74e25de3c00 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat May 15 22:39:07 2021 +0200 @@ -10,7 +10,9 @@ val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text list val output_source: Proof.context -> string -> Latex.text list - type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state} + type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state} val present_thy: Options.T -> theory -> segment list -> Latex.text list val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T @@ -357,7 +359,9 @@ in -type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}; +type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state}; fun present_thy options thy (segments: segment list) = let diff -r 60a788467639 -r c74e25de3c00 src/Pure/build-jars --- a/src/Pure/build-jars Fri May 14 12:43:19 2021 +0100 +++ b/src/Pure/build-jars Sat May 15 22:39:07 2021 +0200 @@ -11,6 +11,7 @@ declare -a SOURCES=( src/HOL/SPARK/Tools/spark.scala src/HOL/Tools/ATP/system_on_tptp.scala + src/HOL/Tools/Mirabelle/mirabelle.scala src/HOL/Tools/Nitpick/kodkod.scala src/Pure/Admin/afp.scala src/Pure/Admin/build_csdp.scala