Re: [isabelle] Parallel proofs issue, potentially in subst method (also, backtraces)



On Mon, 17 Sep 2012, Rafal Kolanski wrote:

There are real issues with introspection of proofs in larger projects, e.g. being able to reliably tag images (you are looking at the most recent successful build of an image via the wwwfind interface... quick, please tell me which revision that is, and if the correct image is in fact loaded without reading through the entire theory dropdown first). I have also tried discussing this at length, but no one cares except for our team, so we use custom patches and I gave up. The next big project will have the exact same problems, and these hacky solutions will get hacked in again and again, wasting people's time, while every time we bring them up here we'll get told they are not relevant, because the Isabelle project itself doesn't need it, and why would you want multiple instances of an image on the same machine anyway?

This thread is already getting old, but the above paragraph sounds very odd to me. Myself and several other people I know use routinely a lot of different Isabelle versions and work with images from them. You have the regular settings that can be modified locally, and tools like "isabelle version -i" to get more specific identification of repository snapshots. This should give sufficient flexibility to organize images in many ways. In the next release that will be perfected even further, thanks to the new build system.

I don't think any of your local "hacks" are actually needed. IIRC, this was also what I hinted at when the discussion was coming up some years ago, but it was not taken to the end, just cancelled in frustration probably.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.