[isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

Fabian Immler immler at in.tum.de
Tue May 15 14:31:54 CEST 2018

> Am 14.05.2018 um 13:24 schrieb Fabian Immler <immler at 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 afp/5d961e9f8536.
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).


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5026 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180515/61f82bdd/attachment.bin>

More information about the isabelle-dev mailing list