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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and