Email Gateway (Aug 09 2020 at 17:56): Email Gateway (Aug 09 2020 at 17:56):From: Lawrence Paulson <lp15@cam.ac.uk>
What on Earth is this?
Also on the testboard.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 09 2020 at 18:28):From: Makarius <makarius@sketis.net>
I guess it is a situation that David Matthews has described to me privately:
$HOME/.polyml is somehow filled up and should be purged.
I cannot do anything about testboard.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 11 2020 at 15:01):From: Makarius <makarius@sketis.net>
David Matthews has solved this particular problem on his side already some
days ago, but presently I cannot follow the Poly/ML repository, because there
are othe problems (see Isabelle/284d6c06cbfb).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 11 2020 at 19:54):From: Makarius <makarius@sketis.net>
David Mattews has pushed more changes, so we are now on
polyml-test-f54aa41240d0 in Isabelle/c500f6c86e86.
There is some chance that all odd problems from the past couple of months are
now solved.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 20 2020 at 10:55):From: Lawrence Paulson <lp15@cam.ac.uk>
It’s a bit alarming to get an email containing a link to a page saying the distribution has failed. And when you examine the log it turns out that only an AFP entry has failed (HOL-ODE-Numerics), not the distribution. And when you run the AFP entry, it works fine:
devel/thys: isabelle build -d ~/isabelle/afp/devel/thys HOL-ODE-Numerics
Building HOL-Analysis ...
Finished HOL-Analysis (0:03:31 elapsed time, 0:21:22 cpu time, factor 6.06)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:12 elapsed time, 0:05:45 cpu time, factor 4.76)
Running HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:08:40 elapsed time, 0:38:06 cpu time, factor 4.39)
0:13:35 elapsed time, 1:05:14 cpu time, factor 4.80
devel/thys:
Can anybody figure out what’s going on here? GoedelGod also produces spurious messages sometimes.
Larry
build.log
Email Gateway (Oct 20 2020 at 11:03):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/10/2020 12:54, Lawrence Paulson wrote:
It’s a bit alarming to get an email containing a link to a page saying the distribution has failed. And when you examine the log it turns out that only an AFP entry has failed (HOL-ODE-Numerics), not the distribution. And when you run the AFP entry, it works fine:
devel/thys: isabelle build -d ~/isabelle/afp/devel/thys HOL-ODE-Numerics
Building HOL-Analysis ...
Finished HOL-Analysis (0:03:31 elapsed time, 0:21:22 cpu time, factor 6.06)
Building Ordinary_Differential_Equations ...
Finished Ordinary_Differential_Equations (0:01:12 elapsed time, 0:05:45 cpu time, factor 4.76)
Running HOL-ODE-Numerics ...
Finished HOL-ODE-Numerics (0:08:40 elapsed time, 0:38:06 cpu time, factor 4.39)
0:13:35 elapsed time, 1:05:14 cpu time, factor 4.80
devel/thys:Can anybody figure out what’s going on here?
This is a known problem due to a change in directory structure. Lars tells me he
is talking to Gerwin about it.
GoedelGod also produces spurious messages sometimes.
This is due to a change in some backend tool. Makarius is aware.
Tobias
Larry
Begin forwarded message:
From: Isabelle/Jenkins <ci@isabelle.systems>
Subject: [Isabelle-ci] Build failure in AFP
Date: 20 October 2020 at 00:02:18 BST
To: isabelle-ci@mail46.informatik.tu-muenchen.deThe AFP build failed. See the log at: https://ci.isabelle.systems/jenkins/job/isabelle-all/2349/
Isabelle-ci mailing list
Isabelle-ci@mailman46.in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-ci
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Last updated: Apr 26 2024 at 08:19 UTC