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

On 13/09/12 04:16, Makarius wrote:
> 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 :-)

We generally try to run with the highest amount of parallelism that does
not make the machine thrash or PolyML segfault. Previously that was -q
0, now it's -q 1. We're tracking the svn version of the upcoming PolyML
5.5 to see if at some point we can switch to -q 2.

>> 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.

I made a bad joke about how I should title my post to the list "On the
improper use of context in the subst method", but then we weren't sure
if that was exactly the case. Context is really hard to get right, and
old code does accumulate these leaks.

> 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.

Yes, we ended up doing that, and now we're back to PolyML segfaulting
with -q 2. David seems to be applying quite a few fixes to the GC
though, so we have high hopes of getting it working soon.

I would also like to say thank you in general for the movement towards
local context and parallelism over the years. We went down from a full
test run of almost 8 hours down to 4 when switching to -q 1.

Thanks for patching it in the repository. Hopefully it will save someone
a major head-scratching in future!


Rafal Kolanski

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