src/HOL/Tools/Mirabelle/mirabelle.scala

reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;

/*  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)
  })
}