On 15.05.2013, at 11:33 PM, Makarius <[email protected]> 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.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to