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

Makarius makarius at sketis.net
Fri May 17 17:38:57 CEST 2013

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.


More information about the isabelle-dev mailing list