[isabelle-dev] I don't understand isatest AFP report

[Makarius]

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