> 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 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
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
