Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] [Isabelle-ci] Build failure in AFP


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.de

The 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: Mar 04 2024 at 12:30 UTC