[isabelle-dev] [Afp-submit] AFP build times out in file/theory presentation

Makarius makarius at sketis.net
Tue Nov 16 22:08:42 CET 2021


On 16/11/2021 13:01, Makarius wrote:
> On 16/11/2021 09:35, Fabian Huch wrote:
>> There seems to be a performance degradation in the presentation somewhere
>> between Isabelle/adb10e840b71 and Isabelle/2b212c8138a. I notified Makarius
>> about that but didn't spot the error yet (there were lots of changes in the
>> signature).
> 
> That interval is shortly before Isabelle2021-RC3 (12-Nov-2021). From the
> changesets, nothing special has happened: I will investigate more closely later.

This particular new problem was introduced here:
https://isabelle.sketis.net/repos/isabelle-release/rev/32c2587cda4f#l2.7

In that version, the HTML.Context has mutable content (originally from the
version by Fabian, that I shuffled around a lot without eliminating it yet).
For the moment, I have done it slightly differently here:
https://isabelle.sketis.net/repos/isabelle-release/rev/507f50dbeb79

Moreover, this change will save a lot of Java heap:
https://isabelle.sketis.net/repos/isabelle-release/rev/5eac4b13d1f1

Thus we should be back to a half-decent situation.


I will investigate further fine points, to see if remaining conceptual can be
resolved, notably a mismatch of sessions_structure.build_topological_order vs.
sessions_structure.imports_topological_order that is only relevant for
presentation.


	Makarius


More information about the isabelle-dev mailing list