diff --git a/src/HOL/Mirabelle.thy b/src/HOL/Mirabelle.thy --- a/src/HOL/Mirabelle.thy +++ b/src/HOL/Mirabelle.thy @@ -1,18 +1,27 @@ (* Title: HOL/Mirabelle.thy - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich *) theory Mirabelle imports Sledgehammer Predicate_Compile begin ML_file \Tools/Mirabelle/mirabelle.ML\ + +ML \ +signature MIRABELLE_ACTION = sig + val make_action : Mirabelle.action_context -> Mirabelle.action +end +\ + ML_file \Tools/Mirabelle/mirabelle_arith.ML\ ML_file \Tools/Mirabelle/mirabelle_metis.ML\ ML_file \Tools/Mirabelle/mirabelle_quickcheck.ML\ ML_file \Tools/Mirabelle/mirabelle_sledgehammer.ML\ ML_file \Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\ ML_file \Tools/Mirabelle/mirabelle_try0.ML\ -end +end \ No newline at end of file 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,268 +1,289 @@ (* Title: HOL/Mirabelle/Tools/mirabelle.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich *) 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 + type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time} + type command = + {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state} + type action = {run_action: command -> string, finalize: unit -> string} + val register_action: string -> (action_context -> action) -> unit (*utility functions*) + val print_exn: exn -> string 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; -); +type command = + {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}; +type action_context = {index: int, name: string, arguments: Properties.T, timeout: Time.time}; +type action = {run_action: command -> string, finalize: unit -> string}; -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 *) +local + val actions = Synchronized.var "Mirabelle.actions" + (Symtab.empty : (action_context -> action) Symtab.table); +in -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))]); +val register_action = Synchronized.change actions oo curry Symtab.update; -fun log_command ({name, pos, ...}: command) body = - XML.Elem (("command", (Markup.nameN, name) :: Position.properties_of pos), body); +fun get_action name = Symtab.lookup (Synchronized.value actions) name; -fun log_report props body = - XML.Elem (("report", props), body); +end (* 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); + | exn => "exception: " ^ General.exnMessage exn); -fun command_action binding action = +fun run_action_function f = + f () handle exn => + if Exn.is_interrupt exn then Exn.reraise exn + else print_exn exn; + +fun make_action_path (context as {index, name, ...} : action_context) = + Path.basic (string_of_int index ^ "." ^ name); + +fun finalize_action ({finalize, ...} : action) context = 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; + val s = run_action_function finalize; + val action_path = make_action_path context; + val export_name = + Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize"); + in + if s <> "" then + Export.export \<^theory> export_name [XML.Text s] + else + () + end + +fun apply_action ({run_action, ...} : action) context (command as {pos, pre, ...} : command) = + let + val thy = Proof.theory_of pre; + val action_path = make_action_path context; + val goal_name_path = Path.basic (#name command) + val line_path = Path.basic (string_of_int (the (Position.line_of pos))); + val offset_path = Path.basic (string_of_int (the (Position.offset_of pos))); + val export_name = + Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path + + line_path + offset_path); + val s = run_action_function (fn () => run_action command); + in + if s <> "" then + Export.export thy export_name [XML.Text s] + else + () + 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; -fun check_session qualifier thy_name (_: Position.T) = - Resources.theory_qualifier thy_name = qualifier; - (* presentation hook *) val whitelist = ["apply", "by", "proof"]; val _ = Build.add_hook (fn qualifier => fn loaded_theories => let val mirabelle_timeout = Options.default_seconds \<^system_option>\mirabelle_timeout\; val mirabelle_stride = Options.default_int \<^system_option>\mirabelle_stride\; + val mirabelle_max_calls = Options.default_int \<^system_option>\mirabelle_max_calls\; val mirabelle_actions = Options.default_string \<^system_option>\mirabelle_actions\; val mirabelle_theories = Options.default_string \<^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 = - if mirabelle_theories = "" then check_session qualifier - else check_theories (space_explode "," mirabelle_theories); + in + if null actions then + () + else + let + val check_theory = check_theories (space_explode "," mirabelle_theories); - fun theory_commands (thy, segments) = - let - val commands = segments - |> map_index (fn (n, {command = tr, prev_state = st, state = st', ...}) => - if n mod mirabelle_stride = 0 then + fun make_commands (thy_index, (thy, segments)) = + let + val thy_long_name = Context.theory_long_name thy; + val check_thy = check_theory thy_long_name; + fun make_command {command = tr, prev_state = st, state = st', ...} = let val name = Toplevel.name_of tr; val 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'} + member (op =) whitelist name andalso check_thy pos + then SOME {theory_index = thy_index, name = name, pos = pos, + pre = Toplevel.proof_of st, post = st'} else NONE - end - else NONE) - |> map_filter I; - in if null commands then NONE else SOME (thy, commands) end; + end; + in + if Resources.theory_qualifier thy_long_name = qualifier then + map_filter make_command segments + else + [] + end; - fun app_actions (thy, commands) = - (actions, ()) |-> fold_index (fn (index, (name, arguments)) => fn () => - apply_action (index + 1) name arguments mirabelle_timeout commands thy); - in - if null actions then () - else List.app app_actions (map_filter theory_commands loaded_theories) + (* initialize actions *) + val contexts = actions |> map_index (fn (n, (name, args)) => + let + val make_action = the (get_action name); + val context = {index = n, name = name, arguments = args, timeout = mirabelle_timeout}; + in + (make_action context, context) + end); + in + (* run actions on all relevant goals *) + loaded_theories + |> map_index I + |> maps make_commands + |> map_index I + |> maps (fn (n, command) => + let val (m, k) = Integer.div_mod (n + 1) mirabelle_stride in + if k = 0 andalso m <= mirabelle_max_calls then + map (fn context => (context, command)) contexts + else + [] + end) + |> Par_List.map (fn ((action, context), command) => apply_action action context command) + |> ignore; + + (* finalize actions *) + List.app (uncurry finalize_action) contexts + end 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,272 +1,240 @@ /* 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) + Isabelle_System.make_directory(output_dir) 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" + ("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))) + val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs) + val store = Sessions.store(build_options) + + def session_setup(session_name: String, session: Session): Unit = + { + val session_hierarchy = structure.hierarchy(session_name) + session.all_messages += + Session.Consumer[Prover.Message]("mirabelle_export") { + case msg: Prover.Protocol_Output => + msg.properties match { + case Protocol.Export(args) if args.name.startsWith("mirabelle/") => + if (verbose) { + progress.echo( + "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")") + } + using(store.open_database_context())(db_context => + { + for (export <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) { + val prefix = args.name.split('/') match { + case Array("mirabelle", action, "finalize") => + s"${action} finalize " + case Array("mirabelle", action, "goal", goal_name, line, offset) => + s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset} " + case _ => "" + } + val lines = Pretty.string_of(export.uncompressed_yxml).trim() + val body = Library.prefix_lines(prefix, lines) + "\n" + val log_file = output_dir + Path.basic("mirabelle.log") + File.append(log_file, body) + } + }) + case _ => + } + case _ => } - }) } - 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, + session_setup = session_setup) } 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 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_max_calls = options.int("mirabelle_max_calls") 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 + """) - -T THEORY theory restriction: NAME or NAME[LINE:END_LINE] + -T THEORY theory restriction: NAME or NAME[FIRST_LINE:LAST_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) + -m INT max. no. of calls to each Mirabelle action (default """ + default_max_calls + """) -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)), "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)), + "m:" -> (arg => options = options + ("mirabelle_max_calls=" + 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( 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_arith.ML b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML @@ -1,17 +1,24 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "arith". *) -structure Mirabelle_Arith: sig end = +structure Mirabelle_Arith: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\arith\ - (fn {timeout, ...} => fn {pre, ...} => - if Mirabelle.can_apply timeout Arith_Data.arith_tac pre - then "succeeded" else "")); +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + fun run_action ({pre, ...} : Mirabelle.command) = + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then + "succeeded" + else + "" + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "arith" make_action end diff --git a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML @@ -1,23 +1,28 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Martin Desharnais, UniBw Munich Mirabelle action: "metis". *) -structure Mirabelle_Metis: sig end = +structure Mirabelle_Metis: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\metis\ - (fn {timeout, ...} => fn {pre, post, ...} => +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + fun run_action ({pre, post, ...} : Mirabelle.command) = 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 + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "metis" make_action end diff --git a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML @@ -1,23 +1,26 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_quickcheck.ML - Author: Jasmin Blanchette and Sascha Boehme, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Martin Desharnais, UniBw Munich Mirabelle action: "quickcheck". *) -structure Mirabelle_Quickcheck: sig end = +structure Mirabelle_Quickcheck: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\quickcheck\ - (fn {arguments, timeout, ...} => fn {pre, ...} => - let - val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst; - val quickcheck = - Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1; - in - (case Timeout.apply timeout quickcheck pre of - NONE => "no counterexample" - | SOME _ => "counterexample found") - end)); +fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) = + 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 + + fun run_action ({pre, ...} : Mirabelle.command) = + (case Timeout.apply timeout quickcheck pre of + NONE => "no counterexample" + | SOME _ => "counterexample found") + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "quickcheck" make_action end 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,675 +1,623 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML - Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich + Author: Jasmin Blanchette, TU Munich + Author: Sascha Boehme, TU Munich + Author: Tobias Nipkow, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "sledgehammer". *) -structure Mirabelle_Sledgehammer: sig end = +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 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 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)) + => (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_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, + time_prover, time_prover_fail}) = + "\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)) -fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, - nontriv_success, proofs, time, timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) = +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 + "\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 + end in -fun log_data index (Data {sh, re_u}) = +fun log_data (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 [] + let val text1 = log_sh_data sh in + if re_calls > 0 then text1 ^ "\n" ^ log_re_data sh_calls re_u else text1 + 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) ^ "__") + ("prob_" ^ StringCvt.padLeft #"0" 5 (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 = +fun run_sledgehammer change_data thy_index trivial args proof_method named_thms pos st = let val thy = Proof.theory_of st + val thy_name = Context.theory_name thy 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 + |> Option.map (fn dir => + let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in + Path.append (Path.explode dir) (Path.basic subdir) + |> Isabelle_System.make_directory + |> Path.implode + end) 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 ^ ")") + | 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 _ = - 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 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) +fun make_action ({arguments, timeout, ...} : Mirabelle.action_context) = + let + val check_trivial = + Mirabelle.get_bool_argument arguments (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 - let - 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 data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data + val change_data = Synchronized.change data - val report = log_data index (! data) - in results @ report end)) + fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) = + 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 + let + val meth = Unsynchronized.ref "" + val named_thms = + Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) + val trivial = + check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre + handle Timeout.TIMEOUT _ => false + val log1 = + run_sledgehammer change_data theory_index trivial arguments meth named_thms pos pre + val log2 = + (case !named_thms of + SOME thms => + !meth ^ " (sledgehammer): " ^ run_proof_method change_data trivial false name meth + thms timeout pos pre + | NONE => "") + in log1 ^ "\n" ^ log2 end + end + + fun finalize () = log_data (Synchronized.value data) + in {run_action = run_action, finalize = finalize} end + +val () = Mirabelle.register_action "sledgehammer" make_action end diff --git a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML @@ -1,183 +1,186 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Author: Jasmin Blanchette, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "sledgehammer_filter". *) -structure Mirabelle_Sledgehammer_Filter: sig end = +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) -fun print_int x = Value.print_int (! x) +fun print_int x = Value.print_int (Synchronized.value x) fun percentage a b = if b = 0 then "N/A" else Value.print_int (a * 100 div b) fun percentage_alt a b = percentage a (a + b) val default_prover = ATP_Proof.eN (* arbitrary ATP *) fun with_index (i, s) = s ^ "@" ^ Value.print_int i val proof_fileK = "proof_file" -val _ = - Theory.setup (Mirabelle.theory_action \<^binding>\sledgehammer_filter\ - (fn context => fn commands => +fun make_action ({arguments, ...} : Mirabelle.action_context) = + let + val (proof_table, args) = let - val (proof_table, args) = - let - val (pf_args, other_args) = - #arguments context |> List.partition (curry (op =) proof_fileK o fst) - val proof_file = - (case pf_args of - [] => error "No \"proof_file\" specified" - | (_, s) :: _ => s) - fun do_line line = - (case line |> space_explode ":" of - [line_num, offset, proof] => - SOME (apply2 (the o Int.fromString) (line_num, offset), - proof |> space_explode " " |> filter_out (curry (op =) "")) - | _ => NONE) - val proof_table = - File.read (Path.explode proof_file) - |> space_explode "\n" - |> map_filter do_line - |> AList.coalesce (op =) - |> Prooftab.make - in (proof_table, other_args) end + val (pf_args, other_args) = + List.partition (curry (op =) proof_fileK o fst) arguments + val proof_file = + (case pf_args of + [] => error "No \"proof_file\" specified" + | (_, s) :: _ => s) + fun do_line line = + (case space_explode ":" line of + [line_num, offset, proof] => + SOME (apply2 (the o Int.fromString) (line_num, offset), + proof |> space_explode " " |> filter_out (curry (op =) "")) + | _ => NONE) + val proof_table = + File.read (Path.explode proof_file) + |> space_explode "\n" + |> map_filter do_line + |> AList.coalesce (op =) + |> Prooftab.make + in (proof_table, other_args) end - val num_successes = Unsynchronized.ref 0 - val num_failures = Unsynchronized.ref 0 - val num_found_proofs = Unsynchronized.ref 0 - val num_lost_proofs = Unsynchronized.ref 0 - val num_found_facts = Unsynchronized.ref 0 - val num_lost_facts = Unsynchronized.ref 0 + val num_successes = Synchronized.var "num_successes" 0 + val num_failures = Synchronized.var "num_failures" 0 + val num_found_proofs = Synchronized.var "num_found_proofs" 0 + val num_lost_proofs = Synchronized.var "num_lost_proofs" 0 + val num_found_facts = Synchronized.var "num_found_facts" 0 + val num_lost_facts = Synchronized.var "num_lost_facts" 0 + fun run_action ({pos, pre, ...} : Mirabelle.command) = + let val results = - commands |> maps (fn {pos, pre, ...} => - (case (Position.line_of pos, Position.offset_of pos) of - (SOME line_num, SOME offset) => - (case Prooftab.lookup proof_table (line_num, offset) of - SOME proofs => - let - val thy = Proof.theory_of pre - val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre - val prover = AList.lookup (op =) args "prover" |> the_default default_prover - val params as {max_facts, ...} = Sledgehammer_Commands.default_params thy args - val default_max_facts = - Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover - val relevance_fudge = - extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge - val subgoal = 1 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt - val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover - val keywords = Thy_Header.get_keywords' ctxt - val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = - Sledgehammer_Fact.nearly_all_facts ctxt ho_atp - Sledgehammer_Fact.no_fact_override keywords css_table chained_ths - hyp_ts concl_t - |> Sledgehammer_Fact.drop_duplicate_facts - |> Sledgehammer_MePo.mepo_suggested_facts ctxt params - (the_default default_max_facts max_facts) - (SOME relevance_fudge) hyp_ts concl_t - |> map (fst o fst) - val (found_facts, lost_facts) = - flat proofs |> sort_distinct string_ord - |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) - |> List.partition (curry (op <=) 0 o fst) - |>> sort (prod_ord int_ord string_ord) ||> map snd - val found_proofs = filter (forall (member (op =) facts)) proofs - val n = length found_proofs - val log1 = - if n = 0 then - (Unsynchronized.inc num_failures; "Failure") - else - (Unsynchronized.inc num_successes; - Unsynchronized.add num_found_proofs n; - "Success (" ^ Value.print_int n ^ " of " ^ - Value.print_int (length proofs) ^ " proofs)") - val _ = Unsynchronized.add num_lost_proofs (length proofs - n) - val _ = Unsynchronized.add num_found_facts (length found_facts) - val _ = Unsynchronized.add num_lost_facts (length lost_facts) - val log2 = - if null found_facts then [] - else - let - val found_weight = - Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) - / Real.fromInt (length found_facts) - |> Math.sqrt |> Real.ceil - in - ["Found facts (among " ^ Value.print_int (length facts) ^ - ", weight " ^ Value.print_int found_weight ^ "): " ^ - commas (map with_index found_facts)] - end - val log3 = - if null lost_facts then [] - else - ["Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ - commas lost_facts] - in [XML.Text (cat_lines (log1 :: log2 @ log3))] end - | NONE => [XML.Text "No known proof"]) - | _ => [])) + (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 _ = Int.div + val _ = Synchronized.change num_failures (curry op+ 1) + val log1 = + if n = 0 then + (Synchronized.change num_failures (curry op+ 1); "Failure") + else + (Synchronized.change num_successes (curry op+ 1); + Synchronized.change num_found_proofs (curry op+ n); + "Success (" ^ Value.print_int n ^ " of " ^ + Value.print_int (length proofs) ^ " proofs)") + val _ = Synchronized.change num_lost_proofs (curry op+ (length proofs - n)) + val _ = Synchronized.change num_found_facts (curry op+ (length found_facts)) + val _ = Synchronized.change num_lost_facts (curry op+ (length lost_facts)) + val log2 = + if null found_facts then + "" + else + let + val found_weight = + Real.fromInt (fold (fn (n, _) => Integer.add (n * n)) found_facts 0) + / Real.fromInt (length found_facts) + |> Math.sqrt |> Real.ceil + in + "Found facts (among " ^ Value.print_int (length facts) ^ + ", weight " ^ Value.print_int found_weight ^ "): " ^ + commas (map with_index found_facts) + end + val log3 = + if null lost_facts then + "" + else + "Lost facts (among " ^ Value.print_int (length facts) ^ "): " ^ + commas lost_facts + in cat_lines [log1, log2, log3] end + | NONE => "No known proof") + | _ => "") + in + results + end - val report = - if ! num_successes + ! num_failures > 0 then - let - val props = - [("num_successes", print_int num_successes), - ("num_failures", print_int num_failures), - ("num_found_proofs", print_int num_found_proofs), - ("num_lost_proofs", print_int num_lost_proofs), - ("num_found_facts", print_int num_found_facts), - ("num_lost_facts", print_int num_lost_facts)] - val text = - "\nNumber of overall successes: " ^ print_int num_successes ^ - "\nNumber of overall failures: " ^ print_int num_failures ^ - "\nOverall success rate: " ^ - percentage_alt (! num_successes) (! num_failures) ^ "%" ^ - "\nNumber of found proofs: " ^ print_int num_found_proofs ^ - "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ - "\nProof found rate: " ^ - percentage_alt (! num_found_proofs) (! num_lost_proofs) ^ "%" ^ - "\nNumber of found facts: " ^ print_int num_found_facts ^ - "\nNumber of lost facts: " ^ print_int num_lost_facts ^ - "\nFact found rate: " ^ - percentage_alt (! num_found_facts) (! num_lost_facts) ^ "%" - in [Mirabelle.log_report props [XML.Text text]] end - else [] - in results @ report end)) + fun finalize () = + if Synchronized.value num_successes + Synchronized.value num_failures > 0 then + "\nNumber of overall successes: " ^ print_int num_successes ^ + "\nNumber of overall failures: " ^ print_int num_failures ^ + "\nOverall success rate: " ^ + percentage_alt (Synchronized.value num_successes) + (Synchronized.value num_failures) ^ "%" ^ + "\nNumber of found proofs: " ^ print_int num_found_proofs ^ + "\nNumber of lost proofs: " ^ print_int num_lost_proofs ^ + "\nProof found rate: " ^ + percentage_alt (Synchronized.value num_found_proofs) + (Synchronized.value num_lost_proofs) ^ "%" ^ + "\nNumber of found facts: " ^ print_int num_found_facts ^ + "\nNumber of lost facts: " ^ print_int num_lost_facts ^ + "\nFact found rate: " ^ + percentage_alt (Synchronized.value num_found_facts) + (Synchronized.value num_lost_facts) ^ "%" + else + "" + in {run_action = run_action, finalize = finalize} end + +val () = Mirabelle.register_action "sledgehammer_filter" make_action end diff --git a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML +++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML @@ -1,17 +1,25 @@ (* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML Author: Jasmin Blanchette, TU Munich Author: Makarius + Author: Martin Desharnais, UniBw Munich Mirabelle action: "try0". *) -structure Mirabelle_Try0 : sig end = +structure Mirabelle_Try0: MIRABELLE_ACTION = struct -val _ = - Theory.setup (Mirabelle.command_action \<^binding>\try0\ - (fn {timeout, ...} => fn {pre, ...} => - if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre - then "succeeded" else "")); +fun make_action ({timeout, ...} : Mirabelle.action_context) = + let + val generous_timeout = Time.scale 10.0 timeout + + fun run_action ({pre, ...} : Mirabelle.command) = + if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then + "succeeded" + else + "" + in {run_action = run_action, finalize = K ""} end + +val () = Mirabelle.register_action "try0" make_action 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,63 +1,66 @@ (* :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_max_calls : int = 10000000 + -- "default max. no. of calls to each Mirabelle action" + 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)"