# HG changeset patch # User wenzelm # Date 1344004058 -7200 # Node ID 49c080255a57ca675c44cd0fa988bc7d1f73628d # Parent 40a87b4dac19bd6ae016d9f4f6696ed21d3f5c63# Parent b171bcd5dd86579a000354ae3544daf371ad61bf merged diff -r 40a87b4dac19 -r 49c080255a57 etc/options --- a/etc/options Fri Aug 03 15:38:44 2012 +0200 +++ b/etc/options Fri Aug 03 16:27:38 2012 +0200 @@ -63,3 +63,6 @@ declare timing : bool = false -- "global timing of toplevel command execution and theory processing" +declare timeout : real = 0 + -- "timeout for session build job (seconds > 0)" + diff -r 40a87b4dac19 -r 49c080255a57 lib/scripts/run-polyml --- a/lib/scripts/run-polyml Fri Aug 03 15:38:44 2012 +0200 +++ b/lib/scripts/run-polyml Fri Aug 03 16:27:38 2012 +0200 @@ -46,10 +46,10 @@ if [ -z "$INFILE" ]; then INIT="" - EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" + EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" else check_file "$INFILE" - INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.failure));" + INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));" EXIT="" fi diff -r 40a87b4dac19 -r 49c080255a57 lib/scripts/run-smlnj --- a/lib/scripts/run-smlnj Fri Aug 03 15:38:44 2012 +0200 +++ b/lib/scripts/run-smlnj Fri Aug 03 16:27:38 2012 +0200 @@ -52,7 +52,7 @@ ## prepare databases if [ -z "$INFILE" ]; then - EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" + EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" DB="" else EXIT="" diff -r 40a87b4dac19 -r 49c080255a57 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Fri Aug 03 15:38:44 2012 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Fri Aug 03 16:27:38 2012 +0200 @@ -45,6 +45,12 @@ lexicon: Scan.Lexicon = Scan.Lexicon.empty, val completion: Completion = Completion.empty) { + override def toString: String = + (for ((name, kind) <- keywords) yield { + if (kind == Keyword.MINOR) quote(name) + else quote(name) + " :: " + quote(kind) + }).toList.sorted.mkString("Outer_Syntax(keywords ", " and ", ")") + def keyword_kind(name: String): Option[String] = keywords.get(name) def + (name: String, kind: String, replace: String): Outer_Syntax = diff -r 40a87b4dac19 -r 49c080255a57 src/Pure/System/build.ML --- a/src/Pure/System/build.ML Fri Aug 03 15:38:44 2012 +0200 +++ b/src/Pure/System/build.ML Fri Aug 03 16:27:38 2012 +0200 @@ -79,7 +79,9 @@ val _ = Session.finish (); val _ = if do_output then () else quit (); in () end - handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); + handle exn => + (Output.error_msg (ML_Compiler.exn_message exn); + if Exn.is_interrupt exn then exit 130 else exit 1); end; diff -r 40a87b4dac19 -r 49c080255a57 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Fri Aug 03 15:38:44 2012 +0200 +++ b/src/Pure/System/build.scala Fri Aug 03 16:27:38 2012 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.util.{Timer, TimerTask} import java.io.{BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, IOException} import java.util.zip.GZIPInputStream @@ -264,21 +265,28 @@ sealed case class Node( loaded_theories: Set[String], + syntax: Outer_Syntax, sources: List[(Path, SHA1.Digest)]) sealed case class Deps(deps: Map[String, Node]) { def is_empty: Boolean = deps.isEmpty + def apply(name: String): Node = deps(name) def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2) } def dependencies(verbose: Boolean, queue: Session.Queue): Deps = Deps((Map.empty[String, Node] /: queue.topological_order)( { case (deps, (name, info)) => - val preloaded = + val (preloaded, parent_syntax) = info.parent match { - case None => Set.empty[String] - case Some(parent) => deps(parent).loaded_theories + case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax) + case None => + (Set.empty[String], + Outer_Syntax.init() + + // FIXME avoid hardwired stuff!? + ("hence", Keyword.PRF_ASM_GOAL, "then have") + + ("thus", Keyword.PRF_ASM_GOAL, "then show")) } val thy_info = new Thy_Info(new Thy_Load(preloaded)) @@ -296,6 +304,9 @@ val loaded_theories = preloaded ++ thy_deps.map(_._1.theory) + val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten + val syntax = (parent_syntax /: keywords)(_ + _) + val all_files = thy_deps.map({ case (n, h) => val thy = Path.explode(n.node).expand @@ -314,14 +325,14 @@ error(msg + "\nThe error(s) above occurred in session " + quote(name)) } - deps + (name -> Node(loaded_theories, sources)) + deps + (name -> Node(loaded_theories, syntax, sources)) })) /* jobs */ private class Job(dir: Path, env: Map[String, String], script: String, args: String, - val parent_heap: String, output: Path, do_output: Boolean) + val parent_heap: String, output: Path, do_output: Boolean, time: Time) { private val args_file = File.tmp_file("args") private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) @@ -332,7 +343,29 @@ def terminate: Unit = thread.interrupt def is_finished: Boolean = result.is_finished - def join: (String, String, Int) = { val res = result.join; args_file.delete; res } + + @volatile private var timeout = false + private val timer: Option[Timer] = + if (time.seconds > 0.0) { + val t = new Timer("build", true) + t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms) + Some(t) + } + else None + + def join: (String, String, Int) = { + val (out, err, rc) = result.join + args_file.delete + timer.map(_.cancel()) + + val err1 = + if (rc == 130) + (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") + + (if (timeout) "*** Timeout\n" else "*** Interrupt\n") + else err + (out, err1, rc) + } + def output_path: Option[Path] = if (do_output) Some(output) else None } @@ -392,7 +425,8 @@ (do_output, (options, (verbose, (browser_info, (parent, (name, info.theories))))))) } - new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap, output, do_output) + new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap, + output, do_output, Time.seconds(options.real("timeout"))) } @@ -515,10 +549,12 @@ File.write(output_dir + log(name), out) echo(name + " FAILED") - echo("(see also " + (output_dir + log(name)).file.toString + ")") - val lines = split_lines(out) - val tail = lines.drop(lines.length - 20 max 0) - echo("\n" + cat_lines(tail)) + if (rc != 130) { + echo("(see also " + (output_dir + log(name)).file.toString + ")") + val lines = split_lines(out) + val tail = lines.drop(lines.length - 20 max 0) + echo("\n" + cat_lines(tail)) + } no_heap } @@ -611,5 +647,15 @@ } } } + + + /* static outer syntax */ + + // FIXME Symbol.decode!? + def outer_syntax(session: String): Outer_Syntax = + { + val (_, queue) = find_sessions(Options.init(), Nil).required(false, Nil, List(session)) + dependencies(false, queue)(session).syntax + } } diff -r 40a87b4dac19 -r 49c080255a57 src/Pure/build --- a/src/Pure/build Fri Aug 03 15:38:44 2012 +0200 +++ b/src/Pure/build Fri Aug 03 16:27:38 2012 +0200 @@ -61,11 +61,11 @@ if [ "$TARGET" = RAW ]; then if [ -z "$OUTPUT" ]; then "$ISABELLE_PROCESS" \ - -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ + -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ -q RAW_ML_SYSTEM else "$ISABELLE_PROCESS" \ - -e "use\"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ + -e "use\"$COMPAT\" handle _ => Posix.Process.exit 0w1;" \ -e "structure Isar = struct fun main () = () end;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -q -w RAW_ML_SYSTEM "$OUTPUT" @@ -73,11 +73,11 @@ else if [ -z "$OUTPUT" ]; then "$ISABELLE_PROCESS" \ - -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ -q RAW_ML_SYSTEM else "$ISABELLE_PROCESS" \ - -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => Posix.Process.exit 0w1;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -f -q -w RAW_ML_SYSTEM "$OUTPUT" fi diff -r 40a87b4dac19 -r 49c080255a57 src/Tools/Code/lib/Tools/codegen --- a/src/Tools/Code/lib/Tools/codegen Fri Aug 03 15:38:44 2012 +0200 +++ b/src/Tools/Code/lib/Tools/codegen Fri Aug 03 16:27:38 2012 +0200 @@ -52,7 +52,7 @@ FORMAL_CMD="Toplevel.program (fn () => (use_thy thyname; ML_Context.eval_text_in \ (SOME (Proof_Context.init_global (Thy_Info.get_theory thyname))) false Position.none ml_cmd)) \ - handle _ => OS.Process.exit OS.Process.failure;" + handle _ => Posix.Process.exit 0w1;" ACTUAL_CMD="val thyname = \"$THYNAME\"; \ val _ = quick_and_dirty := $QUICK_AND_DIRTY; \