[isabelle-dev] Performance of datatype_new

[Makarius]

This is a public continuation of a sporadic private discussion over the 
past few months.  Dmitriy had occasionally shown me small and big datatype 
examples, and recalled some old questions about the performance of 
Local_Theory.define in common local theory targets.

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Datatype_Test.tar.gz
Type: application/octet-stream
Size: 3745 bytes
Desc: 
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140312/5253df30/attachment.obj>