Re: [isabelle] Parallel proofs issue, potentially in subst method



On Mon, 10 Sep 2012, Rafal Kolanski wrote:

I have recently come across an issue when trying to improve the runtimes of our regression test server. When I ran it with -q 1, the times improved drastically, which was nice. When I ran it with -q 2 though, it didn't build at all.

Now the world knows that the top-secret proofs of L4.verified are still checked sequentially :-)


The error should be on the line attempting the subst:
*** exception THM 0 raised (line 758 of "thm.ML"):
*** forall_intr: variable "bs" free in assumptions
*** [| length bs = sz; P (Suc p) sz bs; p # Z = Z |]
*** ==> p # load_list_basic sz (Suc p) = Z
***   [!!]
*** At command "apply" (line 30 of "/home/rafalk/t/isa_bug/Loading.thy")

The issue is definitely due to some shadowing/renaming of the variable bs, but what else is going on is well beyond my current grasp of comprehension.

I've had a quick look at the "subst" method, but it looks very bad. That code has not been maintained in many years. It simply ignores the all-important Proof.context when inventing free variables that are expected to be fresh, but aren't. There is not just one place, but many. One could probably make a small changeset to get your example working, but it will then crash in another situation.

The following comment in isand.ML, which is one part of the problem here is quite representative:

  THINK: are we really ok with our varify name w.r.t the prop - do
  we also need to avoid names in the hidden hyps? What about
  unification contraints in flex-flex pairs - might they also have
  extra free vars?

The answer: hyps are necessary, but still not sufficient. One needs to take the full Proof.context into account.


A quick fix is to do the renaming yourself in the proof, i.e. avoid accidental overlap of blue / brown / green variables with the same name on the surface. Then "subst" can continue its work with its archaic context model a little longer.


	Makarius





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