The Algebraic_Numbers theory is notoriously big and resource-intensive.
I have a development that imports Algebraic_Numbers and then adds some
small things on top of it and exports code. Oddly, this then causes
stack overflows unless I switch to 64 bit Isabelle.
I noticed that a huge chunk of the resource hunger of that development
actually comes from Algebraic_Number_Tests.thy, which one does not even
need in order to use the development.
I therefore propose removing this theory from the Algebraic_Numbers
session and introducing a separate Algebraic_Number_Tests session for
it. I tried this locally and this is theh difference that it made:
Before: Finished Algebraic_Numbers (0:04:33 elapsed time, 0:15:05 cpu
time, factor 3.31)
After: Finished Algebraic_Numbers (0:01:18 elapsed time, 0:04:05 cpu
time, factor 3.12)
Now, I don't know if and by how much this reduces the memory
requirements and I have no idea how to measure this reliably. In any
case, I do not see any drawbacks of doing this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and