[isabelle-dev] NEWS: Isabelle sessions and build management
makarius at sketis.net
Thu Aug 2 19:56:50 CEST 2012
On Thu, 2 Aug 2012, Gerwin Klein wrote:
> The etc/sessions file should make that possible, although I'm not
> opposed to Florian's proposal of fusing the two concepts into one file:
> if ROOT supported a syntax construct that lists directories as in the
> session file, we could have a thys/ROOT with the sub-session list and a
> largely independent ROOT for each entry.
I have discontinued etc/sessions already, see Isabelle/47330b712f8f.
> One open issue is time-outs. The AFP IsaMakefiles all have individual
> timeouts (via ulimit) for each session so that one non-terminating proof
> in over 100 entries does not kill the entire test each time. Can we
> include this in build?I'm not sure how well ulimit works on Cygwin.
Ulimit is indeed non-portable. Historically we also had problems with it,
because it limits CPU time, not elapsed time: the system can "hang"
without consuming CPU cycles.
I've first tried to use Isabelle/ML timeouts, but it is not exactly right
(and does not work with traditionally uninterruptible use_thys). I have
already a different idea how to do it in Isabelle/Scala, to make a robust
and portable real time limit for each prover process.
>> Note that the configuration of AFP as Isabelle component does *not*
>> include this large session name space by default.
> Is there a significant slow-down or is it just name space pollution?
Mainly name space pollution for the human maintainer of Isabelle and/or
AFP, sometimes both sometimes only one of the two.
> If it is the latter, can we fix it by making better use of session
> If possible, I'd like to try and avoid special treatment of APF as far
> as possible and rather make sure the underlying system scales naturally
> to many sessions.
This would mean to make the groups work like a "tag cloud". So far we
managed without that, but it might have come at some stage.
More information about the isabelle-dev