reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
--- a/etc/components Thu May 13 15:52:10 2021 +0200
+++ b/etc/components Fri May 14 21:32:11 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
--- a/etc/options Thu May 13 15:52:10 2021 +0200
+++ b/etc/options Fri May 14 21:32:11 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)"
--- a/src/HOL/Main.thy Thu May 13 15:52:10 2021 +0200
+++ b/src/HOL/Main.thy Fri May 14 21:32:11 2021 +0200
@@ -9,6 +9,7 @@
imports
Predicate_Compile
Quickcheck_Narrowing
+ Mirabelle
Extraction
Nunchaku
BNF_Greatest_Fixpoint
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle.thy Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,19 @@
+(* Title: HOL/Mirabelle.thy
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
+*)
+
+theory Mirabelle
+ imports Sledgehammer Predicate_Compile
+begin
+
+ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
+(*
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
+*)
+ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
+
+end
--- a/src/HOL/Mirabelle/Mirabelle.thy Thu May 13 15:52:10 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOL/Mirabelle/Mirabelle.thy
- Author: Jasmin Blanchette and Sascha Boehme, TU Munich
-*)
-
-theory Mirabelle
-imports Main
-begin
-
-ML_file \<open>Tools/mirabelle.ML\<close>
-
-ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
-
-ML \<open>
-signature MIRABELLE_ACTION =
-sig
- val invoke : (string * string) list -> theory -> theory
-end
-\<close>
-
-end
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Thu May 13 15:52:10 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: HOL/Mirabelle/Mirabelle_Test.thy
- Author: Sascha Boehme, TU Munich
-*)
-
-section \<open>Simple test theory for Mirabelle actions\<close>
-
-theory Mirabelle_Test
-imports Main Mirabelle
-begin
-
-ML_file \<open>Tools/mirabelle_arith.ML\<close>
-ML_file \<open>Tools/mirabelle_metis.ML\<close>
-ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
-ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
-ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
-ML_file \<open>Tools/mirabelle_try0.ML\<close>
-
-text \<open>
- Only perform type-checking of the actions,
- any reasonable test would be too complicated.
-\<close>
-
-end
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu May 13 15:52:10 2021 +0200
+++ /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>\<open>mirabelle_logfile\<close> (K "")
-val timeout = Attrib.setup_config_int \<^binding>\<open>mirabelle_timeout\<close> (K 30)
-val start_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_start_line\<close> (K 0)
-val end_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_end_line\<close> (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 exn_log tag id e = tag id ^ "exception:\n" ^ General.exnMessage e
-
-fun catch tag f id (args: run_args) = f id args
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn else #log args (exn_log tag id exn)
-
-fun catch_result tag default f id (args: run_args) = f id args
- handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn else (#log args (exn_log tag id exn); default)
-
-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
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu May 13 15:52:10 2021 +0200
+++ /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;
--- a/src/HOL/Mirabelle/Tools/mirabelle_try0.ML Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/etc/settings Thu May 13 15:52:10 2021 +0200
+++ /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"
--- a/src/HOL/Mirabelle/ex/Ex.thy Thu May 13 15:52:10 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-theory Ex imports Pure
-begin
-
-ML \<open>
- 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 ();
-\<close> \<comment> \<open>some arbitrary small test case\<close>
-
-end
-
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Thu May 13 15:52:10 2021 +0200
+++ /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
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Thu May 13 15:52:10 2021 +0200
+++ /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 <<END;
-theory "$setup_thy_name"
-imports "$mirabelle_thy" "$mirabelle_theory"
-begin
-
-$tools
-
-setup {*
- Config.put_global Mirabelle.logfile "$log_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 = <OLD_FILE>;
-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);
--- a/src/HOL/ROOT Thu May 13 15:52:10 2021 +0200
+++ b/src/HOL/ROOT Fri May 14 21:32:11 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]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,241 @@
+(* 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 = {tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}
+ type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
+ val command_result: command -> XML.body -> XML.tree
+ val print_exn: exn -> string
+ val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory
+ 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 print_action name [] = name
+ | print_action name arguments = name ^ " " ^ print_properties arguments;
+
+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 = {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;
+
+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 = {tag = tag, arguments = arguments, timeout = timeout, theory = thy};
+ val export_body = action context commands;
+ val export_head =
+ XML.Elem (("action", (Markup.nameN, name) :: arguments),
+ [XML.Text (print_action name arguments)]);
+ val export_path = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index));
+ in Export.export thy export_path (export_head :: export_body) end;
+
+
+(* command action *)
+
+fun command_result ({name, pos, ...}: command) body =
+ XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body);
+
+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 (command_result 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>\<open>mirabelle_timeout\<close>;
+ val mirabelle_actions = Options.string options \<^system_option>\<open>mirabelle_actions\<close>;
+ val mirabelle_theories = Options.string options \<^system_option>\<open>mirabelle_theories\<close>;
+
+ 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,264 @@
+/* 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 content */
+
+ val separator = "------------------\n"
+
+ def mirabelle_path(index: Int): String = "mirabelle/" + index
+
+ object Action
+ {
+ def get(export_name: String, xml: XML.Tree): Action =
+ xml match {
+ case XML.Elem(Markup("action", (Markup.NAME, name) :: arguments), body) =>
+ Action(name, arguments, body)
+ case _ =>
+ error("Expected action in export " + quote(export_name) + "\nmalformed XML: " + xml)
+ }
+ }
+ case class Action(name: String, arguments: Properties.T, body: XML.Body)
+ {
+ def print: String = XML.content(body)
+ }
+
+ object Command
+ {
+ def get(export_name: String, xml: XML.Tree): Command =
+ xml match {
+ case XML.Elem(Markup("command", (Markup.NAME, name) :: props), result) =>
+ Command(name, props.filter(Markup.position_property), result)
+ case _ =>
+ error("Expected command in export " + quote(export_name) + "\nmalformed XML: " + xml)
+ }
+ }
+ sealed case class Command(name: String, pos: Properties.T, result: XML.Body)
+ {
+ def print_head: String =
+ {
+ val line = Position.Line.get(pos)
+ val offset = Position.Offset.get(pos)
+ val loc = line.toString + ":" + offset.toString
+ "at " + loc + " (" + name + "):\n"
+ }
+ def print_body: String = Pretty.string_of(result)
+ def print: String = "\n\n" + print_head + separator + print_body
+ }
+
+
+ /* 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 =
+ {
+ val build_options =
+ options + "parallel_presentation=false" +
+ ("mirabelle_actions=" + actions.mkString(";")) +
+ ("mirabelle_theories=" + theories.mkString(","))
+
+ 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, mirabelle_path(index))
+ body = export.uncompressed_yxml
+ if body.nonEmpty
+ } {
+ seen_theories += theory
+ val export_name = Export.compound_name(theory, mirabelle_path(index))
+ val (action, commands) =
+ (Action.get(export_name, body.head), body.tail.map(Command.get(export_name, _)))
+ val dir = Isabelle_System.make_directory(output_dir + Path.basic(theory))
+ val log_file = dir + Path.basic("mirabelle" + index).log
+ progress.echo("Writing " + log_file)
+ File.write(log_file, terminate_lines(action.print :: commands.map(_.print)))
+ }
+ })
+ }
+
+ build_results
+ }
+
+
+ /* 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) error("Missing actions (option -A)")
+
+ 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)
+ })
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Fri May 14 21:32:11 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>\<open>arith\<close>
+ (fn {timeout, ...} => fn {pre, ...} =>
+ if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
+ then "succeeded" else ""));
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML Fri May 14 21:32:11 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>\<open>metis\<close>
+ (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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Fri May 14 21:32:11 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>\<open>quickcheck\<close>
+ (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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,660 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
+ Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
+
+Mirabelle action: "sledgehammer".
+*)
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,180 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
+ Author: Jasmin Blanchette, TU Munich
+
+Mirabelle action: "sledgehammer_filter".
+*)
+
+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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Fri May 14 21:32:11 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>\<open>try0\<close>
+ (fn {timeout, ...} => fn {pre, ...} =>
+ if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
+ then "succeeded" else ""));
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu May 13 15:52:10 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri May 14 21:32:11 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>\<open>=\<close> |-- 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>\<open>sledgehammer\<close>
"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>\<open>sledgehammer_params\<close>
"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
--- a/src/HOL/Tools/etc/options Thu May 13 15:52:10 2021 +0200
+++ b/src/HOL/Tools/etc/options Fri May 14 21:32:11 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)"
--- a/src/Pure/General/path.scala Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/General/path.scala Fri May 14 21:32:11 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 =
{
--- a/src/Pure/Isar/token.ML Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/Isar/token.ML Fri May 14 21:32:11 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 *)
--- a/src/Pure/Isar/toplevel.ML Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri May 14 21:32:11 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
@@ -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>\<open>f tr st st'\<close>);
in (st', opt_err') end;
end;
--- a/src/Pure/System/isabelle_tool.scala Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/System/isabelle_tool.scala Fri May 14 21:32:11 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)
--- a/src/Pure/Thy/thy_info.ML Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML Fri May 14 21:32:11 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>\<open>parallel_presentation\<close>);
+
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
--- a/src/Pure/build-jars Thu May 13 15:52:10 2021 +0200
+++ b/src/Pure/build-jars Fri May 14 21:32:11 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