[isabelle-dev] Feature request

[Thomas Sewell]

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.