src/Pure/Tools/build.scala
author wenzelm
Sun May 14 20:16:13 2017 +0200 (2017-05-14)
changeset 65832 2fb85623c386
parent 65831 3b197547c1d4
child 65935 73c099fa96a4
permissions -rw-r--r--
implicitly check for unknown files (not part of a Mercurial repository);
     1 /*  Title:      Pure/Tools/build.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:
     4 
     5 Build and manage Isabelle sessions.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.io.{BufferedInputStream, FileInputStream,
    12   BufferedReader, InputStreamReader, IOException}
    13 import java.util.zip.GZIPInputStream
    14 
    15 import scala.collection.SortedSet
    16 import scala.collection.mutable
    17 import scala.annotation.tailrec
    18 
    19 
    20 object Build
    21 {
    22   /** auxiliary **/
    23 
    24   /* persistent build info */
    25 
    26   sealed case class Session_Info(
    27     sources: List[String],
    28     input_heaps: List[String],
    29     output_heap: Option[String],
    30     return_code: Int)
    31 
    32 
    33   /* queue with scheduling information */
    34 
    35   private object Queue
    36   {
    37     def load_timings(progress: Progress, store: Sessions.Store, name: String)
    38       : (List[Properties.T], Double) =
    39     {
    40       val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    41 
    42       store.find_database(name) match {
    43         case None => no_timings
    44         case Some(database) =>
    45           def ignore_error(msg: String) =
    46           {
    47             progress.echo_warning("Ignoring bad database: " +
    48               database.expand + (if (msg == "") "" else "\n" + msg))
    49             no_timings
    50           }
    51           try {
    52             using(SQLite.open_database(database))(db =>
    53             {
    54               val build_log = store.read_build_log(db, name, command_timings = true)
    55               val session_timing = Markup.Elapsed.unapply(build_log.session_timing) getOrElse 0.0
    56               (build_log.command_timings, session_timing)
    57             })
    58           }
    59           catch {
    60             case ERROR(msg) => ignore_error(msg)
    61             case exn: java.lang.Error => ignore_error(Exn.message(exn))
    62             case _: XML.Error => ignore_error("")
    63           }
    64       }
    65     }
    66 
    67     def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
    68     {
    69       val graph = sessions.build_graph
    70       val names = graph.keys
    71 
    72       val timings = names.map(name => (name, load_timings(progress, store, name)))
    73       val command_timings =
    74         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
    75       val session_timing =
    76         Map(timings.map({ case (name, (_, t)) => (name, t) }): _*).withDefaultValue(0.0)
    77 
    78       def outdegree(name: String): Int = graph.imm_succs(name).size
    79 
    80       object Ordering extends scala.math.Ordering[String]
    81       {
    82         def compare_timing(name1: String, name2: String): Int =
    83         {
    84           val t1 = session_timing(name1)
    85           val t2 = session_timing(name2)
    86           if (t1 == 0.0 || t2 == 0.0) 0
    87           else t1 compare t2
    88         }
    89 
    90         def compare(name1: String, name2: String): Int =
    91           outdegree(name2) compare outdegree(name1) match {
    92             case 0 =>
    93               compare_timing(name2, name1) match {
    94                 case 0 =>
    95                   sessions(name2).timeout compare sessions(name1).timeout match {
    96                     case 0 => name1 compare name2
    97                     case ord => ord
    98                   }
    99                 case ord => ord
   100               }
   101             case ord => ord
   102           }
   103       }
   104 
   105       new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
   106     }
   107   }
   108 
   109   private class Queue(
   110     graph: Graph[String, Sessions.Info],
   111     order: SortedSet[String],
   112     val command_timings: String => List[Properties.T])
   113   {
   114     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   115 
   116     def is_empty: Boolean = graph.is_empty
   117 
   118     def - (name: String): Queue =
   119       new Queue(graph.del_node(name),
   120         order - name,  // FIXME scala-2.10.0 TreeSet problem!?
   121         command_timings)
   122 
   123     def dequeue(skip: String => Boolean): Option[(String, Sessions.Info)] =
   124     {
   125       val it = order.iterator.dropWhile(name =>
   126         skip(name)
   127           || !graph.defined(name)  // FIXME scala-2.10.0 TreeSet problem!?
   128           || !graph.is_minimal(name))
   129       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   130       else None
   131     }
   132   }
   133 
   134 
   135   /* PIDE protocol handler */
   136 
   137   class Handler(progress: Progress, session: Session, session_name: String)
   138     extends Session.Protocol_Handler
   139   {
   140     val result_error: Promise[String] = Future.promise
   141 
   142     override def exit() { result_error.cancel }
   143 
   144     private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
   145     {
   146       val error_message =
   147         try { Pretty.string_of(Symbol.decode_yxml(msg.text)) }
   148         catch { case ERROR(msg) => msg }
   149       result_error.fulfill(error_message)
   150       session.send_stop()
   151       true
   152     }
   153 
   154     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
   155       msg.properties match {
   156         case Markup.Loading_Theory(name) =>
   157           progress.theory(session_name, name)
   158           true
   159         case _ => false
   160       }
   161 
   162     val functions =
   163       List(
   164         Markup.BUILD_SESSION_FINISHED -> build_session_finished _,
   165         Markup.LOADING_THEORY -> loading_theory _)
   166   }
   167 
   168 
   169   /* job: running prover process */
   170 
   171   private class Job(progress: Progress,
   172     name: String,
   173     val info: Sessions.Info,
   174     sessions: Sessions.T,
   175     deps: Sessions.Deps,
   176     store: Sessions.Store,
   177     do_output: Boolean,
   178     verbose: Boolean,
   179     pide: Boolean,
   180     val numa_node: Option[Int],
   181     command_timings: List[Properties.T])
   182   {
   183     val output = store.output_dir + Path.basic(name)
   184     def output_path: Option[Path] = if (do_output) Some(output) else None
   185     output.file.delete
   186 
   187     val options =
   188       numa_node match {
   189         case None => info.options
   190         case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
   191       }
   192 
   193     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
   194     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph)
   195 
   196     private val future_result: Future[Process_Result] =
   197       Future.thread("build") {
   198         val parent = info.parent.getOrElse("")
   199         val base = deps(name)
   200         val args_yxml =
   201           YXML.string_of_body(
   202             {
   203               import XML.Encode._
   204               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
   205                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
   206                 pair(string, pair(string, pair(string, pair(Path.encode,
   207                 pair(list(pair(Options.encode, list(pair(string, properties)))),
   208                 pair(list(pair(string, string)), pair(list(pair(string, string)),
   209                 list(pair(string, string))))))))))))))))(
   210               (Symbol.codes, (command_timings, (do_output, (verbose,
   211                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
   212                 (parent, (info.chapter, (name, (Path.current,
   213                 (info.theories,
   214                 (base.global_theories.toList, (base.loaded_theories.toList,
   215                 base.dest_known_theories)))))))))))))))
   216             })
   217 
   218         val env =
   219           Isabelle_System.settings() +
   220             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
   221 
   222         def save_heap: String =
   223           "ML_Heap.share_common_data (); ML_Heap.save_child " +
   224             ML_Syntax.print_string0(File.platform_path(output))
   225 
   226         if (pide && !Sessions.is_pure(name)) {
   227           val resources = new Resources(deps(parent))
   228           val session = new Session(options, resources)
   229           val handler = new Handler(progress, session, name)
   230           session.init_protocol_handler(handler)
   231 
   232           val session_result = Future.promise[Process_Result]
   233 
   234           Isabelle_Process.start(session, options, logic = parent,
   235             cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
   236             phase_changed =
   237             {
   238               case Session.Ready => session.protocol_command("build_session", args_yxml)
   239               case Session.Terminated(result) => session_result.fulfill(result)
   240               case _ =>
   241             })
   242 
   243           val result = session_result.join
   244           handler.result_error.join match {
   245             case "" => result
   246             case msg =>
   247               result.copy(
   248                 rc = result.rc max 1,
   249                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   250           }
   251         }
   252         else {
   253           val args_file = Isabelle_System.tmp_file("build")
   254           File.write(args_file, args_yxml)
   255 
   256           val eval =
   257             "Command_Line.tool0 (fn () => (" +
   258             "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
   259             (if (do_output) "; " + save_heap else "") + "));"
   260 
   261           val process =
   262             if (Sessions.is_pure(name)) {
   263               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   264                 args =
   265                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   266                   List("--eval", eval),
   267                 env = env, sessions = Some(sessions), store = store,
   268                 cleanup = () => args_file.delete)
   269             }
   270             else {
   271               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   272                 env = env, sessions = Some(sessions), store = store,
   273                 cleanup = () => args_file.delete)
   274             }
   275 
   276           process.result(
   277             progress_stdout = (line: String) =>
   278               Library.try_unprefix("\floading_theory = ", line) match {
   279                 case Some(theory) => progress.theory(name, theory)
   280                 case None =>
   281               },
   282             progress_limit =
   283               options.int("process_output_limit") match {
   284                 case 0 => None
   285                 case m => Some(m * 1000000L)
   286               },
   287             strict = false)
   288         }
   289       }
   290 
   291     def terminate: Unit = future_result.cancel
   292     def is_finished: Boolean = future_result.is_finished
   293 
   294     @volatile private var was_timeout = false
   295     private val timeout_request: Option[Event_Timer.Request] =
   296     {
   297       if (info.timeout > Time.zero)
   298         Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
   299       else None
   300     }
   301 
   302     def join: Process_Result =
   303     {
   304       val result = future_result.join
   305 
   306       if (result.ok)
   307         Present.finish(progress, store.browser_info, graph_file, info, name)
   308 
   309       graph_file.delete
   310       timeout_request.foreach(_.cancel)
   311 
   312       if (result.interrupted) {
   313         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   314         else result.error(Output.error_message_text("Interrupt"))
   315       }
   316       else result
   317     }
   318   }
   319 
   320 
   321 
   322   /** build with results **/
   323 
   324   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   325   {
   326     def sessions: Set[String] = results.keySet
   327     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   328     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   329     def info(name: String): Sessions.Info = results(name)._2
   330     val rc =
   331       (0 /: results.iterator.map(
   332         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   333     def ok: Boolean = rc == 0
   334 
   335     override def toString: String = rc.toString
   336   }
   337 
   338   def build(
   339     options: Options,
   340     progress: Progress = No_Progress,
   341     check_unknown_files: Boolean = false,
   342     build_heap: Boolean = false,
   343     clean_build: Boolean = false,
   344     dirs: List[Path] = Nil,
   345     select_dirs: List[Path] = Nil,
   346     numa_shuffling: Boolean = false,
   347     max_jobs: Int = 1,
   348     list_files: Boolean = false,
   349     check_keywords: Set[String] = Set.empty,
   350     no_build: Boolean = false,
   351     system_mode: Boolean = false,
   352     verbose: Boolean = false,
   353     pide: Boolean = false,
   354     requirements: Boolean = false,
   355     all_sessions: Boolean = false,
   356     exclude_session_groups: List[String] = Nil,
   357     exclude_sessions: List[String] = Nil,
   358     session_groups: List[String] = Nil,
   359     sessions: List[String] = Nil,
   360     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   361   {
   362     /* session selection and dependencies */
   363 
   364     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   365 
   366     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
   367 
   368     val (selected, selected_sessions) =
   369       full_sessions.selection(
   370           Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   371             exclude_sessions, session_groups, sessions) + selection)
   372 
   373     val deps =
   374       Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
   375         verbose = verbose, list_files = list_files, check_keywords = check_keywords,
   376         global_theories = full_sessions.global_theories)
   377 
   378     def sources_stamp(name: String): List[String] =
   379       (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   380 
   381     if (check_unknown_files) {
   382       val source_files =
   383         (for {
   384           (_, base) <- deps.session_bases.iterator
   385           (path, _) <- base.sources.iterator
   386         } yield path).toList
   387       val unknown_files = Mercurial.unknown_files(source_files)
   388       if (unknown_files.nonEmpty) {
   389         progress.echo_warning("Unknown files (not part of a Mercurial repository):" +
   390           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
   391       }
   392     }
   393 
   394 
   395     /* main build process */
   396 
   397     val store = Sessions.store(system_mode)
   398     val queue = Queue(progress, selected_sessions, store)
   399 
   400     store.prepare_output()
   401 
   402     // optional cleanup
   403     if (clean_build) {
   404       for (name <- full_sessions.build_descendants(selected)) {
   405         val files =
   406           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   407             map(store.output_dir + _).filter(_.is_file)
   408         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   409         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   410       }
   411     }
   412 
   413     // scheduler loop
   414     case class Result(
   415       current: Boolean, heap_stamp: Option[String],
   416       process: Option[Process_Result], info: Sessions.Info)
   417     {
   418       def ok: Boolean =
   419         process match {
   420           case None => false
   421           case Some(res) => res.rc == 0
   422         }
   423     }
   424 
   425     def sleep()
   426     {
   427       try { Thread.sleep(500) }
   428       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   429     }
   430 
   431     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   432 
   433     @tailrec def loop(
   434       pending: Queue,
   435       running: Map[String, (List[String], Job)],
   436       results: Map[String, Result]): Map[String, Result] =
   437     {
   438       def used_node(i: Int): Boolean =
   439         running.iterator.exists(
   440           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   441 
   442       if (pending.is_empty) results
   443       else {
   444         if (progress.stopped)
   445           for ((_, (_, job)) <- running) job.terminate
   446 
   447         running.find({ case (_, (_, job)) => job.is_finished }) match {
   448           case Some((name, (input_heaps, job))) =>
   449             //{{{ finish job
   450 
   451             val process_result = job.join
   452             process_result.err_lines.foreach(progress.echo(_))
   453             if (process_result.ok)
   454               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   455 
   456             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   457             val process_result_tail =
   458             {
   459               val tail = job.info.options.int("process_output_tail")
   460               process_result.copy(
   461                 out_lines =
   462                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   463                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   464             }
   465 
   466             val heap_stamp =
   467               if (process_result.ok) {
   468                 (store.output_dir + store.log(name)).file.delete
   469                 val heap_stamp =
   470                   for (path <- job.output_path if path.is_file)
   471                     yield Sessions.write_heap_digest(path)
   472 
   473                 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   474 
   475                 heap_stamp
   476               }
   477               else {
   478                 (store.output_dir + Path.basic(name)).file.delete
   479                 (store.output_dir + store.log_gz(name)).file.delete
   480 
   481                 File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   482                 progress.echo(name + " FAILED")
   483                 if (!process_result.interrupted) progress.echo(process_result_tail.out)
   484 
   485                 None
   486               }
   487 
   488             // write database
   489             {
   490               val database = store.output_dir + store.database(name)
   491               database.file.delete
   492 
   493               using(SQLite.open_database(database))(db =>
   494                 store.write_session_info(db, name,
   495                   build_log =
   496                     Build_Log.Log_File(name, process_result.out_lines).
   497                       parse_session_info(
   498                         command_timings = true, ml_statistics = true, task_statistics = true),
   499                   build =
   500                     Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   501             }
   502 
   503             loop(pending - name, running - name,
   504               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   505             //}}}
   506           case None if running.size < (max_jobs max 1) =>
   507             //{{{ check/start next job
   508             pending.dequeue(running.isDefinedAt(_)) match {
   509               case Some((name, info)) =>
   510                 val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
   511                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   512 
   513                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   514 
   515                 val (current, heap_stamp) =
   516                 {
   517                   store.find_database_heap(name) match {
   518                     case Some((database, heap_stamp)) =>
   519                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   520                         case Some(build) =>
   521                           val current =
   522                             build.sources == sources_stamp(name) &&
   523                             build.input_heaps == ancestor_heaps &&
   524                             build.output_heap == heap_stamp &&
   525                             !(do_output && heap_stamp.isEmpty) &&
   526                             build.return_code == 0
   527                           (current, heap_stamp)
   528                         case None => (false, None)
   529                       }
   530                     case None => (false, None)
   531                   }
   532                 }
   533                 val all_current = current && ancestor_results.forall(_.current)
   534 
   535                 if (all_current)
   536                   loop(pending - name, running,
   537                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   538                 else if (no_build) {
   539                   if (verbose) progress.echo("Skipping " + name + " ...")
   540                   loop(pending - name, running,
   541                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   542                 }
   543                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   544                   val numa_node = numa_nodes.next(used_node(_))
   545                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   546                   val job =
   547                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   548                       verbose, pide, numa_node, queue.command_timings(name))
   549                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   550                 }
   551                 else {
   552                   progress.echo(name + " CANCELLED")
   553                   loop(pending - name, running,
   554                     results + (name -> Result(false, heap_stamp, None, info)))
   555                 }
   556               case None => sleep(); loop(pending, running, results)
   557             }
   558             ///}}}
   559           case None => sleep(); loop(pending, running, results)
   560         }
   561       }
   562     }
   563 
   564 
   565     /* build results */
   566 
   567     val results0 =
   568       if (deps.is_empty) {
   569         progress.echo_warning("Nothing to build")
   570         Map.empty[String, Result]
   571       }
   572       else loop(queue, Map.empty, Map.empty)
   573 
   574     val results =
   575       new Results(
   576         (for ((name, result) <- results0.iterator)
   577           yield (name, (result.process, result.info))).toMap)
   578 
   579     if (results.rc != 0 && (verbose || !no_build)) {
   580       val unfinished =
   581         (for {
   582           name <- results.sessions.iterator
   583           if !results(name).ok
   584          } yield name).toList.sorted
   585       progress.echo("Unfinished session(s): " + commas(unfinished))
   586     }
   587 
   588 
   589     /* global browser info */
   590 
   591     if (!no_build) {
   592       val browser_chapters =
   593         (for {
   594           (name, result) <- results0.iterator
   595           if result.ok
   596           info = full_sessions(name)
   597           if info.options.bool("browser_info")
   598         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   599             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   600 
   601       for ((chapter, entries) <- browser_chapters)
   602         Present.update_chapter_index(store.browser_info, chapter, entries)
   603 
   604       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   605     }
   606 
   607     results
   608   }
   609 
   610 
   611   /* Isabelle tool wrapper */
   612 
   613   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   614   {
   615     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   616 
   617     var select_dirs: List[Path] = Nil
   618     var numa_shuffling = false
   619     var pide = false
   620     var requirements = false
   621     var exclude_session_groups: List[String] = Nil
   622     var all_sessions = false
   623     var build_heap = false
   624     var clean_build = false
   625     var dirs: List[Path] = Nil
   626     var session_groups: List[String] = Nil
   627     var max_jobs = 1
   628     var check_keywords: Set[String] = Set.empty
   629     var list_files = false
   630     var no_build = false
   631     var options = (Options.init() /: build_options)(_ + _)
   632     var system_mode = false
   633     var verbose = false
   634     var exclude_sessions: List[String] = Nil
   635 
   636     val getopts = Getopts("""
   637 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   638 
   639   Options are:
   640     -D DIR       include session directory and select its sessions
   641     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   642     -P           build via PIDE protocol
   643     -R           operate on requirements of selected sessions
   644     -X NAME      exclude sessions from group NAME and all descendants
   645     -a           select all sessions
   646     -b           build heap images
   647     -c           clean build
   648     -d DIR       include session directory
   649     -g NAME      select session group NAME
   650     -j INT       maximum number of parallel jobs (default 1)
   651     -k KEYWORD   check theory sources for conflicts with proposed keywords
   652     -l           list session source files
   653     -n           no build -- test dependencies only
   654     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   655     -s           system build mode: produce output in ISABELLE_HOME
   656     -v           verbose
   657     -x NAME      exclude session NAME and all descendants
   658 
   659   Build and manage Isabelle sessions, depending on implicit settings:
   660 
   661 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   662       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   663       "N" -> (_ => numa_shuffling = true),
   664       "P" -> (_ => pide = true),
   665       "R" -> (_ => requirements = true),
   666       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   667       "a" -> (_ => all_sessions = true),
   668       "b" -> (_ => build_heap = true),
   669       "c" -> (_ => clean_build = true),
   670       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   671       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   672       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   673       "k:" -> (arg => check_keywords = check_keywords + arg),
   674       "l" -> (_ => list_files = true),
   675       "n" -> (_ => no_build = true),
   676       "o:" -> (arg => options = options + arg),
   677       "s" -> (_ => system_mode = true),
   678       "v" -> (_ => verbose = true),
   679       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   680 
   681     val sessions = getopts(args)
   682 
   683     val progress = new Console_Progress(verbose = verbose)
   684 
   685     val start_date = Date.now()
   686 
   687     if (verbose) {
   688       progress.echo(
   689         "Started at " + Build_Log.print_date(start_date) +
   690           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   691       progress.echo(Build_Log.Settings.show() + "\n")
   692     }
   693 
   694     val results =
   695       progress.interrupt_handler {
   696         build(options, progress,
   697           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   698           build_heap = build_heap,
   699           clean_build = clean_build,
   700           dirs = dirs,
   701           select_dirs = select_dirs,
   702           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   703           max_jobs = max_jobs,
   704           list_files = list_files,
   705           check_keywords = check_keywords,
   706           no_build = no_build,
   707           system_mode = system_mode,
   708           verbose = verbose,
   709           pide = pide,
   710           requirements = requirements,
   711           all_sessions = all_sessions,
   712           exclude_session_groups = exclude_session_groups,
   713           exclude_sessions = exclude_sessions,
   714           session_groups = session_groups,
   715           sessions = sessions)
   716       }
   717     val end_date = Date.now()
   718     val elapsed_time = end_date.time - start_date.time
   719 
   720     if (verbose) {
   721       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   722     }
   723 
   724     val total_timing =
   725       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   726         copy(elapsed = elapsed_time)
   727     progress.echo(total_timing.message_resources)
   728 
   729     sys.exit(results.rc)
   730   })
   731 }