author | wenzelm |
Sat, 30 Jul 2022 14:49:22 +0200 | |
changeset 75733 | d3430f302c2e |
parent 75454 | 295e1c9d2994 |
child 75737 | 288c4d4042cc |
permissions | -rw-r--r-- |
72662 | 1 |
/* Title: Pure/Tools/build_job.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build job running prover process, with rudimentary PIDE session. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import scala.collection.mutable |
|
11 |
||
12 |
||
75393 | 13 |
object Build_Job { |
72854 | 14 |
/* theory markup/messages from database */ |
15 |
||
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
16 |
def read_theory( |
72857 | 17 |
db_context: Sessions.Database_Context, |
74712 | 18 |
session_hierarchy: List[String], |
72867 | 19 |
theory: String, |
75393 | 20 |
unicode_symbols: Boolean = false |
21 |
): Option[Command] = { |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
22 |
def read(name: String): Export.Entry = |
74712 | 23 |
db_context.get_export(session_hierarchy, theory, name) |
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
24 |
|
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
25 |
def read_xml(name: String): XML.Body = |
73033 | 26 |
YXML.parse_body( |
27 |
Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), |
|
28 |
cache = db_context.cache) |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
29 |
|
75733 | 30 |
for { |
31 |
id <- Export.read_document_id(read) |
|
32 |
(thy_file, blobs_files) <- Export.read_files(read) |
|
33 |
} |
|
34 |
yield { |
|
35 |
val node_name = Resources.file_node(Path.explode(thy_file), theory = theory) |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
36 |
|
75733 | 37 |
val results = |
38 |
Command.Results.make( |
|
39 |
for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) |
|
40 |
yield i -> elem) |
|
41 |
||
42 |
val blobs = |
|
43 |
blobs_files.map { file => |
|
44 |
val path = Path.explode(file) |
|
45 |
val name = Resources.file_node(path) |
|
46 |
val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) |
|
47 |
Command.Blob(name, src_path, None) |
|
48 |
} |
|
49 |
val blobs_xml = |
|
50 |
for (i <- (1 to blobs.length).toList) |
|
51 |
yield read_xml(Export.MARKUP + i) |
|
72865
ebf72a3b8daa
clarified file sources: take from build database instead of file-system;
wenzelm
parents:
72864
diff
changeset
|
52 |
|
75733 | 53 |
val blobs_info = |
54 |
Command.Blobs_Info( |
|
55 |
for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml } |
|
56 |
yield { |
|
57 |
val text = XML.content(xml) |
|
58 |
val chunk = Symbol.Text_Chunk(text) |
|
59 |
val digest = SHA1.digest(Symbol.encode(text)) |
|
60 |
Exn.Res(Command.Blob(name, src_path, Some((digest, chunk)))) |
|
61 |
}) |
|
72864 | 62 |
|
75733 | 63 |
val thy_xml = read_xml(Export.MARKUP) |
64 |
val thy_source = XML.content(thy_xml) |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
65 |
|
75733 | 66 |
val markups_index = |
67 |
Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob) |
|
68 |
val markups = |
|
69 |
Command.Markups.make( |
|
70 |
for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) |
|
71 |
yield index -> Markup_Tree.from_XML(xml)) |
|
72 |
||
73 |
Command.unparsed(thy_source, theory = true, id = id, node_name = node_name, |
|
74 |
blobs_info = blobs_info, results = results, markups = markups) |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
75 |
} |
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
76 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
77 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
78 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
79 |
/* print messages */ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
80 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
81 |
def print_log( |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
82 |
options: Options, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
83 |
session_name: String, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
84 |
theories: List[String] = Nil, |
72878 | 85 |
verbose: Boolean = false, |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
86 |
progress: Progress = new Progress, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
87 |
margin: Double = Pretty.default_margin, |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
88 |
breakgain: Double = Pretty.default_breakgain, |
72873 | 89 |
metric: Pretty.Metric = Symbol.Metric, |
75393 | 90 |
unicode_symbols: Boolean = false |
91 |
): Unit = { |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
92 |
val store = Sessions.store(options) |
74755
510296c0d8d1
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents:
74731
diff
changeset
|
93 |
val session = new Session(options, Resources.empty) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
94 |
|
75394 | 95 |
using(store.open_database_context()) { db_context => |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
96 |
val result = |
75394 | 97 |
db_context.input_database(session_name) { (db, _) => |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
98 |
val theories = store.read_theories(db, session_name) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
99 |
val errors = store.read_errors(db, session_name) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
100 |
store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) |
75394 | 101 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
102 |
result match { |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
103 |
case None => error("Missing build database for session " + quote(session_name)) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
104 |
case Some((used_theories, errors, rc)) => |
73835 | 105 |
theories.filterNot(used_theories.toSet) match { |
106 |
case Nil => |
|
107 |
case bad => error("Unknown theories " + commas_quote(bad)) |
|
108 |
} |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
109 |
val print_theories = |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
110 |
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
111 |
for (thy <- print_theories) { |
72868 | 112 |
val thy_heading = "\nTheory " + quote(thy) + ":" |
74755
510296c0d8d1
clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;
wenzelm
parents:
74731
diff
changeset
|
113 |
read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols) |
72867 | 114 |
match { |
72863 | 115 |
case None => progress.echo(thy_heading + " MISSING") |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
116 |
case Some(command) => |
72958 | 117 |
val snapshot = Document.State.init.snippet(command) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
118 |
val rendering = new Rendering(snapshot, options, session) |
72878 | 119 |
val messages = |
120 |
rendering.text_messages(Text.Range.full) |
|
121 |
.filter(message => verbose || Protocol.is_exported(message.info)) |
|
72863 | 122 |
if (messages.nonEmpty) { |
72875 | 123 |
val line_document = Line.Document(command.source) |
72863 | 124 |
progress.echo(thy_heading) |
72875 | 125 |
for (Text.Info(range, elem) <- messages) { |
126 |
val line = line_document.position(range.start).line1 |
|
127 |
val pos = Position.Line_File(line, command.node_name.node) |
|
72863 | 128 |
progress.echo( |
72875 | 129 |
Protocol.message_text(elem, heading = true, pos = pos, |
130 |
margin = margin, breakgain = breakgain, metric = metric)) |
|
72863 | 131 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
132 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
133 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
134 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
135 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
136 |
if (errors.nonEmpty) { |
72867 | 137 |
val msg = Symbol.output(unicode_symbols, cat_lines(errors)) |
72868 | 138 |
progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
139 |
} |
74306 | 140 |
if (rc != Process_Result.RC.ok) { |
141 |
progress.echo("\n" + Process_Result.RC.print_long(rc)) |
|
142 |
} |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
143 |
} |
75394 | 144 |
} |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
145 |
} |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
146 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
147 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
148 |
/* Isabelle tool wrapper */ |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
149 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
150 |
val isabelle_tool = Isabelle_Tool("log", "print messages from build database", |
75394 | 151 |
Scala_Project.here, |
152 |
{ args => |
|
153 |
/* arguments */ |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
154 |
|
75394 | 155 |
var unicode_symbols = false |
156 |
var theories: List[String] = Nil |
|
157 |
var margin = Pretty.default_margin |
|
158 |
var options = Options.init() |
|
159 |
var verbose = false |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
160 |
|
75394 | 161 |
val getopts = Getopts(""" |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
162 |
Usage: isabelle log [OPTIONS] SESSION |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
163 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
164 |
Options are: |
72876 | 165 |
-T NAME restrict to given theories (multiple options possible) |
72867 | 166 |
-U output Unicode symbols |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
167 |
-m MARGIN margin for pretty printing (default: """ + margin + """) |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
168 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
73837
f72335f6a9ed
clarified documentation: tracing messages are not shown here;
wenzelm
parents:
73835
diff
changeset
|
169 |
-v print all messages, including information etc. |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
170 |
|
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
171 |
Print messages from the build database of the given session, without any |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
172 |
checks against current sources: results from a failed build can be |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
173 |
printed as well. |
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
174 |
""", |
75394 | 175 |
"T:" -> (arg => theories = theories ::: List(arg)), |
176 |
"U" -> (_ => unicode_symbols = true), |
|
177 |
"m:" -> (arg => margin = Value.Double.parse(arg)), |
|
178 |
"o:" -> (arg => options = options + arg), |
|
179 |
"v" -> (_ => verbose = true)) |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
180 |
|
75394 | 181 |
val more_args = getopts(args) |
182 |
val session_name = |
|
183 |
more_args match { |
|
184 |
case List(session_name) => session_name |
|
185 |
case _ => getopts.usage() |
|
186 |
} |
|
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
187 |
|
75394 | 188 |
val progress = new Console_Progress() |
72858
cb0c407fbc6e
added "isabelle log": print messages from build database;
wenzelm
parents:
72857
diff
changeset
|
189 |
|
75394 | 190 |
print_log(options, session_name, theories = theories, verbose = verbose, margin = margin, |
191 |
progress = progress, unicode_symbols = unicode_symbols) |
|
192 |
}) |
|
72848
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
193 |
} |
d5d0e36eda16
read theory with PIDE markup from session database;
wenzelm
parents:
72844
diff
changeset
|
194 |
|
72662 | 195 |
class Build_Job(progress: Progress, |
196 |
session_name: String, |
|
197 |
val info: Sessions.Info, |
|
198 |
deps: Sessions.Deps, |
|
199 |
store: Sessions.Store, |
|
200 |
do_store: Boolean, |
|
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73774
diff
changeset
|
201 |
log: Logger, |
73805
b73777a0c076
allow build session setup, e.g. for protocol handlers;
wenzelm
parents:
73804
diff
changeset
|
202 |
session_setup: (String, Session) => Unit, |
72662 | 203 |
val numa_node: Option[Int], |
75393 | 204 |
command_timings0: List[Properties.T] |
205 |
) { |
|
72662 | 206 |
val options: Options = NUMA.policy_options(info.options, numa_node) |
207 |
||
208 |
private val sessions_structure = deps.sessions_structure |
|
209 |
||
210 |
private val future_result: Future[Process_Result] = |
|
211 |
Future.thread("build", uninterruptible = true) { |
|
212 |
val parent = info.parent.getOrElse("") |
|
213 |
val base = deps(parent) |
|
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
214 |
val result_base = deps(session_name) |
72662 | 215 |
|
75454 | 216 |
val env = |
217 |
Isabelle_System.settings( |
|
218 |
List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) |
|
72662 | 219 |
|
220 |
val is_pure = Sessions.is_pure(session_name) |
|
221 |
||
222 |
val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil |
|
223 |
||
224 |
val eval_store = |
|
225 |
if (do_store) { |
|
226 |
(if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: |
|
227 |
List("ML_Heap.save_child " + |
|
228 |
ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) |
|
229 |
} |
|
230 |
else Nil |
|
231 |
||
73774 | 232 |
val resources = |
233 |
new Resources(sessions_structure, base, log = log, command_timings = command_timings0) |
|
72662 | 234 |
val session = |
235 |
new Session(options, resources) { |
|
74731
161e84e6b40a
just one cache, via HTML_Context, via Sessions.Store or Session;
wenzelm
parents:
74712
diff
changeset
|
236 |
override val cache: Term.Cache = store.cache |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
237 |
|
75393 | 238 |
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { |
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
239 |
result_base.load_commands.get(name.expand) match { |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
240 |
case Some(spans) => |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
241 |
val syntax = result_base.theory_syntax(name) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
242 |
Command.build_blobs_info(syntax, name, spans) |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
243 |
case None => Command.Blobs_Info.none |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
244 |
} |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
245 |
} |
72662 | 246 |
} |
247 |
||
75393 | 248 |
object Build_Session_Errors { |
72662 | 249 |
private val promise: Promise[List[String]] = Future.promise |
250 |
||
251 |
def result: Exn.Result[List[String]] = promise.join_result |
|
73367 | 252 |
def cancel(): Unit = promise.cancel() |
75393 | 253 |
def apply(errs: List[String]): Unit = { |
72662 | 254 |
try { promise.fulfill(errs) } |
255 |
catch { case _: IllegalStateException => } |
|
256 |
} |
|
257 |
} |
|
258 |
||
259 |
val export_consumer = |
|
74255 | 260 |
Export.consumer(store.open_database(session_name, output = true), store.cache, |
261 |
progress = progress) |
|
72662 | 262 |
|
263 |
val stdout = new StringBuilder(1000) |
|
264 |
val stderr = new StringBuilder(1000) |
|
265 |
val command_timings = new mutable.ListBuffer[Properties.T] |
|
266 |
val theory_timings = new mutable.ListBuffer[Properties.T] |
|
267 |
val session_timings = new mutable.ListBuffer[Properties.T] |
|
268 |
val runtime_statistics = new mutable.ListBuffer[Properties.T] |
|
269 |
val task_statistics = new mutable.ListBuffer[Properties.T] |
|
270 |
||
271 |
def fun( |
|
272 |
name: String, |
|
273 |
acc: mutable.ListBuffer[Properties.T], |
|
75393 | 274 |
unapply: Properties.T => Option[Properties.T] |
275 |
): (String, Session.Protocol_Function) = { |
|
72662 | 276 |
name -> ((msg: Prover.Protocol_Output) => |
277 |
unapply(msg.properties) match { |
|
278 |
case Some(props) => acc += props; true |
|
279 |
case _ => false |
|
280 |
}) |
|
281 |
} |
|
282 |
||
75393 | 283 |
session.init_protocol_handler(new Session.Protocol_Handler { |
73367 | 284 |
override def exit(): Unit = Build_Session_Errors.cancel() |
72662 | 285 |
|
75393 | 286 |
private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { |
72662 | 287 |
val (rc, errors) = |
288 |
try { |
|
75393 | 289 |
val (rc, errs) = { |
72662 | 290 |
import XML.Decode._ |
291 |
pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) |
|
292 |
} |
|
293 |
val errors = |
|
294 |
for (err <- errs) yield { |
|
295 |
val prt = Protocol_Message.expose_no_reports(err) |
|
296 |
Pretty.string_of(prt, metric = Symbol.Metric) |
|
297 |
} |
|
298 |
(rc, errors) |
|
299 |
} |
|
74306 | 300 |
catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) } |
72662 | 301 |
|
302 |
session.protocol_command("Prover.stop", rc.toString) |
|
303 |
Build_Session_Errors(errors) |
|
304 |
true |
|
305 |
} |
|
306 |
||
307 |
private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
|
308 |
msg.properties match { |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
309 |
case Markup.Loading_Theory(Markup.Name(name)) => |
72662 | 310 |
progress.theory(Progress.Theory(name, session = session_name)) |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
311 |
false |
72662 | 312 |
case _ => false |
313 |
} |
|
314 |
||
74685 | 315 |
private def export_(msg: Prover.Protocol_Output): Boolean = |
72662 | 316 |
msg.properties match { |
317 |
case Protocol.Export(args) => |
|
73559 | 318 |
export_consumer(session_name, args, msg.chunk) |
72662 | 319 |
true |
320 |
case _ => false |
|
321 |
} |
|
322 |
||
75440 | 323 |
override val functions: Session.Protocol_Functions = |
72662 | 324 |
List( |
325 |
Markup.Build_Session_Finished.name -> build_session_finished, |
|
326 |
Markup.Loading_Theory.name -> loading_theory, |
|
74685 | 327 |
Markup.EXPORT -> export_, |
72662 | 328 |
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), |
329 |
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), |
|
330 |
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) |
|
331 |
}) |
|
332 |
||
75393 | 333 |
session.command_timings += Session.Consumer("command_timings") { |
334 |
case Session.Command_Timing(props) => |
|
335 |
for { |
|
336 |
elapsed <- Markup.Elapsed.unapply(props) |
|
337 |
elapsed_time = Time.seconds(elapsed) |
|
338 |
if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") |
|
339 |
} command_timings += props.filter(Markup.command_timing_property) |
|
340 |
} |
|
72711 | 341 |
|
75393 | 342 |
session.runtime_statistics += Session.Consumer("ML_statistics") { |
343 |
case Session.Runtime_Statistics(props) => runtime_statistics += props |
|
344 |
} |
|
72662 | 345 |
|
75393 | 346 |
session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { |
347 |
case snapshot => |
|
348 |
if (!progress.stopped) { |
|
349 |
val rendering = new Rendering(snapshot, options, session) |
|
72730 | 350 |
|
75393 | 351 |
def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { |
352 |
if (!progress.stopped) { |
|
353 |
val theory_name = snapshot.node_name.theory |
|
354 |
val args = |
|
355 |
Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) |
|
356 |
val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) |
|
357 |
if (!bytes.is_empty) export_consumer(session_name, args, bytes) |
|
74258 | 358 |
} |
75393 | 359 |
} |
360 |
def export_text(name: String, text: String, compress: Boolean = true): Unit = |
|
361 |
export_(name, List(XML.Text(text)), compress = compress) |
|
72730 | 362 |
|
75393 | 363 |
for (command <- snapshot.snippet_command) { |
364 |
export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) |
|
365 |
} |
|
72844 | 366 |
|
75393 | 367 |
export_text(Export.FILES, |
368 |
cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) |
|
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72783
diff
changeset
|
369 |
|
75393 | 370 |
for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { |
371 |
export_(Export.MARKUP + (i + 1), xml) |
|
372 |
} |
|
373 |
export_(Export.MARKUP, snapshot.xml_markup()) |
|
374 |
export_(Export.MESSAGES, snapshot.messages.map(_._1)) |
|
74258 | 375 |
|
75393 | 376 |
val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) |
377 |
export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations)) |
|
378 |
} |
|
379 |
} |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72683
diff
changeset
|
380 |
|
75393 | 381 |
session.all_messages += Session.Consumer[Any]("build_session_output") { |
382 |
case msg: Prover.Output => |
|
383 |
val message = msg.message |
|
384 |
if (msg.is_system) resources.log(Protocol.message_text(message)) |
|
73774 | 385 |
|
75393 | 386 |
if (msg.is_stdout) { |
387 |
stdout ++= Symbol.encode(XML.content(message)) |
|
388 |
} |
|
389 |
else if (msg.is_stderr) { |
|
390 |
stderr ++= Symbol.encode(XML.content(message)) |
|
391 |
} |
|
392 |
else if (msg.is_exit) { |
|
393 |
val err = |
|
394 |
"Prover terminated" + |
|
395 |
(msg.properties match { |
|
396 |
case Markup.Process_Result(result) => ": " + result.print_rc |
|
397 |
case _ => "" |
|
398 |
}) |
|
399 |
Build_Session_Errors(List(err)) |
|
400 |
} |
|
401 |
case _ => |
|
402 |
} |
|
72662 | 403 |
|
73805
b73777a0c076
allow build session setup, e.g. for protocol handlers;
wenzelm
parents:
73804
diff
changeset
|
404 |
session_setup(session_name, session) |
b73777a0c076
allow build session setup, e.g. for protocol handlers;
wenzelm
parents:
73804
diff
changeset
|
405 |
|
72662 | 406 |
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
407 |
||
408 |
val process = |
|
73802 | 409 |
Isabelle_Process.start(session, options, sessions_structure, store, |
72662 | 410 |
logic = parent, raw_ml_system = is_pure, |
411 |
use_prelude = use_prelude, eval_main = eval_main, |
|
412 |
cwd = info.dir.file, env = env) |
|
413 |
||
414 |
val build_errors = |
|
73367 | 415 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { |
416 |
Exn.capture { process.await_startup() } match { |
|
72662 | 417 |
case Exn.Res(_) => |
418 |
val resources_yxml = resources.init_session_yxml |
|
74144 | 419 |
val encode_options: XML.Encode.T[Options] = |
420 |
options => session.prover_options(options).encode |
|
72662 | 421 |
val args_yxml = |
422 |
YXML.string_of_body( |
|
423 |
{ |
|
424 |
import XML.Encode._ |
|
74144 | 425 |
pair(string, list(pair(encode_options, list(pair(string, properties)))))( |
72662 | 426 |
(session_name, info.theories)) |
427 |
}) |
|
428 |
session.protocol_command("build_session", resources_yxml, args_yxml) |
|
429 |
Build_Session_Errors.result |
|
430 |
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
|
431 |
} |
|
432 |
} |
|
433 |
||
434 |
val process_result = |
|
73367 | 435 |
Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } |
72662 | 436 |
|
72697 | 437 |
session.stop() |
438 |
||
72662 | 439 |
val export_errors = |
440 |
export_consumer.shutdown(close = true).map(Output.error_message_text) |
|
441 |
||
72699 | 442 |
val (document_output, document_errors) = |
72662 | 443 |
try { |
72881 | 444 |
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { |
75394 | 445 |
using(store.open_database_context()) { db_context => |
446 |
val documents = |
|
447 |
Document_Build.build_documents( |
|
448 |
Document_Build.context(session_name, deps, db_context, progress = progress), |
|
449 |
output_sources = info.document_output, |
|
450 |
output_pdf = info.document_output) |
|
451 |
db_context.output_database(session_name)(db => |
|
452 |
documents.foreach(_.write(db, session_name))) |
|
453 |
(documents.flatMap(_.log_lines), Nil) |
|
454 |
} |
|
72662 | 455 |
} |
72881 | 456 |
else (Nil, Nil) |
72662 | 457 |
} |
72882 | 458 |
catch { |
73718 | 459 |
case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) |
72882 | 460 |
case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) |
461 |
} |
|
72662 | 462 |
|
75393 | 463 |
val result = { |
72738
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
464 |
val theory_timing = |
75438 | 465 |
theory_timings.iterator.flatMap( |
75425 | 466 |
{ |
75438 | 467 |
case props @ Markup.Name(name) => Some(name -> props) |
468 |
case _ => None |
|
75425 | 469 |
}).toMap |
72738
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
470 |
val used_theory_timings = |
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
471 |
for { (name, _) <- deps(session_name).used_theories } |
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
472 |
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) |
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
473 |
|
72662 | 474 |
val more_output = |
475 |
Library.trim_line(stdout.toString) :: |
|
476 |
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: |
|
72738
a4d7da18ac5c
store timings for used_theories in canonical order, with reconstructed store.read_theories;
wenzelm
parents:
72730
diff
changeset
|
477 |
used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) ::: |
72662 | 478 |
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: |
479 |
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: |
|
480 |
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: |
|
72699 | 481 |
document_output |
72662 | 482 |
|
72726
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72725
diff
changeset
|
483 |
process_result.output(more_output) |
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72725
diff
changeset
|
484 |
.error(Library.trim_line(stderr.toString)) |
ec6a27bbdab8
proper return code for more errors (amending d892f6d66402);
wenzelm
parents:
72725
diff
changeset
|
485 |
.errors_rc(export_errors ::: document_errors) |
72662 | 486 |
} |
487 |
||
488 |
build_errors match { |
|
489 |
case Exn.Res(build_errs) => |
|
490 |
val errs = build_errs ::: document_errors |
|
74259
6d48d6ba58df
more robust: progress.stopped means that build has failed;
wenzelm
parents:
74258
diff
changeset
|
491 |
if (errs.nonEmpty) { |
72662 | 492 |
result.error_rc.output( |
493 |
errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: |
|
494 |
errs.map(Protocol.Error_Message_Marker.apply)) |
|
495 |
} |
|
74306 | 496 |
else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt) |
74259
6d48d6ba58df
more robust: progress.stopped means that build has failed;
wenzelm
parents:
74258
diff
changeset
|
497 |
else result |
72662 | 498 |
case Exn.Exn(Exn.Interrupt()) => |
74306 | 499 |
if (result.ok) result.copy(rc = Process_Result.RC.interrupt) |
74259
6d48d6ba58df
more robust: progress.stopped means that build has failed;
wenzelm
parents:
74258
diff
changeset
|
500 |
else result |
72662 | 501 |
case Exn.Exn(exn) => throw exn |
502 |
} |
|
503 |
} |
|
504 |
||
73367 | 505 |
def terminate(): Unit = future_result.cancel() |
72662 | 506 |
def is_finished: Boolean = future_result.is_finished |
507 |
||
75393 | 508 |
private val timeout_request: Option[Event_Timer.Request] = { |
73700
908351c8c0b1
check timeout_ignored as in ML, before applying timeout_scale;
wenzelm
parents:
73559
diff
changeset
|
509 |
if (info.timeout_ignored) None |
908351c8c0b1
check timeout_ignored as in ML, before applying timeout_scale;
wenzelm
parents:
73559
diff
changeset
|
510 |
else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) |
72662 | 511 |
} |
512 |
||
75393 | 513 |
def join: (Process_Result, Option[String]) = { |
72662 | 514 |
val result1 = future_result.join |
515 |
||
516 |
val was_timeout = |
|
517 |
timeout_request match { |
|
518 |
case None => false |
|
73367 | 519 |
case Some(request) => !request.cancel() |
72662 | 520 |
} |
521 |
||
522 |
val result2 = |
|
73134
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
73033
diff
changeset
|
523 |
if (result1.ok) result1 |
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
73033
diff
changeset
|
524 |
else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc |
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
73033
diff
changeset
|
525 |
else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt")) |
72662 | 526 |
else result1 |
527 |
||
528 |
val heap_digest = |
|
529 |
if (result2.ok && do_store && store.output_heap(session_name).is_file) |
|
530 |
Some(Sessions.write_heap_digest(store.output_heap(session_name))) |
|
531 |
else None |
|
532 |
||
533 |
(result2, heap_digest) |
|
534 |
} |
|
535 |
} |