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

[Thiemann, René]

I know: I just forgot to add "HOL-Real_Asymp” into the corresponding ROOT-file under sessions.
(This error did not show up when using jEdit without an isabelle build)

at least on my machine, with commit 1fa9b1612d09  Perron-Frobenius compiles again.

Sorry,
René

> Am 05.09.2019 um 13:17 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> 
> I have no idea how to fix this total failure of AFP-devel:
> 
> 02:13:24 Session AFP/Linear_Recurrences (AFP)
> 02:13:24 Session AFP/Perron_Frobenius (AFP)
> 02:13:24 *** Cannot load theory "HOL-Real_Asymp.Real_Asymp"
> 02:13:24 *** The error(s) above occurred in session "Perron_Frobenius" (line 3 of "/media/data/jenkins/workspace/isabelle-all/afp/thys/Perron_Frobenius/ROOT")
> 02:13:25 Build step 'Execute shell' marked build as failure
> 
> I get the same error on my machine:
> 
> ~/isabelle/Repos/src/HOL: isabelle build -j4 -a -o threads=6
> *** Cannot load theory "HOL-Real_Asymp.Real_Asymp"
> *** The error(s) above occurred in session "Perron_Frobenius" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Perron_Frobenius/ROOT”)
> 
> With “Isabelle jEdit” I get the dreaded
> 
> *** Duplicate theory "HOL-Real_Asymp.Real_Asymp" vs. "/Users/lp15/isabelle/Repos/src/HOL/Real_Asymp/Real_Asymp.thy"
> 
> Unless I first delete /Users/lp15/isabelle/afp/devel/thys from ~/.isabelle/ROOT.
> 
> Any tips? Because to me it looks like game over.
> 
> Larry
> 
> > Begin forwarded message:
> >
> > From: Isabelle/Jenkins <ci at isabelle.systems>
> > Subject: [Isabelle-ci] Build failure in AFP
> > Date: 5 September 2019 at 01:17:36 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/1355/
> > _______________________________________________
> > Isabelle-ci mailing list
> > Isabelle-ci at mailman46.in.tum.de
> > https://mailman46.in.tum.de/mailman/listinfo/isabelle-ci
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> <build.log>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 874 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190905/e40f0326/attachment-0001.sig>