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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
