[isabelle-dev] HOL-Proofs slow
makarius at sketis.net
Mon Oct 22 19:34:53 CEST 2012
On Mon, 22 Oct 2012, Florian Haftmann wrote:
>> I first thought it would be related to 1167c1157a5b (haftmann on
>> src/Pure/Proof/extraction.ML), which is not immediately easy to follow
>> in every detail.
> It indeed isn't, but the effect is idempotent.
> To my defence, reordering arguments is not very comprehensible from a diff.
In such cases, the general question is if making the sources "canonical"
has any purpose. It is rather old material by Stefan Berghofer, written
in the typical style from around 2000, and not going to be revisited in
the foreseeable future. There are no fundamental known problems with it.
So why change it in the first place?
Concerning the digestability of the changeset, it did not turn out as bad
as first anticipated. Bitbucket has pretty good word-wise diffs. So
after spending about 45min with:
I came to the conclusion that the changeset is clean.
More information about the isabelle-dev