src/HOL/Tools/Mirabelle/mirabelle.scala
author haftmann
Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734 89347c0cc6a3
parent 81529 92a3017f7d1a
permissions -rw-r--r--
treat map_filter similar to list_all, list_ex, list_ex1
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
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75080
diff changeset
    12
object Mirabelle {
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    13
  /* actions and options */
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    14
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75080
diff changeset
    15
  def action_names(): List[String] = {
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    16
    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
    17
    (for {
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    18
      file <-
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    19
        File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file,
75906
2167b9e3157a clarified signature: support for adhoc file types;
wenzelm
parents: 75394
diff changeset
    20
          pred = file => File.is_ML(file.getName))
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    21
      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
    22
      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
    23
    } yield name).sorted
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    24
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    25
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75080
diff changeset
    26
  def sledgehammer_options(): List[String] = {
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    27
    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
    28
    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
    29
      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
    30
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    31
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    32
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    33
  /* main mirabelle */
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
  def mirabelle(
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    36
    options: Options,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    37
    actions: List[String],
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    38
    output_dir: Path,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    39
    theories: List[String] = Nil,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    40
    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
    41
    progress: Progress = new Progress,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    42
    dirs: List[Path] = Nil,
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    43
    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
    44
    numa_shuffling: Boolean = false,
79616
12bb31d01510 more robust type, with explicit default;
wenzelm
parents: 77628
diff changeset
    45
    max_jobs: Option[Int] = None,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75080
diff changeset
    46
  ): Build.Results = {
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    47
    require(!selection.requirements)
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    48
    Isabelle_System.make_directory(output_dir)
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    49
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    50
    progress.echo("Building required heaps ...")
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    51
    val build_results0 =
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    52
      Build.build(options, build_heap = true,
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    53
        selection = selection.copy(requirements = true), progress = progress, dirs = dirs,
77521
5642de4d225d clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77510
diff changeset
    54
        select_dirs = select_dirs, numa_shuffling = numa_shuffling, max_jobs = max_jobs)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    55
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    56
    if (build_results0.ok) {
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    57
      val build_options =
73821
9ead8d9be3ab clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents: 73807
diff changeset
    58
        options + "timeout_build=false" +
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    59
          ("mirabelle_actions=" + actions.mkString(";")) +
74116
5cd8b5cd0451 fixed malconfigured option output_dir in mirabelle
desharna
parents: 74078
diff changeset
    60
          ("mirabelle_theories=" + theories.mkString(",")) +
5cd8b5cd0451 fixed malconfigured option output_dir in mirabelle
desharna
parents: 74078
diff changeset
    61
          ("mirabelle_output_dir=" + output_dir.implode)
5cd8b5cd0451 fixed malconfigured option output_dir in mirabelle
desharna
parents: 74078
diff changeset
    62
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    63
75070
500a668f3ef5 added Isabelle identification to Mirabelle output
desharna
parents: 74989
diff changeset
    64
      progress.echo("Running Mirabelle on " + Isabelle_System.identification() + "...")
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    65
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75080
diff changeset
    66
      def session_setup(session_name: String, session: Session): Unit = {
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    67
        session.all_messages +=
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    68
          Session.Consumer[Prover.Message]("mirabelle_export") {
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    69
            case msg: Prover.Protocol_Output =>
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    70
              msg.properties match {
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    71
                case Protocol.Export(args) if args.name.startsWith("mirabelle/") =>
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
    72
                  progress.echo(
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
    73
                    "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
    74
                    verbose = true)
80480
972f7a4cdc0e clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;
wenzelm
parents: 80350
diff changeset
    75
                  val yxml = YXML.parse_body(msg.chunk, cache = build_results0.cache)
74746
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    76
                  val lines = Pretty.string_of(yxml).trim()
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    77
                  val prefix =
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    78
                    Export.explode_name(args.name) match {
74948
15ce207f69c8 added support for initialization messages to Mirabelle
desharna
parents: 74762
diff changeset
    79
                      case List("mirabelle", action, "initialize") => action + " initialize "
15ce207f69c8 added support for initialization messages to Mirabelle
desharna
parents: 74762
diff changeset
    80
                      case List("mirabelle", action, "finalize") => action + " finalize   "
74987
877f0c44d77e added cpu time (in ms) to Mirabelle run_action output
desharna
parents: 74986
diff changeset
    81
                      case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) =>
75080
1dae5cbcd358 Mirabelle now considers goals preceding "unfolding" and "using" commands
desharna
parents: 75070
diff changeset
    82
                        action + " goal." + String.format("%-9s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
74987
877f0c44d77e added cpu time (in ms) to Mirabelle run_action output
desharna
parents: 74986
diff changeset
    83
                          args.theory_name + " " + line + ":" + offset + "  "
74746
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    84
                      case _ => ""
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    85
                    }
74989
003f378b78a5 added Mirabelle option "-y" for dry run
desharna
parents: 74987
diff changeset
    86
                  val body = (if (lines == "") prefix else Library.prefix_lines(prefix, lines)) + "\n"
74746
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    87
                  val log_file = output_dir + Path.basic("mirabelle.log")
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);
wenzelm
parents: 74687
diff changeset
    88
                  File.append(log_file, body)
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    89
                case _ =>
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    90
              }
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    91
            case _ =>
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    92
          }
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    93
      }
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    94
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    95
      Build.build(build_options, clean_build = true,
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
    96
        selection = selection, progress = progress, dirs = dirs, select_dirs = select_dirs,
77521
5642de4d225d clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77510
diff changeset
    97
        numa_shuffling = numa_shuffling, max_jobs = max_jobs, session_setup = session_setup)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
    98
    }
73698
3d0952893db8 proper build of required session images vs. build with Mirabelle presentation;
wenzelm
parents: 73695
diff changeset
    99
    else build_results0
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   100
  }
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   101
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   102
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   103
  /* Isabelle tool wrapper */
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   104
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   105
  val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   106
    Scala_Project.here,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   107
    { args =>
77628
a538dab533ef clarified signature: prefer explicit types;
wenzelm
parents: 77521
diff changeset
   108
      var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   109
      val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   110
      val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   111
      val mirabelle_randomize = options.check_name("mirabelle_randomize")
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   112
      val mirabelle_stride = options.check_name("mirabelle_stride")
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   113
      val mirabelle_timeout = options.check_name("mirabelle_timeout")
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   114
      val mirabelle_output_dir = options.check_name("mirabelle_output_dir")
81528
e4b4141e6954 added parallel_group_size option to Mirabelle
desharna
parents: 77628
diff changeset
   115
      val mirabelle_parallel_group_size = options.check_name("mirabelle_parallel_group_size")
74078
a2cbe81e1e32 changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents: 74077
diff changeset
   116
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   117
      var actions: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   118
      var base_sessions: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   119
      var select_dirs: List[Path] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   120
      var numa_shuffling = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   121
      var output_dir = Path.explode(mirabelle_output_dir.default_value)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   122
      var theories: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   123
      var exclude_session_groups: List[String] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   124
      var all_sessions = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   125
      var dirs: List[Path] = Nil
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   126
      var session_groups: List[String] = Nil
79616
12bb31d01510 more robust type, with explicit default;
wenzelm
parents: 77628
diff changeset
   127
      var max_jobs: Option[Int] = None
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   128
      var verbose = false
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   129
      var exclude_sessions: List[String] = Nil
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   130
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   131
      val getopts = Getopts("""
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   132
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
   133
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   134
  Options are:
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   135
    -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
   136
    -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
   137
    -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
   138
    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
74078
a2cbe81e1e32 changed Mirabelle_Sledgehammer keep option from path to boolean
desharna
parents: 74077
diff changeset
   139
    -O DIR       """ + mirabelle_output_dir.description + " (default: " + mirabelle_output_dir.default_value + """)
73847
58f6b41efe88 refactored Mirabelle to produce output in real time
desharna
parents: 73821
diff changeset
   140
    -T THEORY    theory restriction: NAME or NAME[FIRST_LINE:LAST_LINE]
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   141
    -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
   142
    -a           select all sessions
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   143
    -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
   144
    -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
   145
    -j INT       maximum number of parallel jobs (default 1)
74077
b93d8c2ebab0 added automatic uniform stride option to Mirabelle
desharna
parents: 73849
diff changeset
   146
    -m INT       """ + mirabelle_max_calls.description + " (default " + mirabelle_max_calls.default_value + """)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   147
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
81528
e4b4141e6954 added parallel_group_size option to Mirabelle
desharna
parents: 77628
diff changeset
   148
    -p INT       """ + mirabelle_parallel_group_size.description + " (default " + mirabelle_parallel_group_size.default_value + """)
74986
fc664e4fbf6d added Mirabelle option -r to randomize the goals before selection
desharna
parents: 74959
diff changeset
   149
    -r INT       """ + mirabelle_randomize.description + " (default " + mirabelle_randomize.default_value + """)
74077
b93d8c2ebab0 added automatic uniform stride option to Mirabelle
desharna
parents: 73849
diff changeset
   150
    -s INT       """ + mirabelle_stride.description + " (default " + mirabelle_stride.default_value + """)
b93d8c2ebab0 added automatic uniform stride option to Mirabelle
desharna
parents: 73849
diff changeset
   151
    -t SECONDS   """ + mirabelle_timeout.description + " (default " + mirabelle_timeout.default_value + """)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   152
    -v           verbose
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   153
    -x NAME      exclude session NAME and all descendants
74989
003f378b78a5 added Mirabelle option "-y" for dry run
desharna
parents: 74987
diff changeset
   154
    -y           """ + mirabelle_dry_run.description + " (default " + mirabelle_dry_run.default_value + """)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   155
73849
4eac16052a94 tuned Mirabelle
desharna
parents: 73847
diff changeset
   156
  Apply the given ACTIONs at all theories and proof steps of the
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   157
  specified sessions.
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   158
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   159
  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
   160
  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
   161
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   162
  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
   163
  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
   164
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   165
  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
   166
74959
340c5f3506a8 tuned mirabelle command-line help message
desharna
parents: 74948
diff changeset
   167
  For the ACTION "sledgehammer", the usual sledgehammer as well as the following mirabelle-specific OPTIONs are available:""" +
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   168
        sledgehammer_options().mkString("\n    ", "\n    ", "\n"),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   169
        "A:" -> (arg => actions = actions ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   170
        "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   171
        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   172
        "N" -> (_ => numa_shuffling = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   173
        "O:" -> (arg => output_dir = Path.explode(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   174
        "T:" -> (arg => theories = theories ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   175
        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   176
        "a" -> (_ => all_sessions = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   177
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   178
        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
79616
12bb31d01510 more robust type, with explicit default;
wenzelm
parents: 77628
diff changeset
   179
        "j:" -> (arg => max_jobs = Some(Value.Nat.parse(arg))),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   180
        "m:" -> (arg => options = options + ("mirabelle_max_calls=" + arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   181
        "o:" -> (arg => options = options + arg),
81528
e4b4141e6954 added parallel_group_size option to Mirabelle
desharna
parents: 77628
diff changeset
   182
        "p:" -> (arg => options = options + ("mirabelle_parallel_group_size=" + arg)),
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   183
        "r:" -> (arg => options = options + ("mirabelle_randomize=" + arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   184
        "s:" -> (arg => options = options + ("mirabelle_stride=" + arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   185
        "t:" -> (arg => options = options + ("mirabelle_timeout=" + arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   186
        "v" -> (_ => verbose = true),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   187
        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   188
        "y" -> (arg => options = options + ("mirabelle_dry_run=true")))
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   189
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   190
      val sessions = getopts(args)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   191
      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
   192
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   193
      val progress = new Console_Progress(verbose = verbose)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   194
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   195
      val start_date = Date.now()
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   196
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
   197
      progress.echo("Started at " + Build_Log.print_date(start_date), verbose = true)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   198
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   199
      val results =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   200
        progress.interrupt_handler {
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   201
          mirabelle(options, actions, output_dir.absolute,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   202
            theories = theories,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   203
            selection = Sessions.Selection(
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   204
              all_sessions = all_sessions,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   205
              base_sessions = base_sessions,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   206
              exclude_session_groups = exclude_session_groups,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   207
              exclude_sessions = exclude_sessions,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   208
              session_groups = session_groups,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   209
              sessions = sessions),
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   210
            progress = progress,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   211
            dirs = dirs,
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   212
            select_dirs = select_dirs,
77477
f376aebca9c1 clarified modules;
wenzelm
parents: 77326
diff changeset
   213
            numa_shuffling = Host.numa_check(progress, numa_shuffling),
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
   214
            max_jobs = max_jobs)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   215
        }
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   216
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   217
      val end_date = Date.now()
79819
wenzelm
parents: 79616
diff changeset
   218
      val elapsed_time = end_date - start_date
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   219
77510
f5d6cd98b16a clarified signature: manage "verbose" flag via "progress";
wenzelm
parents: 77477
diff changeset
   220
      progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   221
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   222
      val total_timing =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   223
        results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   224
          copy(elapsed = elapsed_time)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   225
      progress.echo(total_timing.message_resources)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   226
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   227
      sys.exit(results.rc)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   228
    })
73691
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
wenzelm
parents:
diff changeset
   229
}