[isabelle] Algebraic_Numbers



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.

Any opinions?


Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.