src/Pure/Tools/build.scala
author wenzelm
Sat Sep 02 12:09:07 2017 +0200 (20 months ago)
changeset 66594 c16ed3250de0
parent 66571 0fdeb24e535e
child 66595 fa10b0f589c3
permissions -rw-r--r--
tuned whitespace;
     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).check_errors
   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,
   420       heap_stamp: Option[String],
   421       process: Option[Process_Result],
   422       info: Sessions.Info)
   423     {
   424       def ok: Boolean =
   425         process match {
   426           case None => false
   427           case Some(res) => res.rc == 0
   428         }
   429     }
   430 
   431     def sleep()
   432     {
   433       try { Thread.sleep(500) }
   434       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
   435     }
   436 
   437     val numa_nodes = new NUMA.Nodes(numa_shuffling)
   438 
   439     @tailrec def loop(
   440       pending: Queue,
   441       running: Map[String, (List[String], Job)],
   442       results: Map[String, Result]): Map[String, Result] =
   443     {
   444       def used_node(i: Int): Boolean =
   445         running.iterator.exists(
   446           { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
   447 
   448       if (pending.is_empty) results
   449       else {
   450         if (progress.stopped)
   451           for ((_, (_, job)) <- running) job.terminate
   452 
   453         running.find({ case (_, (_, job)) => job.is_finished }) match {
   454           case Some((name, (input_heaps, job))) =>
   455             //{{{ finish job
   456 
   457             val process_result = job.join
   458             process_result.err_lines.foreach(progress.echo(_))
   459             if (process_result.ok)
   460               progress.echo("Finished " + name + " (" + process_result.timing.message_resources + ")")
   461 
   462             val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
   463             val process_result_tail =
   464             {
   465               val tail = job.info.options.int("process_output_tail")
   466               process_result.copy(
   467                 out_lines =
   468                   "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
   469                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
   470             }
   471 
   472             val heap_stamp =
   473               if (process_result.ok) {
   474                 (store.output_dir + store.log(name)).file.delete
   475                 val heap_stamp =
   476                   for (path <- job.output_path if path.is_file)
   477                     yield Sessions.write_heap_digest(path)
   478 
   479                 File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
   480 
   481                 heap_stamp
   482               }
   483               else {
   484                 (store.output_dir + Path.basic(name)).file.delete
   485                 (store.output_dir + store.log_gz(name)).file.delete
   486 
   487                 File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
   488                 progress.echo(name + " FAILED")
   489                 if (!process_result.interrupted) progress.echo(process_result_tail.out)
   490 
   491                 None
   492               }
   493 
   494             // write database
   495             {
   496               val database = store.output_dir + store.database(name)
   497               database.file.delete
   498 
   499               using(SQLite.open_database(database))(db =>
   500                 store.write_session_info(db, name,
   501                   build_log =
   502                     Build_Log.Log_File(name, process_result.out_lines).
   503                       parse_session_info(
   504                         command_timings = true, ml_statistics = true, task_statistics = true),
   505                   build =
   506                     Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   507             }
   508 
   509             loop(pending - name, running - name,
   510               results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
   511             //}}}
   512           case None if running.size < (max_jobs max 1) =>
   513             //{{{ check/start next job
   514             pending.dequeue(running.isDefinedAt(_)) match {
   515               case Some((name, info)) =>
   516                 val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
   517                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
   518 
   519                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
   520 
   521                 val (current, heap_stamp) =
   522                 {
   523                   store.find_database_heap(name) match {
   524                     case Some((database, heap_stamp)) =>
   525                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
   526                         case Some(build) =>
   527                           val current =
   528                             build.sources == sources_stamp(name) &&
   529                             build.input_heaps == ancestor_heaps &&
   530                             build.output_heap == heap_stamp &&
   531                             !(do_output && heap_stamp.isEmpty) &&
   532                             build.return_code == 0
   533                           (current, heap_stamp)
   534                         case None => (false, None)
   535                       }
   536                     case None => (false, None)
   537                   }
   538                 }
   539                 val all_current = current && ancestor_results.forall(_.current)
   540 
   541                 if (all_current)
   542                   loop(pending - name, running,
   543                     results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
   544                 else if (no_build) {
   545                   if (verbose) progress.echo("Skipping " + name + " ...")
   546                   loop(pending - name, running,
   547                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   548                 }
   549                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   550                   val numa_node = numa_nodes.next(used_node(_))
   551                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   552                   val job =
   553                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
   554                       verbose, pide, numa_node, queue.command_timings(name))
   555                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
   556                 }
   557                 else {
   558                   progress.echo(name + " CANCELLED")
   559                   loop(pending - name, running,
   560                     results + (name -> Result(false, heap_stamp, None, info)))
   561                 }
   562               case None => sleep(); loop(pending, running, results)
   563             }
   564             ///}}}
   565           case None => sleep(); loop(pending, running, results)
   566         }
   567       }
   568     }
   569 
   570 
   571     /* build results */
   572 
   573     val results0 =
   574       if (deps.is_empty) {
   575         progress.echo_warning("Nothing to build")
   576         Map.empty[String, Result]
   577       }
   578       else loop(queue, Map.empty, Map.empty)
   579 
   580     val results =
   581       new Results(
   582         (for ((name, result) <- results0.iterator)
   583           yield (name, (result.process, result.info))).toMap)
   584 
   585     if (results.rc != 0 && (verbose || !no_build)) {
   586       val unfinished =
   587         (for {
   588           name <- results.sessions.iterator
   589           if !results(name).ok
   590          } yield name).toList.sorted
   591       progress.echo("Unfinished session(s): " + commas(unfinished))
   592     }
   593 
   594 
   595     /* global browser info */
   596 
   597     if (!no_build) {
   598       val browser_chapters =
   599         (for {
   600           (name, result) <- results0.iterator
   601           if result.ok
   602           info = full_sessions(name)
   603           if info.options.bool("browser_info")
   604         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
   605             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
   606 
   607       for ((chapter, entries) <- browser_chapters)
   608         Present.update_chapter_index(store.browser_info, chapter, entries)
   609 
   610       if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
   611     }
   612 
   613     results
   614   }
   615 
   616 
   617   /* Isabelle tool wrapper */
   618 
   619   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   620   {
   621     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
   622 
   623     var select_dirs: List[Path] = Nil
   624     var numa_shuffling = false
   625     var pide = false
   626     var requirements = false
   627     var exclude_session_groups: List[String] = Nil
   628     var all_sessions = false
   629     var build_heap = false
   630     var clean_build = false
   631     var dirs: List[Path] = Nil
   632     var session_groups: List[String] = Nil
   633     var max_jobs = 1
   634     var check_keywords: Set[String] = Set.empty
   635     var list_files = false
   636     var no_build = false
   637     var options = (Options.init() /: build_options)(_ + _)
   638     var system_mode = false
   639     var verbose = false
   640     var exclude_sessions: List[String] = Nil
   641 
   642     val getopts = Getopts("""
   643 Usage: isabelle build [OPTIONS] [SESSIONS ...]
   644 
   645   Options are:
   646     -D DIR       include session directory and select its sessions
   647     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   648     -P           build via PIDE protocol
   649     -R           operate on requirements of selected sessions
   650     -X NAME      exclude sessions from group NAME and all descendants
   651     -a           select all sessions
   652     -b           build heap images
   653     -c           clean build
   654     -d DIR       include session directory
   655     -g NAME      select session group NAME
   656     -j INT       maximum number of parallel jobs (default 1)
   657     -k KEYWORD   check theory sources for conflicts with proposed keywords
   658     -l           list session source files
   659     -n           no build -- test dependencies only
   660     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   661     -s           system build mode: produce output in ISABELLE_HOME
   662     -v           verbose
   663     -x NAME      exclude session NAME and all descendants
   664 
   665   Build and manage Isabelle sessions, depending on implicit settings:
   666 
   667 """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
   668       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   669       "N" -> (_ => numa_shuffling = true),
   670       "P" -> (_ => pide = true),
   671       "R" -> (_ => requirements = true),
   672       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   673       "a" -> (_ => all_sessions = true),
   674       "b" -> (_ => build_heap = true),
   675       "c" -> (_ => clean_build = true),
   676       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   677       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   678       "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
   679       "k:" -> (arg => check_keywords = check_keywords + arg),
   680       "l" -> (_ => list_files = true),
   681       "n" -> (_ => no_build = true),
   682       "o:" -> (arg => options = options + arg),
   683       "s" -> (_ => system_mode = true),
   684       "v" -> (_ => verbose = true),
   685       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   686 
   687     val sessions = getopts(args)
   688 
   689     val progress = new Console_Progress(verbose = verbose)
   690 
   691     val start_date = Date.now()
   692 
   693     if (verbose) {
   694       progress.echo(
   695         "Started at " + Build_Log.print_date(start_date) +
   696           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
   697       progress.echo(Build_Log.Settings.show() + "\n")
   698     }
   699 
   700     val results =
   701       progress.interrupt_handler {
   702         build(options, progress,
   703           check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
   704           build_heap = build_heap,
   705           clean_build = clean_build,
   706           dirs = dirs,
   707           select_dirs = select_dirs,
   708           numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
   709           max_jobs = max_jobs,
   710           list_files = list_files,
   711           check_keywords = check_keywords,
   712           no_build = no_build,
   713           system_mode = system_mode,
   714           verbose = verbose,
   715           pide = pide,
   716           requirements = requirements,
   717           all_sessions = all_sessions,
   718           exclude_session_groups = exclude_session_groups,
   719           exclude_sessions = exclude_sessions,
   720           session_groups = session_groups,
   721           sessions = sessions)
   722       }
   723     val end_date = Date.now()
   724     val elapsed_time = end_date.time - start_date.time
   725 
   726     if (verbose) {
   727       progress.echo("\nFinished at " + Build_Log.print_date(end_date))
   728     }
   729 
   730     val total_timing =
   731       (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
   732         copy(elapsed = elapsed_time)
   733     progress.echo(total_timing.message_resources)
   734 
   735     sys.exit(results.rc)
   736   })
   737 }