Re: [isabelle] Algebraic_Numbers



On 02/06/16 22:37, Gerwin Klein wrote:
> For comparison, weâre doing this already: since we canât merge multiple parent sessions, all entries that re-use more than one other entry will currently definitely rebuild all of at least one parent anyway. Given that, and the effort Iâm spending periodically to make sure the AFP does not rebuild HOL-Library 100 times each day, I donât think the light part of one entry being rebuilt is a problem.

BTW, for years I am trying to get to a situation where sessions and heap
images are independent (also for document preparation). That would allow
to run many AFP sessions within the same Poly/ML process, providing a
chance that the big number of small sessions uses much less resources.


	Makarius





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