Re: [isabelle] Algebraic_Numbers

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

That is a good idea, I donât think we need to keep all artefacts.

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

Good, these are worth keeping, at least for a moderately longer time span. They enable statistics etc.

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

Extra sessions and documents should be very rare, i.e. almost all AFP sessions should have exactly one document, which is the one that is linked.

Is this not the case or am I misunderstanding the question?

>> 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 information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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