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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
