[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Makarius]

On 18/04/2023 12:41, Makarius wrote:
> 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.

To conclude this divergence, the situation in Isabelle/dd222e2af01a + 
AFP/fcf84c1dcf9b is now as follows:

   * All my inference kernel changes concerning the improved Table() and Set() 
functors have been reverted: they help for large persistent data, but not for 
data that changes dynamically a lot (e.g. the hyps in inferences, where merge 
is critical).

   * There are some minor changes to 
AFP/thys/PAPP_Impossibility/papp_impossibility.ML to make it faster than 
before: this includes the version that you had sent me privately + plus some 
tuning. The key changes are:

changeset:   13550:317d450e66bc
user:        wenzelm
date:        Tue Apr 18 20:45:33 2023 +0200
files:       thys/PAPP_Impossibility/papp_impossibility.ML
description:
alternative version by Manuel Eberl, following the approach of 
Isabelle2022/src/HOL/Tools/sat.ML with one big hyp;

changeset:   13552:351b7b576892
user:        wenzelm
date:        Tue Apr 18 20:58:25 2023 +0200
files:       thys/PAPP_Impossibility/papp_impossibility.ML
description:
eliminated pointless parallelism: approx. 1.3s as plain sequential ML;


Here are some timings:

* before Isabelle/b43ee37926a9 + AFP/c9540530e3db:

Finished PAPP_Impossibility (0:03:23 elapsed time, 0:04:51 cpu time, factor 1.43)

* current Isabelle/dd222e2af01a + AFP/fcf84c1dcf9b:
Finished PAPP_Impossibility (0:00:57 elapsed time, 0:02:18 cpu time, factor 2.40)


Not bad for something that appeared like a huge monster proof.


	Makarius