> Am 14.05.2018 um 13:24 schrieb Fabian Immler <imm...@in.tum.de>:
> I did notice that those changes caused issues with timeouts in some AFP 
> sessions, and simply "fixed" those on the spot (e.g., the ones in afp/85324e3 
> and afp/2ff575e hinted at problems caused by incorporating syntax for FuncSet 
> into Complex_Main).
> This was just to keep everything going, but I was well aware that I needed to 
> take a closer look at the problems caused there and resolve them properly 
> (e.g., not exposing FuncSet-syntax in Complex_Main).
I did move FuncSet back to HOL-Library in isabelle/2af1f142f855 and 
It seems like this improved the performance a lot:

Finished JinjaThreads (0:35:12 elapsed time, 2:28:07 cpu time, factor 4.21)
0:35:24 elapsed time, 2:28:07 cpu time, factor 4.18

Before it was:
Finished JinjaThreads (0:54:35 elapsed time, 3:32:25 cpu time, factor 3.89)
0:58:01 elapsed time, 3:43:03 cpu time, factor 3.84

We will have to wait for the results on
to see whether this is actually back to normal or whether there are more 
performance problems.

In JinjaThreads/Common/ExternalCall.thy one can see that e.g., in definition 
red_external_aggr, the funcset syntax → causes
"Ambiguous input⌂ produces 32768 parse trees" and therefore takes 6 minutes 
(instead of 1 second).


Attachment: smime.p7s
Description: S/MIME cryptographic signature

isabelle-dev mailing list

Reply via email to