Email Gateway (Nov 16 2021 at 08:02): Email Gateway (Nov 16 2021 at 08:02):From: Tobias Nipkow <nipkow@in.tum.de>
Oops, hadn't noticed that. The hard timing facts: The presentation part, which
used to take 35-40 mins is now taking 90 minutes at least, and we don't have an
upper bound (because of the timeout). Of course we could try to increase the
timeout and see what happens. The problem is largely due to the fact that theory
presentation used to be incremental (quite some time ago) but these days, even
if only 1 AFP entry has changed, the presentation for the entire AFP is built.
Tobias
smime.p7s
Email Gateway (Nov 16 2021 at 08:06):From: Gerwin Klein <kleing@unsw.edu.au>
I'm not sure it's that, although it might be related. The log looks like the presentation part went on for almost the full 4h, which sure isn't how long it is supposed to take.
Cheers,
Gerwin
signature.asc
Email Gateway (Nov 16 2021 at 08:17):From: Tobias Nipkow <nipkow@in.tum.de>
We are both right: in the log I looked at, the proofs only left 90 minutes for
the presentation until timeout (hence no upper bound), but as you point out, if
the proofs are shorter, the presentation part will happily use the rest of the 4
hours.
Tobias
smime.p7s
Email Gateway (Nov 16 2021 at 08:35):From: Fabian Huch <huch@in.tum.de>
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).
I think the jenkins build should be configured to send out notification
emails in situations like that. Either by marking builds that time out
as "failed" rather than "aborted" (which I'm in favour of) or by
explicitly sending out emails on aborted builds (though it seems like it
would send an email at every aborted built, not just the first one).
Fabian
Email Gateway (Nov 16 2021 at 08:50):From: Gerwin Klein <kleing@unsw.edu.au>
Right, that explains the 90 min vs 4h, and it looks like Fabian has already identified a range of change sets that might be the cause.
So apart from the fork, nothing specific needs to happen on the AFP side at the moment.
Cheers,
Gerwin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 08:53):From: Gerwin Klein <kleing@unsw.edu.au>
+1 to that a timed-out build should be a failed build.
Cheers,
Gerwin
Email Gateway (Nov 16 2021 at 12:01):From: Makarius <makarius@sketis.net>
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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 18:30):From: Tobias Nipkow <nipkow@in.tum.de>
I'll check if that can be done right away and then we can see.
What I never understood is why incremental generation of presentations is no
longer possible.
Tobias
smime.p7s
Email Gateway (Nov 16 2021 at 20:08):From: Makarius <makarius@sketis.net>
The situation is getting more and more complex.
Nonetheless, there is a plain and simple mistake somewhere in
Isabelle2021-RC3: afterwards it will be more incremental, but not maximally
incremental.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 21:08):From: Makarius <makarius@sketis.net>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 16 2021 at 23:41):From: Makarius <makarius@sketis.net>
Half-decent in that version means 2h for presentation.
(I will make one more round to see if the session dependency situation can be
further clarified. This will allow better persistance of results, e.g. for
incremental presentation.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 17 2021 at 06:23):From: Tobias Nipkow <nipkow@in.tum.de>
On 17/11/2021 00:41, Makarius wrote:
On 16/11/2021 22:08, Makarius wrote:
Moreover, this change will save a lot of Java heap:
https://isabelle.sketis.net/repos/isabelle-release/rev/5eac4b13d1f1Thus we should be back to a half-decent situation.
Half-decent in that version means 2h for presentation.
For the AFP test hardware we seem to be back more or less to where we were, i.e.
about 40 mins for presentation.
Thanks a lot for that!!
Tobias
(I will make one more round to see if the session dependency situation can be
further clarified. This will allow better persistance of results, e.g. for
incremental presentation.)Makarius
Afp-submit mailing list
Afp-submit@mailman46.in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/afp-submit
Last updated: Dec 21 2024 at 16:20 UTC