[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Makarius]

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 
> https://isabelle.sketis.net/devel/build_status/AFP/PAPP_Impossibility.csv
> 
> Stay tuned ...

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 need to look more closely into the special SAT prover in PAPP_Impossibility, 
to see what is really going on.


	Makarius