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