--- 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)"
+
--- 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
--- 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=""
--- 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 =
--- 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;
--- 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
+ }
}
--- 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
--- 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; \