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



On Tue, 25 Sep 2012, Rafal Kolanski wrote:

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.

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.

This is getting a bit far off the Isabelle track.

I claimed that Isabelle has sufficiently many ways to identify itself precisely, and reconfigure locations for images and other resources. Building other projects on top should work. People have done that without patching Isabelle.

BTW, when you say "the latest source version" my semantic spell-checker marks it read, because that is not a well-defined notion. The changeset id is how you identify things unambigously, or a collection of ids -- for each repository.


	Makarius





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