[isabelle-dev] NEWS: Isabelle sessions and build management

[Makarius]

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 
> groups?
>
> 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.


 	Makarius