[isabelle-dev] AFP: PAPP_Impossibility not terminating
makarius at sketis.net
Tue Apr 18 12:41:15 CEST 2023
On 17/04/2023 23:38, Makarius wrote:
> The first bad revision is:
> changeset: 77808:b43ee37926a9
> user: wenzelm
> date: Mon Apr 10 22:38:18 2023 +0200
> summary: performance tuning: replace Ord_List by Set();
> This is a change of the thm hyps field to make applications like
> PAPP_Impossibility actually faster, but I did not notice that this is such an
> application, and that it becomes very slow.
> Even worse, it is not sufficient to take b43ee37926a9 back, because other
> changes on top appear to cause similar problems.
I have now managed to revert several changes to make PAPP_Impossibility works
again --- nothing pushed yet.
More information about the isabelle-dev