On Wed, 15 May 2013, Gerwin Klein wrote:
We're probably better off if I make the AFP test more aware of global
JVM crashes and better at interpreting regular output. It's good to try
to reduce JVM problems, but the JVM being what it is, they will still
happen from time to time.
The JVM was never pretty, which we knew already in 1995, and it did not
change substantially in almost 20 years. Nonetheless, it can be turned
into some use, although the plumbing of wood onto lead (i.e. shell scripts
invoking JVM) is more slow and fragile than necessary.
One could use Scala "scripts" directly (despite some oddities that the
EPFL guys have in the startup phase of the "scala" command interpreter
concerning classpaths).
Isabelle/Build is primarily isabelle.Build.build() within Isabelle/Scala.
For historic reasons it is presented as command-line tool with a single
byte as return code, and some plain text output on stdout/stderr. Its
main internal result has more precise information for each session, but it
is reduced like this in the very end (see
http://isabelle.in.tum.de/repos/isabelle/annotate/7b8ce8403340/src/Pure/Tools/build.scala#l887):
/* return code */
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
val unfinished =
(for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
.sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1
progress.echo("Unfinished session(s): " + commas(unfinished))
}
rc
In this instance, there was some kind of JVM problem which then caused the scan
on the AFP test side to miss the Container session entirely and the tool
therefore concluded that it must have been removed.
Basically the Isabelle build executable should follow the usual conventions of
return codes:
0: all fine
1: program error, e.g. some sessions failed / remains outdated
2: systemic failure, e.g. some unexpected exception within the JVM
I should definitely react better to case 2.
2 should mean anything >= 2.
As can be seen above, the rc is the maximum of any of the sessions (but
they normally fail only via 1).
There is another wrapper in isabelle.Command_Line.tool() that gives a
plain 2 for arbitrary Throwable produced by the tool body. If that
handler breaks down due to total JVM failure, you probably get some >=2
code from the shell that was trying to run it in the first place.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
