Re: [isabelle] Algebraic_Numbers



On 04/06/16 02:34, Gerwin Klein wrote:
> 
>>> Stepping back further, the question is why Algebraic_Number_Tests
>>> requires so much persistent heap memory that sessions built on it might
>>> get into problems. Maybe there is a deeper resource problem behind it.
>>
>> That is an excellent question. I still can't quite put my finger on it
>> as to why that single theory forces us to run AFP tests in bulky 64 bit
>> mode.
> 
> Does sound worth investigating, I have no direct ideas either.
> 
> Maybe it is indeed time to officially enable multiple sessions for AFP entries. That will take some infrastructure work, but it would give us more flexibility in treating things like this, for instance with the technique Makarius mentioned, which we used for Jinja years back.

The split into two sessions had mainly the effect to enforce a full heap
compaction (and reload). In contempory Poly/ML this can be done at
runtime, e.g. by putting this into a suitable place (e.g.
Algebraic_Number_Tests.thy):

ML_command %invisible \<open>ML_Heap.share_common_data ()\<close>


Here are some measurements for Isabelle/d8884c111bca + AFP/44c49a721891
on x86-linux with 6 threads.

(0) standard setup:
Finished Algebraic_Numbers (0:04:21 elapsed time, 0:20:03 cpu time,
factor 4.60)

(1) ML_command share_common_data:
Finished Algebraic_Numbers (0:05:23 elapsed time, 0:23:52 cpu time,
factor 4.43)

(2) Algebraic_Numbers based on Algebraic_Number_Lib:
Finished Algebraic_Number_Lib (0:01:18 elapsed time, 0:05:31 cpu time,
factor 4.21)
Finished Algebraic_Numbers (0:04:07 elapsed time, 0:17:55 cpu time,
factor 4.34)

The times for (1) are approximately equal to the sums of times for (2).


Maybe Lars can try share_common_data on the AFP test hardware to see if
it still happens to work on 32bit architecture.


	Makarius





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