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

On 25/09/12 06:12, Makarius wrote:
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.

You are entirely missing my point here. You keep referring to Isabelle versions as if they are the only versions anyone might care about. We run a project *using* Isabelle. The project has its own revision control versions, and Isabelle is just one subrepo.

What you are describing is the isabelle version used to build a particular image. We know which version this is. What we don't know is which repository version of the *project* built the image we are presenting to the user.

Trivially: on port 8193 we have the wwwfind server presenting an interface to users wishing to search through the latest CREFINE image the regression test server was able to build with the current version of Isabelle. Question: given that you know which Isabelle version and PolyML version built it (obvious from the image path and from Isabelle being a subrepo), which repository version are you looking at? Sometimes an image can be broken for a few days, and people need to tell they are not looking at the latest source version, but at the latest successfully built version.

I really can't get the point across any more clearly. I have repeatedly tried to explain that Isabelle is a tool upon which we run a project, and it is not the only project in existence. It should be evident that simply knowing the revision of Isabelle used to build something is not the only revision one should know, as Isabelle was used to build *something* and the version of that *something* is in fact more important, henceforth "isabelle version -i" really does nothing here.


Rafal Kolanski.

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