--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Fri May 14 21:32:11 2021 +0200
@@ -0,0 +1,264 @@
+/* Title: HOL/Tools/Mirabelle/mirabelle.scala
+ Author: Makarius
+
+Isabelle/Scala front-end for Mirabelle.
+*/
+
+package isabelle.mirabelle
+
+import isabelle._
+
+
+object Mirabelle
+{
+ /* actions and options */
+
+ def action_names(): List[String] =
+ {
+ val Pattern = """Mirabelle action: "(\w+)".*""".r
+ (for {
+ file <-
+ File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file,
+ pred = _.getName.endsWith(".ML"))
+ line <- split_lines(File.read(file))
+ name <- line match { case Pattern(a) => Some(a) case _ => None }
+ } yield name).sorted
+ }
+
+ def sledgehammer_options(): List[String] =
+ {
+ val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r
+ split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))).
+ flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None })
+ }
+
+
+ /* exported content */
+
+ val separator = "------------------\n"
+
+ def mirabelle_path(index: Int): String = "mirabelle/" + index
+
+ object Action
+ {
+ def get(export_name: String, xml: XML.Tree): Action =
+ xml match {
+ case XML.Elem(Markup("action", (Markup.NAME, name) :: arguments), body) =>
+ Action(name, arguments, body)
+ case _ =>
+ error("Expected action in export " + quote(export_name) + "\nmalformed XML: " + xml)
+ }
+ }
+ case class Action(name: String, arguments: Properties.T, body: XML.Body)
+ {
+ def print: String = XML.content(body)
+ }
+
+ object Command
+ {
+ def get(export_name: String, xml: XML.Tree): Command =
+ xml match {
+ case XML.Elem(Markup("command", (Markup.NAME, name) :: props), result) =>
+ Command(name, props.filter(Markup.position_property), result)
+ case _ =>
+ error("Expected command in export " + quote(export_name) + "\nmalformed XML: " + xml)
+ }
+ }
+ sealed case class Command(name: String, pos: Properties.T, result: XML.Body)
+ {
+ def print_head: String =
+ {
+ val line = Position.Line.get(pos)
+ val offset = Position.Offset.get(pos)
+ val loc = line.toString + ":" + offset.toString
+ "at " + loc + " (" + name + "):\n"
+ }
+ def print_body: String = Pretty.string_of(result)
+ def print: String = "\n\n" + print_head + separator + print_body
+ }
+
+
+ /* main mirabelle */
+
+ def mirabelle(
+ options: Options,
+ actions: List[String],
+ output_dir: Path,
+ theories: List[String] = Nil,
+ selection: Sessions.Selection = Sessions.Selection.empty,
+ progress: Progress = new Progress,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
+ numa_shuffling: Boolean = false,
+ max_jobs: Int = 1,
+ verbose: Boolean = false): Build.Results =
+ {
+ val build_options =
+ options + "parallel_presentation=false" +
+ ("mirabelle_actions=" + actions.mkString(";")) +
+ ("mirabelle_theories=" + theories.mkString(","))
+
+ val build_results =
+ Build.build(build_options, clean_build = true,
+ selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs,
+ numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose)
+
+ if (build_results.ok) {
+ val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs)
+ val store = Sessions.store(build_options)
+
+ using(store.open_database_context())(db_context =>
+ {
+ var seen_theories = Set.empty[String]
+ for {
+ session <- structure.imports_selection(selection).iterator
+ session_hierarchy = structure.hierarchy(session)
+ theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a)))
+ theory <- theories
+ if !seen_theories(theory)
+ index <- 1 to actions.length
+ export <- db_context.read_export(session_hierarchy, theory, mirabelle_path(index))
+ body = export.uncompressed_yxml
+ if body.nonEmpty
+ } {
+ seen_theories += theory
+ val export_name = Export.compound_name(theory, mirabelle_path(index))
+ val (action, commands) =
+ (Action.get(export_name, body.head), body.tail.map(Command.get(export_name, _)))
+ val dir = Isabelle_System.make_directory(output_dir + Path.basic(theory))
+ val log_file = dir + Path.basic("mirabelle" + index).log
+ progress.echo("Writing " + log_file)
+ File.write(log_file, terminate_lines(action.print :: commands.map(_.print)))
+ }
+ })
+ }
+
+ build_results
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val default_output_dir: Path = Path.explode("mirabelle")
+
+ val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
+ Scala_Project.here, args =>
+ {
+ val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+
+ var actions: List[String] = Nil
+ var base_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var numa_shuffling = false
+ var output_dir = default_output_dir
+ var requirements = false
+ var theories: List[String] = Nil
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var max_jobs = 1
+ var options = Options.init(opts = build_options)
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
+
+ val default_timeout = options.seconds("mirabelle_timeout")
+
+ val getopts = Getopts("""
+Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -A ACTION add to list of actions
+ -B NAME include session NAME and all descendants
+ -D DIR include session directory and select its sessions
+ -N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -O DIR output directory for log files (default: """ + default_output_dir + """,
+ -R refer to requirements of selected sessions
+ -T THEORY theory restriction: NAME or NAME[LINE:END_LINE]
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -j INT maximum number of parallel jobs (default 1)
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -t SECONDS timeout for each action (default """ + default_timeout + """)
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Apply the given actions at all theories and proof steps of the
+ specified sessions.
+
+ The absence of theory restrictions (option -T) means to check all
+ theories fully. Otherwise only the named theories are checked.
+
+ Each ACTION is either of the form NAME or NAME [OPTION, ...]
+ following Isabelle/Isar outer syntax.
+
+ Available actions are:""" + action_names().mkString("\n ", "\n ", "") + """
+
+ For the ACTION "sledgehammer", the following OPTIONs are available:""" +
+ sledgehammer_options().mkString("\n ", "\n ", "\n"),
+ "A:" -> (arg => actions = actions ::: List(arg)),
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "N" -> (_ => numa_shuffling = true),
+ "O:" -> (arg => output_dir = Path.explode(arg)),
+ "R" -> (_ => requirements = true),
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "o:" -> (arg => options = options + arg),
+ "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+ val sessions = getopts(args)
+
+ if (actions.isEmpty) error("Missing actions (option -A)")
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ val start_date = Date.now()
+
+ if (verbose) {
+ progress.echo("Started at " + Build_Log.print_date(start_date))
+ }
+
+ val results =
+ progress.interrupt_handler {
+ mirabelle(options, actions, output_dir,
+ theories = theories,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions,
+ exclude_session_groups = exclude_session_groups,
+ exclude_sessions = exclude_sessions,
+ session_groups = session_groups,
+ sessions = sessions),
+ progress = progress,
+ dirs = dirs,
+ select_dirs = select_dirs,
+ numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
+ max_jobs = max_jobs,
+ verbose = verbose)
+ }
+
+ val end_date = Date.now()
+ val elapsed_time = end_date.time - start_date.time
+
+ if (verbose) {
+ progress.echo("\nFinished at " + Build_Log.print_date(end_date))
+ }
+
+ val total_timing =
+ results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
+ copy(elapsed = elapsed_time)
+ progress.echo(total_timing.message_resources)
+
+ sys.exit(results.rc)
+ })
+}