src/HOL/Tools/Mirabelle/mirabelle.scala
author wenzelm
Sat, 15 May 2021 17:38:49 +0200
changeset 73695 b6d444194280
parent 73693 3ab18af9b2b5
child 73698 3d0952893db8
permissions -rw-r--r--
clarified command-line;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     1
/*  Title:      HOL/Tools/Mirabelle/mirabelle.scala
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     3
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     4
Isabelle/Scala front-end for Mirabelle.
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     5
*/
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     6
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     7
package isabelle.mirabelle
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     8
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
     9
import isabelle._
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    10
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    11
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    12
object Mirabelle
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    13
{
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    14
  /* actions and options */
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    15
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    16
  def action_names(): List[String] =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    17
  {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    18
    val Pattern = """Mirabelle action: "(\w+)".*""".r
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    19
    (for {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    20
      file <-
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    21
        File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    22
          pred = _.getName.endsWith(".ML"))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    23
      line <- split_lines(File.read(file))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    24
      name <- line match { case Pattern(a) => Some(a) case _ => None }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    25
    } yield name).sorted
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    26
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    27
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    28
  def sledgehammer_options(): List[String] =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    29
  {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    30
    val Pattern = """val .*K *= *"(.*)" *\(\*(.*)\*\)""".r
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    31
    split_lines(File.read(Path.explode("~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"))).
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    32
      flatMap(line => line match { case Pattern(a, b) => Some (a + b) case _ => None })
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    33
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    34
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    35
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    36
  /* exported log content */
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    37
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    38
  object Log
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    39
  {
73693
3ab18af9b2b5 clarified signature;
wenzelm
parents: 73692
diff changeset
    40
    def export_name(index: Int, theory: String = ""): String =
3ab18af9b2b5 clarified signature;
wenzelm
parents: 73692
diff changeset
    41
      Export.compound_name(theory, "mirabelle/" + index)
3ab18af9b2b5 clarified signature;
wenzelm
parents: 73692
diff changeset
    42
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    43
    val separator = "\n------------------\n"
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    44
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    45
    sealed abstract class Entry { def print: String }
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    46
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    47
    case class Action(name: String, arguments: Properties.T, body: XML.Body) extends Entry
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    48
    {
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    49
      def print: String = "action: " + XML.content(body) + separator
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    50
    }
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    51
    case class Command(name: String, position: Properties.T, body: XML.Body) extends Entry
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    52
    {
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    53
      def print: String = "\n" + print_head + separator + Pretty.string_of(body)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    54
      def print_head: String =
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    55
      {
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    56
        val line = Position.Line.get(position)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    57
        val offset = Position.Offset.get(position)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    58
        val loc = line.toString + ":" + offset.toString
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    59
        "at " + loc + " (" + name + "):"
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    60
      }
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    61
    }
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    62
    case class Report(result: Properties.T, body: XML.Body) extends Entry
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    63
    {
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    64
      override def print: String = "\n" + separator + Pretty.string_of(body)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    65
    }
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    66
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    67
    def entry(export_name: String, xml: XML.Tree): Entry =
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    68
      xml match {
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    69
        case XML.Elem(Markup("action", (Markup.NAME, name) :: props), body) =>
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    70
          Action(name, props, body)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    71
        case XML.Elem(Markup("command", (Markup.NAME, name) :: props), body) =>
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    72
          Command(name, props.filter(Markup.position_property), body)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    73
        case XML.Elem(Markup("report", props), body) => Report(props, body)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    74
        case _ => error("Malformed export " + quote(export_name) + "\nbad XML: " + xml)
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
    75
      }
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    76
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    77
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    78
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    79
  /* main mirabelle */
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    80
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    81
  def mirabelle(
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    82
    options: Options,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    83
    actions: List[String],
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    84
    output_dir: Path,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    85
    theories: List[String] = Nil,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    86
    selection: Sessions.Selection = Sessions.Selection.empty,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    87
    progress: Progress = new Progress,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    88
    dirs: List[Path] = Nil,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    89
    select_dirs: List[Path] = Nil,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    90
    numa_shuffling: Boolean = false,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    91
    max_jobs: Int = 1,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    92
    verbose: Boolean = false): Build.Results =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    93
  {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    94
    val build_options =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    95
      options + "parallel_presentation=false" +
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    96
        ("mirabelle_actions=" + actions.mkString(";")) +
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    97
        ("mirabelle_theories=" + theories.mkString(","))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    98
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    99
    val build_results =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   100
      Build.build(build_options, clean_build = true,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   101
        selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   102
        numa_shuffling = numa_shuffling, max_jobs = max_jobs, verbose = verbose)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   103
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   104
    if (build_results.ok) {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   105
      val structure = Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   106
      val store = Sessions.store(build_options)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   107
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   108
      using(store.open_database_context())(db_context =>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   109
      {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   110
        var seen_theories = Set.empty[String]
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   111
        for {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   112
          session <- structure.imports_selection(selection).iterator
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   113
          session_hierarchy = structure.hierarchy(session)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   114
          theories <- db_context.input_database(session)((db, a) => Some(store.read_theories(db, a)))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   115
          theory <- theories
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   116
          if !seen_theories(theory)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   117
          index <- 1 to actions.length
73693
3ab18af9b2b5 clarified signature;
wenzelm
parents: 73692
diff changeset
   118
          export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index))
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   119
          body = export.uncompressed_yxml
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   120
          if body.nonEmpty
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   121
        } {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   122
          seen_theories += theory
73693
3ab18af9b2b5 clarified signature;
wenzelm
parents: 73692
diff changeset
   123
          val export_name = Log.export_name(index, theory = theory)
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
   124
          val log = body.map(Log.entry(export_name, _))
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
   125
          val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory))
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
   126
          val log_file = log_dir + Path.basic("mirabelle" + index).log
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   127
          progress.echo("Writing " + log_file)
73692
8444d4ff5646 clarified log content;
wenzelm
parents: 73691
diff changeset
   128
          File.write(log_file, terminate_lines(log.map(_.print)))
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   129
        }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   130
      })
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   131
    }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   132
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   133
    build_results
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   134
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   135
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   136
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   137
  /* Isabelle tool wrapper */
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   138
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   139
  val default_output_dir: Path = Path.explode("mirabelle")
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   140
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   141
  val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   142
    Scala_Project.here, args =>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   143
  {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   144
    val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   145
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   146
    var actions: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   147
    var base_sessions: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   148
    var select_dirs: List[Path] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   149
    var numa_shuffling = false
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   150
    var output_dir = default_output_dir
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   151
    var requirements = false
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   152
    var theories: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   153
    var exclude_session_groups: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   154
    var all_sessions = false
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   155
    var dirs: List[Path] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   156
    var session_groups: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   157
    var max_jobs = 1
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   158
    var options = Options.init(opts = build_options)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   159
    var verbose = false
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   160
    var exclude_sessions: List[String] = Nil
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   161
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   162
    val default_timeout = options.seconds("mirabelle_timeout")
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   163
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   164
    val getopts = Getopts("""
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   165
Usage: isabelle mirabelle [OPTIONS] [SESSIONS ...]
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   166
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   167
  Options are:
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   168
    -A ACTION    add to list of actions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   169
    -B NAME      include session NAME and all descendants
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   170
    -D DIR       include session directory and select its sessions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   171
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   172
    -O DIR       output directory for log files (default: """ + default_output_dir + """,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   173
    -R           refer to requirements of selected sessions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   174
    -T THEORY    theory restriction: NAME or NAME[LINE:END_LINE]
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   175
    -X NAME      exclude sessions from group NAME and all descendants
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   176
    -a           select all sessions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   177
    -d DIR       include session directory
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   178
    -g NAME      select session group NAME
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   179
    -j INT       maximum number of parallel jobs (default 1)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   180
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   181
    -t SECONDS   timeout for each action (default """ + default_timeout + """)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   182
    -v           verbose
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   183
    -x NAME      exclude session NAME and all descendants
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   184
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   185
  Apply the given actions at all theories and proof steps of the
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   186
  specified sessions.
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   187
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   188
  The absence of theory restrictions (option -T) means to check all
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   189
  theories fully. Otherwise only the named theories are checked.
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   190
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   191
  Each ACTION is either of the form NAME or NAME [OPTION, ...]
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   192
  following Isabelle/Isar outer syntax.
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   193
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   194
  Available actions are:""" + action_names().mkString("\n    ", "\n    ", "") + """
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   195
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   196
  For the ACTION "sledgehammer", the following OPTIONs are available:""" +
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   197
      sledgehammer_options().mkString("\n    ", "\n    ", "\n"),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   198
      "A:" -> (arg => actions = actions ::: List(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   199
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   200
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   201
      "N" -> (_ => numa_shuffling = true),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   202
      "O:" -> (arg => output_dir = Path.explode(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   203
      "R" -> (_ => requirements = true),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   204
      "T:" -> (arg => theories = theories ::: List(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   205
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   206
      "a" -> (_ => all_sessions = true),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   207
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   208
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   209
      "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   210
      "o:" -> (arg => options = options + arg),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   211
      "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   212
      "v" -> (_ => verbose = true),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   213
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   214
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   215
    val sessions = getopts(args)
73695
b6d444194280 clarified command-line;
wenzelm
parents: 73693
diff changeset
   216
    if (actions.isEmpty) getopts.usage()
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   217
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   218
    val progress = new Console_Progress(verbose = verbose)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   219
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   220
    val start_date = Date.now()
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   221
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   222
    if (verbose) {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   223
      progress.echo("Started at " + Build_Log.print_date(start_date))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   224
    }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   225
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   226
    val results =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   227
      progress.interrupt_handler {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   228
        mirabelle(options, actions, output_dir,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   229
          theories = theories,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   230
          selection = Sessions.Selection(
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   231
            requirements = requirements,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   232
            all_sessions = all_sessions,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   233
            base_sessions = base_sessions,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   234
            exclude_session_groups = exclude_session_groups,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   235
            exclude_sessions = exclude_sessions,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   236
            session_groups = session_groups,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   237
            sessions = sessions),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   238
          progress = progress,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   239
          dirs = dirs,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   240
          select_dirs = select_dirs,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   241
          numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   242
          max_jobs = max_jobs,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   243
          verbose = verbose)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   244
      }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   245
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   246
    val end_date = Date.now()
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   247
    val elapsed_time = end_date.time - start_date.time
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   248
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   249
    if (verbose) {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   250
      progress.echo("\nFinished at " + Build_Log.print_date(end_date))
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   251
    }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   252
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   253
    val total_timing =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   254
      results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   255
        copy(elapsed = elapsed_time)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   256
    progress.echo(total_timing.message_resources)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   257
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   258
    sys.exit(results.rc)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   259
  })
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   260
}