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