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