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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
