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

[Makarius]

On Wed, 15 May 2013, Gerwin Klein wrote:

> What's going on is that the somewhat primitive AFP test doesn't 
> understand the output of "isabelle build" correctly.
>
> It's currently getting its list of sessions by scanning through the 
> output, trying to find messages for failed or successful sessions. This 
> worked reliably for IsaMakefiles, because there was a separate 
> invocation for each session and there was delimiting output before/after 
> each session.

The difference here is that "make" did not crash in its own right, but in 
exchange had less control over what was run and how it failed.

Doing the management of Isabelle build by a single JVM process gives the 
usual advantages and disadvantages of explicit management: potentially 
more control (e.g. for better scheduling) and more ways of breakdown.

After the bombing of the JVM by tons of tracing messages, I've briefly 
reconsidered the old file-system based approach, but that might then lead 
to bombing of some file-server, which is even worse.

Instead there are now more tight timeouts (AFP/fb808eb615) and a global 
process_output_limit of 100MB -- the JVM can still crash trying to decode 
the resulting log file again (UTF-16 sucks).

Do the AFP test scripts have additional resource limits?


> 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

Apart from that the stdout/stderr have a certain meaning, somewhat 
depending on the return code.


Also note that current Isabelle/ea123790121b allows do give more resources 
to the JVM that is running Isabelle build.  E.g. like this:

   ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss2m"

The default is a bit more frugal, to improve chances that it works on 
small machines that users might have.  (The JVM is very inflexible 
concerning resource management; it tends to misbehave for small heap size, 
but fails to start up for too big heaps.)


 	Makarius