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