diff --git a/src/HOL/Tools/Mirabelle/mirabelle.ML b/src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML @@ -1,252 +1,264 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML Author: Jasmin Blanchette and Sascha Boehme, TU Munich Author: Makarius *) signature MIRABELLE = sig (*core*) val print_name: string -> string val print_properties: Properties.T -> string type context = {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory} type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} val theory_action: binding -> (context -> command list -> XML.body) -> theory -> theory val log_command: command -> XML.body -> XML.tree val log_report: Properties.T -> XML.body -> XML.tree val print_exn: exn -> string val command_action: binding -> (context -> command -> string) -> theory -> theory (*utility functions*) val can_apply : Time.time -> (Proof.context -> int -> tactic) -> Proof.state -> bool val theorems_in_proof_term : theory -> thm -> thm list val theorems_of_sucessful_proof: Toplevel.state -> thm list val get_argument : (string * string) list -> string * string -> string val get_int_argument : (string * string) list -> string * int -> int val get_bool_argument : (string * string) list -> string * bool -> bool val cpu_time : ('a -> 'b) -> 'a -> 'b * int end structure Mirabelle : MIRABELLE = struct (** Mirabelle core **) (* concrete syntax *) val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>); val print_name = Token.print_name keywords; val print_properties = Token.print_properties keywords; fun read_actions str = Token.read_body keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) (Symbol_Pos.explode0 str); (* actions *) type command = {name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; type context = {index: int, tag: string, arguments: Properties.T, timeout: Time.time, theory: theory}; structure Data = Theory_Data ( type T = (context -> command list -> XML.body) Name_Space.table; val empty = Name_Space.empty_table "mirabelle_action"; val extend = I; val merge = Name_Space.merge_tables; ); fun theory_action binding action thy = let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); in thy |> Data.map (#2 o Name_Space.define context true (binding, action)) end; (* log content *) fun log_action name arguments = XML.Elem (("action", (Markup.nameN, name) :: arguments), [XML.Text (print_name name ^ (if null arguments then "" else " " ^ print_properties arguments))]); fun log_command ({name, pos, ...}: command) body = XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); fun log_report props body = XML.Elem (("report", props), body); (* apply actions *) fun apply_action index name arguments timeout commands thy = let val action = #2 (Name_Space.check (Context.Theory thy) (Data.get thy) (name, Position.none)); val tag = "#" ^ Value.print_int index ^ " " ^ name ^ ": "; val context = {index = index, tag = tag, arguments = arguments, timeout = timeout, theory = thy}; val export_body = action context commands; val export_head = log_action name arguments; val export_name = Path.binding0 (Path.basic "mirabelle" + Path.basic (Value.print_int index)); in if null export_body then () else Export.export thy export_name (export_head :: export_body) end; fun print_exn exn = (case exn of Timeout.TIMEOUT _ => "timeout" | ERROR msg => "error: " ^ msg | exn => "exception:\n" ^ General.exnMessage exn); fun command_action binding action = let fun apply context command = let val s = action context command handle exn => if Exn.is_interrupt exn then Exn.reraise exn else #tag context ^ print_exn exn; in if s = "" then NONE else SOME (log_command command [XML.Text s]) end; in theory_action binding (map_filter o apply) end; (* theory line range *) local val theory_name = Scan.many1 (Symbol_Pos.symbol #> (fn s => Symbol.not_eof s andalso s <> "[")) >> Symbol_Pos.content; val line = Symbol_Pos.scan_nat >> (Symbol_Pos.content #> Value.parse_nat); val end_line = Symbol_Pos.$$ ":" |-- line; val range = Symbol_Pos.$$ "[" |-- line -- Scan.option end_line --| Symbol_Pos.$$ "]"; in fun read_theory_range str = (case Scan.read Symbol_Pos.stopper (theory_name -- Scan.option range) (Symbol_Pos.explode0 str) of SOME res => res | NONE => error ("Malformed specification of theory line range: " ^ quote str)); end; fun check_theories strs = let val theories = map read_theory_range strs; fun get_theory name = if null theories then SOME NONE else get_first (fn (a, b) => if a = name then SOME b else NONE) theories; fun check_line NONE _ = false | check_line _ NONE = true | check_line (SOME NONE) _ = true | check_line (SOME (SOME (line, NONE))) (SOME i) = line <= i | check_line (SOME (SOME (line, SOME end_line))) (SOME i) = line <= i andalso i <= end_line; fun check_pos range = check_line range o Position.line_of; in check_pos o get_theory end; (* presentation hook *) val whitelist = ["apply", "by", "proof"]; +fun filter_index f = + let + fun filter_aux _ [] = [] + | filter_aux n (x :: xs) = + if f (n, x) then x :: filter_aux (n + 1) xs else filter_aux (n + 1) xs + in + filter_aux 0 + end + val _ = Theory.setup (Thy_Info.add_presentation (fn context => fn thy => let val {options, adjust_pos, segments, ...} = context; val mirabelle_timeout = Options.seconds options \<^system_option>\mirabelle_timeout\; + val mirabelle_stride = Options.int options \<^system_option>\mirabelle_stride\; val mirabelle_actions = Options.string options \<^system_option>\mirabelle_actions\; val mirabelle_theories = Options.string options \<^system_option>\mirabelle_theories\; val actions = (case read_actions mirabelle_actions of SOME actions => actions | NONE => error ("Failed to parse mirabelle_actions: " ^ quote mirabelle_actions)); val check = check_theories (space_explode "," mirabelle_theories); val commands = - segments |> map_filter (fn {command = tr, prev_state = st, state = st', ...} => + 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); + end) + |> filter_index (fn (n, _) => n mod mirabelle_stride = 0); fun apply (i, (name, arguments)) () = apply_action (i + 1) name arguments mirabelle_timeout commands thy; in if null commands then () else fold_index apply actions () end)); (* Mirabelle utility functions *) fun can_apply time tac st = let val {context = ctxt, facts, goal} = Proof.goal st; val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt); in (case try (Timeout.apply time (Seq.pull o full_tac)) goal of SOME (SOME _) => true | _ => false) end; local fun fold_body_thms f = let fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => fn (x, seen) => if Inttab.defined seen i then (x, seen) else let val name = Proofterm.thm_node_name thm_node; val prop = Proofterm.thm_node_prop thm_node; val body = Future.join (Proofterm.thm_node_body thm_node); val (x', seen') = app (n + (if name = "" then 0 else 1)) body (x, Inttab.update (i, ()) seen); in (x' |> n = 0 ? f (name, prop, body), seen') end); in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end; in fun theorems_in_proof_term thy thm = let val all_thms = Global_Theory.all_thms_of thy true; fun collect (s, _, _) = if s <> "" then insert (op =) s else I; fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE; fun resolve_thms names = map_filter (member_of names) all_thms; in resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) end; end; fun theorems_of_sucessful_proof st = (case try Toplevel.proof_of st of NONE => [] | SOME prf => theorems_in_proof_term (Proof.theory_of prf) (#goal (Proof.goal prf))); fun get_argument arguments (key, default) = the_default default (AList.lookup (op =) arguments key); fun get_int_argument arguments (key, default) = (case Option.map Int.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun get_bool_argument arguments (key, default) = (case Option.map Bool.fromString (AList.lookup (op =) arguments key) of SOME (SOME i) => i | SOME NONE => error ("bad option: " ^ key) | NONE => default); fun cpu_time f x = let val ({cpu, ...}, y) = Timing.timing f x in (y, Time.toMilliseconds cpu) end; end diff --git a/src/HOL/Tools/Mirabelle/mirabelle.scala b/src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala @@ -1,273 +1,276 @@ /* Title: HOL/Tools/Mirabelle/mirabelle.scala Author: Makarius Isabelle/Scala front-end for Mirabelle. */ package isabelle.mirabelle import isabelle._ object Mirabelle { /* actions and options */ def action_names(): List[String] = { val Pattern = """Mirabelle action: "(\w+)".*""".r (for { file <- File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file, pred = _.getName.endsWith(".ML")) line <- split_lines(File.read(file)) name <- line match { case Pattern(a) => Some(a) case _ => None } } yield name).sorted } def sledgehammer_options(): List[String] = { val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))). flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None }) } /* exported log content */ object Log { def export_name(index: Int, theory: String = ""): String = Export.compound_name(theory, "mirabelle/" + index) val separator = "\n------------------\n" sealed abstract class Entry { def print: String } case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry { def print: String = "action: " + XML.content(body) + separator } case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry { def print: String = "\n" + print_head + separator + Pretty.string_of(body) def print_head: String = { val line = Position.Line.get(position) val offset = Position.Offset.get(position) val loc = line.toString + ":" + offset.toString "at " + loc + " (" + name + "):" } } case class Report(result: Properties.T, body: XML.Body) extends Entry { override def print: String = "\n" + separator + Pretty.string_of(body) } def entry(export_name: String, xml: XML.Tree): Entry = xml match { case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) => Action(name, props, body) case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) => Command(name, props.filter(Markup.position_property), body) case XML.Elem(Markup("report", props), body) => Report(props, body) case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml) } } /* main mirabelle */ def mirabelle( options: Options, actions: List[String], output_dir: Path, theories: List[String] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, progress: Progress = new Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, numa_shuffling: Boolean = false, max_jobs: Int = 1, verbose: Boolean = false): Build.Results = { require(!selection.requirements) progress.echo("Building required heaps ...") val build_results0 = Build.build(options, build_heap = true, selection = selection.copy(requirements = true), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) if (build_results0.ok) { val build_options = options + "timeout_build=false" + "parallel_presentation=false" + ("mirabelle_actions=" + actions.mkString(";")) + ("mirabelle_theories=" + theories.mkString(",")) progress.echo("Running Mirabelle ...") val build_results = Build.build(build_options, clean_build = true, selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose) if (build_results.ok) { val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) val store = Sessions.store(build_options) using(store.open_database_context())(db_context => { var seen_theories = Set.empty[String] for { session <- structure.imports_selection(selection).iterator session_hierarchy = structure.hierarchy(session) theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a))) theory <- theories if !seen_theories(theory) index <- 1 to actions.length export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index)) body = export.uncompressed_yxml if body.nonEmpty } { seen_theories += theory val export_name = Log.export_name(index, theory = theory) val log = body.map(Log.entry(export_name, _)) val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory)) val log_file = log_dir + Path.basic("mirabelle" + index).log progress.echo("Writing " + log_file) File.write(log_file, terminate_lines(log.map(_.print))) } }) } build_results } else build_results0 } /* Isabelle tool wrapper */ val default_output_dir: Path = Path.explode("mirabelle") val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools", Scala_Project.here, args => { val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var actions: List[String] = Nil var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false var output_dir = default_output_dir var requirements = false var theories: List[String] = Nil var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var max_jobs = 1 var options = Options.init(opts = build_options) var verbose = false var exclude_sessions: List[String] = Nil + val default_stride = options.int("mirabelle_stride") 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 + """, + -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) + -s INT run actions on every nth goal (default """ + default_stride + """) -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), + "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)), "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) if (actions.isEmpty) getopts.usage() val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() if (verbose) { progress.echo("Started at " + Build_Log.print_date(start_date)) } val results = progress.interrupt_handler { mirabelle(options, actions, output_dir, theories = theories, selection = Sessions.Selection( requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions), progress = progress, dirs = dirs, select_dirs = select_dirs, numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), max_jobs = max_jobs, verbose = verbose) } val end_date = Date.now() val elapsed_time = end_date.time - start_date.time if (verbose) { progress.echo("\nFinished at " + Build_Log.print_date(end_date)) } val total_timing = results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). copy(elapsed = elapsed_time) progress.echo(total_timing.message_resources) sys.exit(results.rc) }) } diff --git a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML @@ -1,684 +1,675 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich Author: Makarius Mirabelle action: "sledgehammer". *) structure Mirabelle_Sledgehammer: sig end = struct (*To facilitate synching the description of Mirabelle Sledgehammer parameters (in ../lib/Tools/mirabelle) with the parameters actually used by this interface, the former extracts PARAMETER and DESCRIPTION from code below which has this pattern (provided it appears in a single line): val .*K = "PARAMETER" (*DESCRIPTION*) *) (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *) val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*) val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*) val fact_filterK = "fact_filter" (*=STRING: fact filter*) val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*) val isar_proofsK = "isar_proofs" (*=SMART_BOOL: enable Isar proof generation*) val keepK = "keep" (*=PATH: path where to keep temporary files created by sledgehammer*) val lam_transK = "lam_trans" (*=STRING: lambda translation scheme*) val max_callsK = "max_calls" (*=NUM: max. no. of calls to sledgehammer*) val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*) val max_mono_itersK = "max_mono_iters" (*=NUM: max. iterations of monomorphiser*) val max_new_mono_instancesK = "max_new_mono_instances" (*=NUM: max. new monomorphic instances*) val max_relevantK = "max_relevant" (*=NUM: max. relevant clauses to use*) val minimizeK = "minimize" (*=BOOL: instruct sledgehammer to run its minimizer*) val preplay_timeoutK = "preplay_timeout" (*=TIME: timeout for finding reconstructed proof*) val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (ie. using metis/smt)*) val proverK = "prover" (*=STRING: name of the external prover to call*) val prover_timeoutK = "prover_timeout" (*=TIME: timeout for invoked ATP (seconds of process time)*) val sliceK = "slice" (*=BOOL: allow sledgehammer-level strategy-scheduling*) val smt_proofsK = "smt_proofs" (*=BOOL: enable SMT proof generation*) val strictK = "strict" (*=BOOL: run in strict mode*) -val strideK = "stride" (*=NUM: run every nth goal*) val term_orderK = "term_order" (*=STRING: term order (in E)*) val type_encK = "type_enc" (*=STRING: type encoding scheme*) val uncurried_aliasesK = "uncurried_aliases" (*=SMART_BOOL: use fresh function names to alias curried applications*) val separator = "-----" (*FIXME sensible to have Mirabelle-level Sledgehammer defaults?*) (*defaults used in this Mirabelle action*) val preplay_timeout_default = "1" val lam_trans_default = "smart" val uncurried_aliases_default = "smart" val fact_filter_default = "smart" val type_enc_default = "smart" val strict_default = "false" -val stride_default = 1 val max_facts_default = "smart" val slice_default = "true" val max_calls_default = 10000000 val check_trivial_default = false (*If a key is present in args then augment a list with its pair*) (*This is used to avoid fixing default values at the Mirabelle level, and instead use the default values of the tool (Sledgehammer in this case).*) fun available_parameter args key label list = let val value = AList.lookup (op =) args key in if is_some value then (label, the value) :: list else list end datatype sh_data = ShData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, lemmas: int, max_lems: int, time_isa: int, time_prover: int, time_prover_fail: int} datatype re_data = ReData of { calls: int, success: int, nontriv_calls: int, nontriv_success: int, proofs: int, time: int, timeout: int, lemmas: int * int * int, posns: (Position.T * bool) list } fun make_sh_data (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa, time_prover,time_prover_fail) = ShData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems, time_isa=time_isa, time_prover=time_prover, time_prover_fail=time_prover_fail} fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time, timeout,lemmas,posns) = ReData{calls=calls, success=success, nontriv_calls=nontriv_calls, nontriv_success=nontriv_success, proofs=proofs, time=time, timeout=timeout, lemmas=lemmas, posns=posns} val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0) val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), []) fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, posns) datatype data = Data of { sh: sh_data, re_u: re_data (* proof method with unminimized set of lemmas *) } type change_data = (data -> data) -> unit fun make_data (sh, re_u) = Data {sh=sh, re_u=re_u} val empty_data = make_data (empty_sh_data, empty_re_data) fun map_sh_data f (Data {sh, re_u}) = let val sh' = make_sh_data (f (tuple_of_sh_data sh)) in make_data (sh', re_u) end fun map_re_data f (Data {sh, re_u}) = let val f' = make_re_data o f o tuple_of_re_data val re_u' = f' re_u in make_data (sh, re_u') end fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_calls = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)) val inc_sh_nontriv_success = map_sh_data (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail) => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail)) fun inc_sh_lemmas n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail)) fun inc_sh_max_lems n = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail)) fun inc_sh_time_isa t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail)) fun inc_sh_time_prover t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail)) fun inc_sh_time_prover_fail t = map_sh_data (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail) => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t)) val inc_proof_method_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_calls = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns)) val inc_proof_method_nontriv_success = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns)) val inc_proof_method_proofs = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns)) fun inc_proof_method_time t = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) val inc_proof_method_timeout = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns)) fun inc_proof_method_lemmas n = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_proof_method_posns pos = map_re_data (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns) => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) val str0 = string_of_int o the_default 0 local val str = string_of_int val str3 = Real.fmt (StringCvt.FIX (SOME 3)) fun percentage a b = string_of_int (a * 100 div b) fun ms t = Real.fromInt t / 1000.0 fun avg_time t n = if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0 fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail}) = let val props = [("sh_calls", str calls), ("sh_success", str success), ("sh_nontriv_calls", str nontriv_calls), ("sh_nontriv_success", str nontriv_success), ("sh_lemmas", str lemmas), ("sh_max_lems", str max_lems), ("sh_time_isa", str3 (ms time_isa)), ("sh_time_prover", str3 (ms time_prover)), ("sh_time_prover_fail", str3 (ms time_prover_fail))] val text = "\nTotal number of sledgehammer calls: " ^ str calls ^ "\nNumber of successful sledgehammer calls: " ^ str success ^ "\nNumber of sledgehammer lemmas: " ^ str lemmas ^ "\nMax number of sledgehammer lemmas: " ^ str max_lems ^ "\nSuccess rate: " ^ percentage success calls ^ "%" ^ "\nTotal number of nontrivial sledgehammer calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^ "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^ "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^ "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^ "\nAverage time for sledgehammer calls (Isabelle): " ^ str3 (avg_time time_isa calls) ^ "\nAverage time for successful sledgehammer calls (ATP): " ^ str3 (avg_time time_prover success) ^ "\nAverage time for failed sledgehammer calls (ATP): " ^ str3 (avg_time time_prover_fail (calls - success)) in (props, text) end fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = let val proved = posns |> map (fn (pos, triv) => str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^ (if triv then "[T]" else "")) val props = [("re_calls", str calls), ("re_success", str success), ("re_nontriv_calls", str nontriv_calls), ("re_nontriv_success", str nontriv_success), ("re_proofs", str proofs), ("re_time", str3 (ms time)), ("re_timeout", str timeout), ("re_lemmas", str lemmas), ("re_lems_sos", str lems_sos), ("re_lems_max", str lems_max), ("re_proved", space_implode "," proved)] val text = "\nTotal number of proof method calls: " ^ str calls ^ "\nNumber of successful proof method calls: " ^ str success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of proof method timeouts: " ^ str timeout ^ "\nSuccess rate: " ^ percentage success sh_calls ^ "%" ^ "\nTotal number of nontrivial proof method calls: " ^ str nontriv_calls ^ "\nNumber of successful nontrivial proof method calls: " ^ str nontriv_success ^ " (proof: " ^ str proofs ^ ")" ^ "\nNumber of successful proof method lemmas: " ^ str lemmas ^ "\nSOS of successful proof method lemmas: " ^ str lems_sos ^ "\nMax number of successful proof method lemmas: " ^ str lems_max ^ "\nTotal time for successful proof method calls: " ^ str3 (ms time) ^ "\nAverage time for successful proof method calls: " ^ str3 (avg_time time success) ^ "\nProved: " ^ space_implode " " proved in (props, text) end in fun log_data index (Data {sh, re_u}) = let val ShData {calls=sh_calls, ...} = sh val ReData {calls=re_calls, ...} = re_u in if sh_calls > 0 then let val (props1, text1) = log_sh_data sh val (props2, text2) = log_re_data sh_calls re_u val text = "\n\nReport #" ^ string_of_int index ^ ":\n" ^ (if re_calls > 0 then text1 ^ "\n" ^ text2 else text1) in [Mirabelle.log_report (props1 @ props2) [XML.Text text]] end else [] end end fun get_prover_name thy args = let fun default_prover_name () = hd (#provers (Sledgehammer_Commands.default_params thy [])) handle List.Empty => error "No ATP available" in (case AList.lookup (op =) args proverK of SOME name => name | NONE => default_prover_name ()) end fun get_prover ctxt name params goal = let val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) in Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name end type stature = ATP_Problem_Generate.stature fun is_good_line s = (String.isSubstring " ms)" s orelse String.isSubstring " s)" s) andalso not (String.isSubstring "(> " s) andalso not (String.isSubstring ", > " s) andalso not (String.isSubstring "may fail" s) (* Fragile hack *) fun proof_method_from_msg args msg = (case AList.lookup (op =) args proof_methodK of SOME name => if name = "smart" then if exists is_good_line (split_lines msg) then "none" else "fail" else name | NONE => if exists is_good_line (split_lines msg) then "none" (* trust the preplayed proof *) else if String.isSubstring "metis (" msg then msg |> Substring.full |> Substring.position "metis (" |> snd |> Substring.position ")" |> fst |> Substring.string |> suffix ")" else if String.isSubstring "metis" msg then "metis" else "smt") local datatype sh_result = SH_OK of int * int * (string * stature) list | SH_FAIL of int * int | SH_ERROR fun run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st = let val thy = Proof.theory_of st val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 fun set_file_name (SOME dir) = Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix ("prob_" ^ str0 (Position.line_of pos) ^ "__") #> Config.put SMT_Config.debug_files (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_" ^ serial_string ()) | set_file_name NONE = I val st' = st |> Proof.map_context (set_file_name dir #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic) e_selection_heuristic |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order) term_order |> the_default I) #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos) force_sos |> the_default I)) val params as {max_facts, minimize, preplay_timeout, ...} = Sledgehammer_Commands.default_params thy ([(* ("verbose", "true"), *) ("fact_filter", fact_filter), ("type_enc", type_enc), ("strict", strict), ("lam_trans", lam_trans |> the_default lam_trans_default), ("uncurried_aliases", uncurried_aliases |> the_default uncurried_aliases_default), ("max_facts", max_facts), ("slice", slice), ("timeout", string_of_int timeout), ("preplay_timeout", preplay_timeout)] |> isar_proofsLST |> smt_proofsLST |> minimizeLST (*don't confuse the two minimization flags*) |> max_new_mono_instancesLST |> max_mono_itersLST) val default_max_facts = Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val time_limit = (case hard_timeout of NONE => I | SOME secs => Timeout.apply (Time.fromSeconds secs)) fun failed failure = ({outcome = SOME failure, used_facts = [], used_from = [], preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime, message = K ""}, ~1) val ({outcome, used_facts, preferred_methss, run_time, message, ...} : Sledgehammer_Prover.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name val keywords = Thy_Header.get_keywords' ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = Sledgehammer_Fact.nearly_all_facts ctxt ho_atp Sledgehammer_Fact.no_fact_override keywords css_table chained_ths hyp_ts concl_t val factss = facts |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name (the_default default_max_facts max_facts) Sledgehammer_Fact.no_fact_override hyp_ts concl_t |> tap (fn factss => "Line " ^ str0 (Position.line_of pos) ^ ": " ^ Sledgehammer.string_of_factss factss |> writeln) val prover = get_prover ctxt prover_name params goal val problem = {comment = "", state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I} in prover params problem end)) () handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time |> Time.toMilliseconds val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts st' i preferred_methss) in (case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) | SOME _ => (msg, SH_FAIL (time_isa, time_prover))) end handle ERROR msg => ("error: " ^ msg, SH_ERROR) in fun run_sledgehammer change_data trivial args proof_method named_thms pos st = let val thy = Proof.theory_of st val triv_str = if trivial then "[T] " else "" val _ = change_data inc_sh_calls val _ = if trivial then () else change_data inc_sh_nontriv_calls val prover_name = get_prover_name thy args val fact_filter = AList.lookup (op =) args fact_filterK |> the_default fact_filter_default val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default val strict = AList.lookup (op =) args strictK |> the_default strict_default val max_facts = (case AList.lookup (op =) args max_factsK of SOME max => max | NONE => (case AList.lookup (op =) args max_relevantK of SOME max => max | NONE => max_facts_default)) val slice = AList.lookup (op =) args sliceK |> the_default slice_default val lam_trans = AList.lookup (op =) args lam_transK val uncurried_aliases = AList.lookup (op =) args uncurried_aliasesK val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK val term_order = AList.lookup (op =) args term_orderK val force_sos = AList.lookup (op =) args force_sosK |> Option.map (curry (op <>) "false") val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_argument args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) val preplay_timeout = AList.lookup (op =) args preplay_timeoutK |> the_default preplay_timeout_default val isar_proofsLST = available_parameter args isar_proofsK "isar_proofs" val smt_proofsLST = available_parameter args smt_proofsK "smt_proofs" val minimizeLST = available_parameter args minimizeK "minimize" val max_new_mono_instancesLST = available_parameter args max_new_mono_instancesK max_new_mono_instancesK val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK val hard_timeout = SOME (4 * timeout) val (msg, result) = run_sh prover_name fact_filter type_enc strict max_facts slice lam_trans uncurried_aliases e_selection_heuristic term_order force_sos hard_timeout timeout preplay_timeout isar_proofsLST smt_proofsLST minimizeLST max_new_mono_instancesLST max_mono_itersLST dir pos st in (case result of SH_OK (time_isa, time_prover, names) => let fun get_thms (name, stature) = try (Sledgehammer_Util.thms_of_name (Proof.context_of st)) name |> Option.map (pair (name, stature)) in change_data inc_sh_success; if trivial then () else change_data inc_sh_nontriv_success; change_data (inc_sh_lemmas (length names)); change_data (inc_sh_max_lems (length names)); change_data (inc_sh_time_isa time_isa); change_data (inc_sh_time_prover time_prover); proof_method := proof_method_from_msg args msg; named_thms := SOME (map_filter get_thms names); triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg end | SH_FAIL (time_isa, time_prover) => let val _ = change_data (inc_sh_time_isa time_isa) val _ = change_data (inc_sh_time_prover_fail time_prover) in triv_str ^ "failed: " ^ msg end | SH_ERROR => "failed: " ^ msg) end end fun override_params prover type_enc timeout = [("provers", prover), ("max_facts", "0"), ("type_enc", type_enc), ("strict", "true"), ("slice", "false"), ("timeout", timeout |> Time.toSeconds |> string_of_int)] fun run_proof_method change_data trivial full name meth named_thms timeout pos st = let fun do_method named_thms ctxt = let val ref_of_str = (* FIXME proper wrapper for parser combinators *) suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none #> Parse.thm #> fst val thms = named_thms |> maps snd val facts = named_thms |> map (ref_of_str o fst o fst) val fact_override = {add = facts, del = [], only = true} fun my_timeout time_slice = timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal fun sledge_tac time_slice prover type_enc = Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in if !meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Proof.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms else if !meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" (!meth) then let val (type_encs, lam_trans) = !meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if !meth = "none" then K all_tac else if !meth = "fail" then K no_tac else (warning ("Unknown method " ^ quote (!meth)); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data inc_proof_method_success; if trivial then () else change_data inc_proof_method_nontriv_success; change_data (inc_proof_method_lemmas (length named_thms)); change_data (inc_proof_method_time t); change_data (inc_proof_method_posns (pos, trivial)); if name = "proof" then change_data inc_proof_method_proofs else (); "succeeded (" ^ string_of_int t ^ ")") fun timed_method named_thms = with_time (Mirabelle.cpu_time apply_method named_thms) handle Timeout.TIMEOUT _ => (change_data inc_proof_method_timeout; "timeout") | ERROR msg => ("error: " ^ msg) val _ = change_data inc_proof_method_calls val _ = if trivial then () else change_data inc_proof_method_nontriv_calls in timed_method named_thms end val try_timeout = seconds 5.0 fun catch e = e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Mirabelle.print_exn exn (* crude hack *) val num_sledgehammer_calls = Unsynchronized.ref 0 -val remaining_stride = Unsynchronized.ref stride_default val _ = Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer\ (fn context => fn commands => let val {index, tag = sh_tag, arguments = args, timeout, ...} = context fun proof_method_tag meth = "#" ^ string_of_int index ^ " " ^ meth ^ " (sledgehammer): " val data = Unsynchronized.ref empty_data val change_data = Unsynchronized.change data - val stride = Mirabelle.get_int_argument args (strideK, stride_default) val max_calls = Mirabelle.get_int_argument args (max_callsK, max_calls_default) val check_trivial = Mirabelle.get_bool_argument args (check_trivialK, check_trivial_default) val results = commands |> maps (fn command => let val {name, pos, pre = st, ...} = command val goal = Thm.major_prem_of (#goal (Proof.goal st)) val log = if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then [] - else if !remaining_stride > 1 then - (* We still have some steps to do *) - (Unsynchronized.dec remaining_stride; ["Skipping because of stride"]) else - (* This was the last step, now run the action *) let - val _ = remaining_stride := stride val _ = Unsynchronized.inc num_sledgehammer_calls in if !num_sledgehammer_calls > max_calls then ["Skipping because max number of calls reached"] else let val meth = Unsynchronized.ref "" val named_thms = Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val trivial = if check_trivial then Try0.try0 (SOME try_timeout) ([], [], [], []) st handle Timeout.TIMEOUT _ => false else false val log1 = sh_tag ^ catch (fn () => run_sledgehammer change_data trivial args meth named_thms pos st) val log2 = (case ! named_thms of SOME thms => [separator, proof_method_tag (!meth) ^ catch (fn () => run_proof_method change_data trivial false name meth thms timeout pos st)] | NONE => []) in log1 :: log2 end end in if null log then [] else [Mirabelle.log_command command [XML.Text (cat_lines log)]] end) val report = log_data index (! data) in results @ report end)) end diff --git a/src/HOL/Tools/etc/options b/src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options +++ b/src/HOL/Tools/etc/options @@ -1,60 +1,63 @@ (* :mode=isabelle-options: *) section "Automatically tried tools" public option auto_time_start : real = 1.0 -- "initial delay for automatically tried tools (seconds)" public option auto_time_limit : real = 2.0 -- "time limit for automatically tried tools (seconds > 0)" public option auto_nitpick : bool = false -- "run Nitpick automatically" public option auto_sledgehammer : bool = false -- "run Sledgehammer automatically" public option auto_methods : bool = false -- "try standard proof methods automatically" public option auto_quickcheck : bool = true -- "run Quickcheck automatically" public option auto_solve_direct : bool = true -- "run solve_direct automatically" section "Miscellaneous Tools" public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" -- "provers for Sledgehammer (separated by blanks)" public option sledgehammer_timeout : int = 30 -- "provers will be interrupted after this time (in seconds)" public option vampire_noncommercial : string = "unknown" -- "status of Vampire activation for noncommercial use (yes, no, unknown)" public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply" -- "URL for SystemOnTPTP service" public option MaSh : string = "sml" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" public option kodkod_scala : bool = true -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" 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_stride : int = 1 + -- "default stride for running Mirabelle actions on every nth goal" + 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)"