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