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

[Lawrence Paulson]

Thanks. Kind of strange that a problem with a single AFP entry can have global effects.
Larry

> On 5 Sep 2019, at 13:37, Thiemann, René <Rene.Thiemann at uibk.ac.at> wrote:
> 
> 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>
>