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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
