src/Pure/Tools/build.scala
author wenzelm
Sun May 14 17:05:06 2017 +0200 (2017-05-14)
changeset 65828 02dd430d80c5
parent 65827 3bba3856b56c
child 65831 3b197547c1d4
permissions -rw-r--r--
tuned signature;
     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 = new Resources(deps(parent))
   227           val session = new Session(options, resources)
   228           val handler = new Handler(progress, session, name)
   229           session.init_protocol_handler(handler)
   230 
   231           val session_result = Future.promise[Process_Result]
   232 
   233           Isabelle_Process.start(session, options, logic = parent,
   234             cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
   235             phase_changed =
   236             {
   237               case Session.Ready => session.protocol_command("build_session", args_yxml)
   238               case Session.Terminated(result) => session_result.fulfill(result)
   239               case _ =>
   240             })
   241 
   242           val result = session_result.join
   243           handler.result_error.join match {
   244             case "" => result
   245             case msg =>
   246               result.copy(
   247                 rc = result.rc max 1,
   248                 out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
   249           }
   250         }
   251         else {
   252           val args_file = Isabelle_System.tmp_file("build")
   253           File.write(args_file, args_yxml)
   254 
   255           val eval =
   256             "Command_Line.tool0 (fn () => (" +
   257             "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
   258             (if (do_output) "; " + save_heap else "") + "));"
   259 
   260           val process =
   261             if (Sessions.is_pure(name)) {
   262               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
   263                 args =
   264                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
   265                   List("--eval", eval),
   266                 env = env, sessions = Some(sessions), store = store,
   267                 cleanup = () => args_file.delete)
   268             }
   269             else {
   270               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
   271                 env = env, sessions = Some(sessions), store = store,
   272                 cleanup = () => args_file.delete)
   273             }
   274 
   275           process.result(
   276             progress_stdout = (line: String) =>
   277               Library.try_unprefix("\floading_theory = ", line) match {
   278                 case Some(theory) => progress.theory(name, theory)
   279                 case None =>
   280               },
   281             progress_limit =
   282               options.int("process_output_limit") match {
   283                 case 0 => None
   284                 case m => Some(m * 1000000L)
   285               },
   286             strict = false)
   287         }
   288       }
   289 
   290     def terminate: Unit = future_result.cancel
   291     def is_finished: Boolean = future_result.is_finished
   292 
   293     @volatile private var was_timeout = false
   294     private val timeout_request: Option[Event_Timer.Request] =
   295     {
   296       if (info.timeout > Time.zero)
   297         Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
   298       else None
   299     }
   300 
   301     def join: Process_Result =
   302     {
   303       val result = future_result.join
   304 
   305       if (result.ok)
   306         Present.finish(progress, store.browser_info, graph_file, info, name)
   307 
   308       graph_file.delete
   309       timeout_request.foreach(_.cancel)
   310 
   311       if (result.interrupted) {
   312         if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
   313         else result.error(Output.error_message_text("Interrupt"))
   314       }
   315       else result
   316     }
   317   }
   318 
   319 
   320 
   321   /** build with results **/
   322 
   323   class Results private[Build](results: Map[String, (Option[Process_Result], Sessions.Info)])
   324   {
   325     def sessions: Set[String] = results.keySet
   326     def cancelled(name: String): Boolean = results(name)._1.isEmpty
   327     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
   328     def info(name: String): Sessions.Info = results(name)._2
   329     val rc =
   330       (0 /: results.iterator.map(
   331         { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
   332     def ok: Boolean = rc == 0
   333 
   334     override def toString: String = rc.toString
   335   }
   336 
   337   def build(
   338     options: Options,
   339     progress: Progress = No_Progress,
   340     build_heap: Boolean = false,
   341     clean_build: Boolean = false,
   342     dirs: List[Path] = Nil,
   343     select_dirs: List[Path] = Nil,
   344     numa_shuffling: Boolean = false,
   345     max_jobs: Int = 1,
   346     list_files: Boolean = false,
   347     check_keywords: Set[String] = Set.empty,
   348     no_build: Boolean = false,
   349     system_mode: Boolean = false,
   350     verbose: Boolean = false,
   351     pide: Boolean = false,
   352     requirements: Boolean = false,
   353     all_sessions: Boolean = false,
   354     exclude_session_groups: List[String] = Nil,
   355     exclude_sessions: List[String] = Nil,
   356     session_groups: List[String] = Nil,
   357     sessions: List[String] = Nil,
   358     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   359   {
   360     /* session selection and dependencies */
   361 
   362     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   363 
   364     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
   365 
   366     val (selected, selected_sessions) =
   367       full_sessions.selection(
   368           Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   369             exclude_sessions, session_groups, sessions) + selection)
   370 
   371     val deps =
   372       Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
   373         verbose = verbose, list_files = list_files, check_keywords = check_keywords,
   374         global_theories = full_sessions.global_theories)
   375 
   376     def sources_stamp(name: String): List[String] =
   377       (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
   378 
   379 
   380     /* main build process */
   381 
   382     val store = Sessions.store(system_mode)
   383     val queue = Queue(selected_sessions, store)
   384 
   385     store.prepare_output()
   386 
   387     // optional cleanup
   388     if (clean_build) {
   389       for (name <- full_sessions.build_descendants(selected)) {
   390         val files =
   391           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
   392             map(store.output_dir + _).filter(_.is_file)
   393         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
   394         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
   395       }
   396     }
   397 
   398     // scheduler loop
   399     case class Result(
   400       current: Boolean, heap_stamp: Option[String],
   401       process: Option[Process_Result], info: Sessions.Info)
   402     {
   403       def ok: Boolean =
   404         process match {
   405           case None => false
   406           case Some(res) => res.rc == 0
   407         }
   408     }
   409 
   410     def sleep()
   411     {
   412       try { Thread.sleep(500) }
   413       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   414     }
   415 
   416     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   417 
   418     @tailrec def loop(
   419       pending: Queue,
   420       running: Map[String, (List[String], Job)],
   421       results: Map[String, Result]): Map[String, Result] =
   422     {
   423       def used_node(i: Int): Boolean =
   424         running.iterator.exists(
   425           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   426 
   427       if (pending.is_empty) results
   428       else {
   429         if (progress.stopped)
   430           for ((_, (_, job)) <- running) job.terminate
   431 
   432         running.find({ case (_, (_, job)) => job.is_finished }) match {
   433           case Some((name, (input_heaps, job))) =>
   434             //{{{ finish job
   435 
   436             val process_result = job.join
   437             process_result.err_lines.foreach(progress.echo(_))
   438             if (process_result.ok)
   439               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   440 
   441             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   442             val process_result_tail =
   443             {
   444               val tail = job.info.options.int("process_output_tail")
   445               process_result.copy(
   446                 out_lines =
   447                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   448                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   449             }
   450 
   451             val heap_stamp =
   452               if (process_result.ok) {
   453                 (store.output_dir + store.log(name)).file.delete
   454                 val heap_stamp =
   455                   for (path <- job.output_path if path.is_file)
   456                     yield Sessions.write_heap_digest(path)
   457 
   458                 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   459 
   460                 heap_stamp
   461               }
   462               else {
   463                 (store.output_dir + Path.basic(name)).file.delete
   464                 (store.output_dir + store.log_gz(name)).file.delete
   465 
   466                 File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   467                 progress.echo(name + " FAILED")
   468                 if (!process_result.interrupted) progress.echo(process_result_tail.out)
   469 
   470                 None
   471               }
   472 
   473             // write database
   474             {
   475               val database = store.output_dir + store.database(name)
   476               database.file.delete
   477 
   478               using(SQLite.open_database(database))(db =>
   479                 store.write_session_info(db, name,
   480                   build_log =
   481                     Build_Log.Log_File(name, process_result.out_lines).
   482                       parse_session_info(
   483                         command_timings = true, ml_statistics = true, task_statistics = true),
   484                   build =
   485                     Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   486             }
   487 
   488             loop(pending - name, running - name,
   489               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   490             //}}}
   491           case None if running.size < (max_jobs max 1) =>
   492             //{{{ check/start next job
   493             pending.dequeue(running.isDefinedAt(_)) match {
   494               case Some((name, info)) =>
   495                 val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
   496                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   497 
   498                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   499 
   500                 val (current, heap_stamp) =
   501                 {
   502                   store.find_database_heap(name) match {
   503                     case Some((database, heap_stamp)) =>
   504                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   505                         case Some(build) =>
   506                           val current =
   507                             build.sources == sources_stamp(name) &&
   508                             build.input_heaps == ancestor_heaps &&
   509                             build.output_heap == heap_stamp &&
   510                             !(do_output && heap_stamp.isEmpty) &&
   511                             build.return_code == 0
   512                           (current, heap_stamp)
   513                         case None => (false, None)
   514                       }
   515                     case None => (false, None)
   516                   }
   517                 }
   518                 val all_current = current && ancestor_results.forall(_.current)
   519 
   520                 if (all_current)
   521                   loop(pending - name, running,
   522                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   523                 else if (no_build) {
   524                   if (verbose) progress.echo("Skipping " + name + " ...")
   525                   loop(pending - name, running,
   526                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   527                 }
   528                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   529                   val numa_node = numa_nodes.next(used_node(_))
   530                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   531                   val job =
   532                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   533                       verbose, pide, numa_node, queue.command_timings(name))
   534                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   535                 }
   536                 else {
   537                   progress.echo(name + " CANCELLED")
   538                   loop(pending - name, running,
   539                     results + (name -> Result(false, heap_stamp, None, info)))
   540                 }
   541               case None => sleep(); loop(pending, running, results)
   542             }
   543             ///}}}
   544           case None => sleep(); loop(pending, running, results)
   545         }
   546       }
   547     }
   548 
   549 
   550     /* build results */
   551 
   552     val results0 =
   553       if (deps.is_empty) {
   554         progress.echo_warning("Nothing to build")
   555         Map.empty[String, Result]
   556       }
   557       else loop(queue, Map.empty, Map.empty)
   558 
   559     val results =
   560       new Results(
   561         (for ((name, result) <- results0.iterator)
   562           yield (name, (result.process, result.info))).toMap)
   563 
   564     if (results.rc != 0 && (verbose || !no_build)) {
   565       val unfinished =
   566         (for {
   567           name <- results.sessions.iterator
   568           if !results(name).ok
   569          } yield name).toList.sorted
   570       progress.echo("Unfinished session(s): " + commas(unfinished))
   571     }
   572 
   573 
   574     /* global browser info */
   575 
   576     if (!no_build) {
   577       val browser_chapters =
   578         (for {
   579           (name, result) <- results0.iterator
   580           if result.ok
   581           info = full_sessions(name)
   582           if info.options.bool("browser_info")
   583         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   584             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   585 
   586       for ((chapter, entries) <- browser_chapters)
   587         Present.update_chapter_index(store.browser_info, chapter, entries)
   588 
   589       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   590     }
   591 
   592     results
   593   }
   594 
   595 
   596   /* Isabelle tool wrapper */
   597 
   598   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   599   {
   600     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   601 
   602     var select_dirs: List[Path] = Nil
   603     var numa_shuffling = false
   604     var pide = false
   605     var requirements = false
   606     var exclude_session_groups: List[String] = Nil
   607     var all_sessions = false
   608     var build_heap = false
   609     var clean_build = false
   610     var dirs: List[Path] = Nil
   611     var session_groups: List[String] = Nil
   612     var max_jobs = 1
   613     var check_keywords: Set[String] = Set.empty
   614     var list_files = false
   615     var no_build = false
   616     var options = (Options.init() /: build_options)(_ + _)
   617     var system_mode = false
   618     var verbose = false
   619     var exclude_sessions: List[String] = Nil
   620 
   621     val getopts = Getopts("""
   622 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   623 
   624   Options are:
   625     -D DIR       include session directory and select its sessions
   626     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   627     -P           build via PIDE protocol
   628     -R           operate on requirements of selected sessions
   629     -X NAME      exclude sessions from group NAME and all descendants
   630     -a           select all sessions
   631     -b           build heap images
   632     -c           clean build
   633     -d DIR       include session directory
   634     -g NAME      select session group NAME
   635     -j INT       maximum number of parallel jobs (default 1)
   636     -k KEYWORD   check theory sources for conflicts with proposed keywords
   637     -l           list session source files
   638     -n           no build -- test dependencies only
   639     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   640     -s           system build mode: produce output in ISABELLE_HOME
   641     -v           verbose
   642     -x NAME      exclude session NAME and all descendants
   643 
   644   Build and manage Isabelle sessions, depending on implicit settings:
   645 
   646 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   647       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   648       "N" -> (_ => numa_shuffling = true),
   649       "P" -> (_ => pide = true),
   650       "R" -> (_ => requirements = true),
   651       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   652       "a" -> (_ => all_sessions = true),
   653       "b" -> (_ => build_heap = true),
   654       "c" -> (_ => clean_build = true),
   655       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   656       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   657       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   658       "k:" -> (arg => check_keywords = check_keywords + arg),
   659       "l" -> (_ => list_files = true),
   660       "n" -> (_ => no_build = true),
   661       "o:" -> (arg => options = options + arg),
   662       "s" -> (_ => system_mode = true),
   663       "v" -> (_ => verbose = true),
   664       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   665 
   666     val sessions = getopts(args)
   667 
   668     val progress = new Console_Progress(verbose = verbose)
   669 
   670     val start_date = Date.now()
   671 
   672     if (verbose) {
   673       progress.echo(
   674         "Started at " + Build_Log.print_date(start_date) +
   675           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   676       progress.echo(Build_Log.Settings.show() + "\n")
   677     }
   678 
   679     val results =
   680       progress.interrupt_handler {
   681         build(options, progress,
   682           build_heap = build_heap,
   683           clean_build = clean_build,
   684           dirs = dirs,
   685           select_dirs = select_dirs,
   686           numa_shuffling = NUMA.enabled_warning(numa_shuffling),
   687           max_jobs = max_jobs,
   688           list_files = list_files,
   689           check_keywords = check_keywords,
   690           no_build = no_build,
   691           system_mode = system_mode,
   692           verbose = verbose,
   693           pide = pide,
   694           requirements = requirements,
   695           all_sessions = all_sessions,
   696           exclude_session_groups = exclude_session_groups,
   697           exclude_sessions = exclude_sessions,
   698           session_groups = session_groups,
   699           sessions = sessions)
   700       }
   701     val end_date = Date.now()
   702     val elapsed_time = end_date.time - start_date.time
   703 
   704     if (verbose) {
   705       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   706     }
   707 
   708     val total_timing =
   709       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   710         copy(elapsed = elapsed_time)
   711     progress.echo(total_timing.message_resources)
   712 
   713     sys.exit(results.rc)
   714   })
   715 }