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

[Lawrence Paulson]

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/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: build.log
Type: application/octet-stream
Size: 22305 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190905/5cbd2bec/attachment.obj>
-------------- next part --------------
> _______________________________________________
> Isabelle-ci mailing list
> Isabelle-ci at mailman46.in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-ci