[isabelle-dev] I don't understand isatest AFP report
makarius at sketis.net
Wed May 15 15:33:52 CEST 2013
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:
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.)
More information about the isabelle-dev