In Isabelle/4d46d53566e6 I've now made the innermost Proof_Context.transfer_syntax more efficient, by switching to a locally linear change discipline of the background theory that makes the merges with the corresponding tables within the proof context much more light-weight.
That was actually motivated by the hope that apart from types and consts, we will manage to do the same with facts, too. It would simplify its global vs. local name space treatment, and make completion of fact names in the Prover IDE work by sudden magic. Coming soon ...
For now there just more efficient consts merges for Local_Theory.define and some concrete datatype timings:
macpro 8fe7414f00b1 $ isabelle build -c -D Datatype_Test Finished Datatype_Test_Old (0:15:03 elapsed time, 0:28:01 cpu time, factor 1.86) Finished Datatype_Test_New (0:06:15 elapsed time, 0:12:14 cpu time, factor 1.95) macpro 8fe7414f00b1 $ isabelle build -c -o quick_and_dirty -D Datatype_Test Finished Datatype_Test_Old (0:11:36 elapsed time, 0:15:19 cpu time, factor 1.32) Finished Datatype_Test_New (0:04:27 elapsed time, 0:05:07 cpu time, factor 1.14) macpro ad6bd8030d88 $ isabelle build -c -D Datatype_Test Finished Datatype_Test_Old (0:14:31 elapsed time, 0:27:18 cpu time, factor 1.88) Finished Datatype_Test_New (0:05:11 elapsed time, 0:10:47 cpu time, factor 2.08) macpro ad6bd8030d88 $ isabelle build -c -o quick_and_dirty -D Datatype_Test Finished Datatype_Test_Old (0:11:14 elapsed time, 0:15:09 cpu time, factor 1.34) Finished Datatype_Test_New (0:03:21 elapsed time, 0:03:52 cpu time, factor 1.15)This is an old 8 core machines, using 4 worker threads and Poly/ML SVN 1915 on x86-darwin. The test session is included -- its seems to stem from some private discussion among the BNF guys and the IsaFoR guys.
The first observation is that datatype_new is actually faster! Are there further observations from early adopters of what is actually a quite advanced definitional tool suite awaiting the release this summer.
Makarius
Datatype_Test.tar.gz
Description: Binary data
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev