# HG changeset patch
# User wenzelm
# Date 1621802790 -7200
# Node ID 734d5d3fbd9d19fdc9548c060c0bd161acfdf1a7
# Parent  ac7f41b66e1b0ba9cb4dd5e6e504fbef1da839a8
syslog option for "isabelle build";

diff -r ac7f41b66e1b -r 734d5d3fbd9d NEWS
--- a/NEWS	Sun May 23 21:03:32 2021 +0200
+++ b/NEWS	Sun May 23 22:46:30 2021 +0200
@@ -226,6 +226,10 @@
 
 *** System ***
 
+* Command-line tool "isabelle build" supports option -L FILE for syslog
+messages. Such messages can be produced in Isabelle/ML via formal
+Output.system_message or informal Output.physical_stderr.
+
 * Command-line tool "isabelle version" supports repository archives
 (without full .hg directory). More options.
 
diff -r ac7f41b66e1b -r 734d5d3fbd9d src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun May 23 21:03:32 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Sun May 23 22:46:30 2021 +0200
@@ -326,6 +326,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
+    -L FILE      append syslog messages to given FILE
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -460,6 +461,11 @@
   the source files that contribute to a session.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-L\<close>~\<open>FILE\<close> appends syslog messages to the given file. Such messages
+  can be produced in Isabelle/ML via formal \<^ML>\<open>Output.system_message\<close> or
+  informal \<^ML>\<open>Output.physical_stderr\<close>.
+
+  \<^medskip>
   Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
   uses allowed). The theory sources are checked for conflicts wrt.\ this
   hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
diff -r ac7f41b66e1b -r 734d5d3fbd9d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 23 21:03:32 2021 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 23 22:46:30 2021 +0200
@@ -169,6 +169,7 @@
     selection: Sessions.Selection = Sessions.Selection.empty,
     presentation: Presentation.Context = Presentation.Context.none,
     progress: Progress = new Progress,
+    log: Logger = No_Logger,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
@@ -418,7 +419,7 @@
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Build_Job(progress, session_name, info, deps, store, do_store,
-                      verbose, numa_node, queue.command_timings(session_name))
+                      verbose, numa_node, log, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
@@ -528,6 +529,7 @@
 
     var base_sessions: List[String] = Nil
     var select_dirs: List[Path] = Nil
+    var log: Logger = No_Logger
     var numa_shuffling = false
     var presentation = Presentation.Context.none
     var requirements = false
@@ -554,6 +556,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
+    -L FILE      append syslog messages to given FILE
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -579,6 +582,7 @@
 """ + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "L:" -> (arg => log = Logger.make(Some(Path.explode(arg)))),
       "N" -> (_ => numa_shuffling = true),
       "P:" -> (arg => presentation = Presentation.Context.make(arg)),
       "R" -> (_ => requirements = true),
@@ -625,6 +629,7 @@
             sessions = sessions),
           presentation = presentation,
           progress = progress,
+          log = log,
           check_unknown_files = Mercurial.is_repository(Path.ISABELLE_HOME),
           build_heap = build_heap,
           clean_build = clean_build,
diff -r ac7f41b66e1b -r 734d5d3fbd9d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sun May 23 21:03:32 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Sun May 23 22:46:30 2021 +0200
@@ -204,6 +204,7 @@
   do_store: Boolean,
   verbose: Boolean,
   val numa_node: Option[Int],
+  log: Logger,
   command_timings0: List[Properties.T])
 {
   val options: Options = NUMA.policy_options(info.options, numa_node)
@@ -232,7 +233,8 @@
         }
         else Nil
 
-      val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
+      val resources =
+        new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
       val session =
         new Session(options, resources) {
           override val cache: XML.Cache = store.cache
@@ -389,6 +391,8 @@
         {
           case msg: Prover.Output =>
             val message = msg.message
+            if (msg.is_syslog) resources.log(msg.toString)
+
             if (msg.is_stdout) {
               stdout ++= Symbol.encode(XML.content(message))
             }