Re: [isabelle] Algebraic_Numbers



On 02/06/16 22:37, Gerwin Klein wrote:
> I thought the point was that the part that is duplicated is *not* bulky. If it is, we should think more, but I donât have any better solutions ready.

I think the worries of Lars Hupel are based on the rather weak
Isabelle/Jenkins testing hardware. My own worries are based on general
observations that Algebraic_Numbers could be close to the infamous
"invisible concrete wall" (without detailed measurements yet).

Here are some numbers on the fastest test machine that I have access to
(i.e. my own workstation):

Isabelle/bcf4828bb125 + AFP/83c0fef83e3f
x86-linux, 6 threads

Finished Algebraic_Number_Lib (0:00:48 elapsed time, 0:04:12 cpu time,
factor 5.22)  ## without heap image
Finished Algebraic_Numbers (0:04:48 elapsed time, 0:22:56 cpu time,
factor 4.78)  ## based on Pre_Algebraic_Numbers


Now the same, but Algebraic_Numbers is based on Algebraic_Number_Lib,
i.e. the first session builds a heap and the second only runs the bulky
tests:

Finished Algebraic_Number_Lib (0:01:17 elapsed time, 0:05:28 cpu time,
factor 4.23)
Finished Algebraic_Numbers (0:03:54 elapsed time, 0:17:54 cpu time,
factor 4.57)


This makes some difference in overall CPU time usage.  It is reminiscent
of ancient times, when Jinja (not JinjaThreads) had to be split into two
sessions: the full compactification of the first heap makes the second
one more comfortable. Although the effect today is not that important,
due to online heap sharing.

There are already AFP entries with more than one session, and also
add-on documents. Maybe that is already sufficient to publish the tests
separately, or maybe not. Lars Hupel might be able to say that.


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.


	Makarius





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