[isabelle-dev] HOL-IMP very slow

[Jasmin Christian Blanchette]

Am 12.02.2014 um 16:03 schrieb Makarius <makarius at sketis.net>:

> I see a lot of incoming changes (and many hg queue accidents) just before that,

The "accidents" were that I experimented with "qfold" for the first time. The command merges two patches together. The patches themselves were all as I intended them to be, and the extra pass I applied to reorder and merge the patches was well worth it.

What I didn't notice until it was too late was that after merging, the messages were merged as well (with " * * * " and in a multiline style). I had expected only the description of the parent patch (the one that's merged into) to appear. The one-line format used for displaying descriptions encouraged my misbelief.

To those who use queues and don't know about "hg qpush --move" and "hg qfold" (which didn't exist some years ago): Those are very useful tools, when used correctly.

Jasmin