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

[Gerwin Klein]

On 15.05.2013, at 11:33 PM, Makarius <makarius at sketis.net> wrote:

> 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.

Yes, that's basically why this approach worked back then and I haven't really renovated it for the new setting.


> Do the AFP test scripts have additional resource limits?

It currently doesn't. We could think of wrapping a global "ulimit" around the test invocation.

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.


>> 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. Currently this gives just a completely confusing "everything removed" report.

I'll have a look at that over the weekend.

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.