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

[Makarius]

On Thu, 16 May 2013, Makarius wrote:

>    /* return code */
>
>    val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
>
>>>> 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.
>
> 2 should mean anything >= 2.

Yet another refinement: processes that are terminated by POSIX signal 
produce rc = 128 + signal_nr.  So an interrupted prover process gives 130, 
and thus distorts the above "max" arithmetic of return codes.

I shall probably turn an interrupt stemming from Isabelle/Scala timeout 
into regular error 1 of the process being addressed, analogously to what 
Isabelle/ML does to turn phyisical (meaningless) Exn.Interrupt into 
TimeLimit.TimeOut in certain situations.


Apart from that, the a more explicit isabelle.Build.Result data structure 
(or a variant of it) would make applications like heavy-duty AFP test more 
clear, without guessing at bit patterns within a byte.


 	Makarius