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

Lawrence Paulson lp15 at cam.ac.uk
Tue Oct 20 12:54:57 CEST 2020


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

> Begin forwarded message:
> 
> From: Isabelle/Jenkins <ci at isabelle.systems>
> Subject: [Isabelle-ci] Build failure in AFP
> Date: 20 October 2020 at 00:02:18 BST
> To: isabelle-ci at mail46.informatik.tu-muenchen.de
> 
> The AFP build failed. See the log at: https://ci.isabelle.systems/jenkins/job/isabelle-all/2349/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: build.log
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20201020/ba21e873/attachment-0001.ksh>
-------------- next part --------------
> _______________________________________________
> Isabelle-ci mailing list
> Isabelle-ci at mailman46.in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-ci



More information about the isabelle-dev mailing list