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