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