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

[Makarius]

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.

I did encounter various problems, shortly before and after that date:

  * lxcisa0, which is a virtual slice of the AFP test machine, could not
finish a plain "isabelle build -b HOL" within finite time. Maybe there was a
lot of disk thrashing on the other slice --- yes, it still has a physical
harddisk. (I ignored the problem and continued the RC3 rollout by other means.)

  * Building the HTML presentation
https://isabelle.sketis.net/website-Isabelle2021-1-RC3/documentation.html
required 6.5h only for the Isabelle distribution, using a relatively weak VM
node under my own control. For RC1 and RC2 this did not work at all for other
reasons. For RC3 it somehow "got stuck" after HOL-Analysis and then proceeded
very slowly, but terminated hours later. My guess is that the Java heap was
getting very full -- too much string and XML material etc. My plan was to
ensure that the JVM for such builds has at least 8-16 GB (but maybe it
requires some other tuning elsewhere).

  * As already for Isabelle2021, HTML presentation on current hardware with
old-fashioned HDD is significantly slower than current  SSD / NVME. In recent
months, I was often wondering, if testing against old iron is actually a good
thing or bad thing, or if the idea of supporting HDDs should be discontinued.


Many newer platforms do assume that your "disk" is not a disk at all, but
random-access persistent memory. Especially macOS: My old MacMini was unusable
with Big Sur until some months ago, when I ordered an obscure adapter for 8
EUR from an obscure manufacture of spare parts in Hong Kong. After 10 weeks of
shipping over the oceans, I could replace the HDD by a regular NVME, and now
this old 2 CPU core + 8 GB machine is great again for testing Isabelle.


So the practical question is: Could the AFP test machine be upgraded to SSD /
NVME?


	Makarius