Hello Isabelle developers.
I was recently reminded of one of the things on my wish-list for Isabelle: a
"make -k" mode in which the system continues for as long as possible and
reports as many errors as possible, rather than halting after the first one. I
think this would be generally useful to Isabelle users, but it would be
especially useful when fiddling with tactics that are already in use. The usual
approach is to try several variations aiming to minimise incompatibility, but
there's no easy way to get an idea of the level of incompatibility without
repairing the first few errors.
To clarify, I'd like to be able to type something like "isabelle testmake
(arguments)", and the system would run through the same sources as on an
"isabelle make", only errors in proof scripts would be suppressed. Once
everything is loaded and any image to be saved is saved, the system would print
all the errors encountered at the end of the log.
It occurred to me how to implement this feature using the existing parallel
apparatus. What's needed is a way to defer an exception raised in computing a
future object forever, leaving the exception in the future and allowing all
other independent work to conclude. Since parallel proofs are executed in
future calculations that never need to be joined (unless someone is inspecting
proof terms), this could provide a solution. I had a go at doing this myself
but got nowhere. Does anyone familiar with the concurrency code think this is
possible?
While I'm putting things on the concurrency wish-list, I have one more: a limit
on the length of the work queue. The reason I request this is that some of our
large sessions (1-2 hrs) seem to perform poorly with parallelism, and I suspect
part of the problem is that the problem parsing thread is getting so far ahead
of the problem-solving threads that the majority of the contexts and problems
from the session are living in memory waiting to be solved. I think the way you
would implement this is by switching mode once the work queue is large enough
and dropping any threads attempting further forks to the bottom of the priority
list. Does anybody else think this might be a good idea? I guess I should try
to conjure up an example session which demonstrates the performance problems.
As always, please tell me if I'm completely wrong about the way the system
works.
Yours,
Thomas.
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
