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

[Fabian Immler]

> 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:

isabelle/2af1f142f855
afp/5d961e9f8536
---------------------
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:
isabelle/48262e3a2bde
afp/7dde4e79f45a
---------------------
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
https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_JinjaThreads
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).

Fabian


-------------- 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>