Re: [isabelle] Algebraic_Numbers



> 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).

Better hardware is on its way.

> 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.

Presently, all documents for the development version are built, but not
published. The reason for that is that it turns out the disk space
requirements to retain all HTML and PDF files is excessive (dozens of GB
amassed during two or three weeks). I have a changeset to the build
server in my pipeline which will retain the latest set of documents.

(NB, build logs are retained and will be retained forever; they are
relatively small due to compression.)

The remaining question is how these documents will be presented in AFP.
Currently only the documents of the main sessions are linked from the
entry pages.

> 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.

Cheers
Lars




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