Email Gateway (Jul 31 2020 at 15:27): Email Gateway (Jul 31 2020 at 15:27):From: Lawrence Paulson <lp15@cam.ac.uk>
I had a run going (the change involved adding a single lemma and shouldn’t have affected anything) but it got stuck as shown in the screenshot and was aborted after three hours. Any idea what could have gone wrong here?
Larry
Screenshot 2020-07-31 at 15.56.34.png
Email Gateway (Aug 01 2020 at 09:16):From: Lawrence Paulson <lp15@cam.ac.uk>
Run #347 (with one slightly modified lemma) also aborted, in a different place:
21:50:01 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Weakening
21:52:04 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class2
21:52:06 HOL-Nominal-Examples: theory HOL-Nominal-Examples.Class3
23:42:11 Build timed out (after 180 minutes). Marking the build as aborted.
23:42:11 Build was aborted
What could be going on?
Larry
On 31 Jul 2020, at 16:26, Lawrence Paulson <lp15@cam.ac.uk> wrote:
I had a run going (the change involved adding a single lemma and shouldn’t have affected anything) but it got stuck as shown in the screenshot and was aborted after three hours. Any idea what could have gone wrong here?
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 01 2020 at 11:24):From: Tobias Nipkow <nipkow@in.tum.de>
I suspect that is not of your making. Poly/ML, OS and even the hardware come to
mind...
Tobias
smime.p7s
Email Gateway (Aug 03 2020 at 11:33):From: Makarius <makarius@sketis.net>
There might be even changes in timing due to hot temperatures outside.
But I've seen such spurious "hangs" occasionally, approx. in the past 12
months. It might be due to subtle changes in how parallel proofs and proof
terms are managed. I am in the process to investigate it further: luckily
there is a mostly reproducible situation on a Mac Mini provided by EPFL.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 04 2020 at 10:33):From: Lawrence Paulson <lp15@cam.ac.uk>
I have had the same outcome in three consecutive runs, so I wonder what we should do now: is it possible to push changes that run okay as far as it goes, or do we have a moratorium until we can get it working again?
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 04 2020 at 10:39):From: Makarius <makarius@sketis.net>
There is no need to satisfy the testboard setup: tests merely need to work via
normal local runs of "isabelle build -a".
Note that over the decades, we have always had the situation that tests might
have to be repeated until it is clear that they do work: Poly/ML + Isabelle/ML
is a slightly non-deterministic game.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 04 2020 at 10:46):From: Lawrence Paulson <lp15@cam.ac.uk>
I could do this quite easily on my nice big work machine, but it’s really not practical on a laptop. I hope we can get the testboard working again soon.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 04 2020 at 11:52):From: Makarius <makarius@sketis.net>
Recall that it is a design flaw of the testboard that it does not allow to
retry builds: you need to make some workarounds with pointless commits.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 06 2020 at 13:37):From: Makarius <makarius@sketis.net>
On 03/08/2020 13:33, Makarius wrote:
On 01/08/2020 13:24, Tobias Nipkow wrote:
I suspect that is not of your making. Poly/ML, OS and even the hardware come
to mind...
On 01/08/2020 11:15, Lawrence Paulson wrote:
Run #347 (with one slightly modified lemma) also aborted, in a different place:
There might be even changes in timing due to hot temperatures outside.
But I've seen such spurious "hangs" occasionally, approx. in the past 12
months. It might be due to subtle changes in how parallel proofs and proof
terms are managed. I am in the process to investigate it further: luckily
there is a mostly reproducible situation on a Mac Mini provided by EPFL.
In the meantime I have made a few changes towards a more robust situation,
notably:
changeset: 72078:b8d0b8659e0a
user: wenzelm
Last updated: Dec 21 2024 at 16:20 UTC