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