[isabelle-dev] AFP: PAPP_Impossibility not terminating
makarius at sketis.net
Mon Apr 17 23:38:53 CEST 2023
On 17/04/2023 14:49, Makarius wrote:
> We have a problem with PAPP_Impossibility for quite some time.
> I am presently running a bisection to see better where it actually happens:
> presently the interval is Isabelle/f5aca3ed1adb .. 69ee23f83884 based on
> Stay tuned ...
The first bad revision is:
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 need to look more closely into the special SAT prover in PAPP_Impossibility,
to see what is really going on.
More information about the isabelle-dev