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 <[email protected]>: > > 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 <[email protected]> > > Subject: [Isabelle-ci] Build failure in AFP > > Date: 5 September 2019 at 01:17:36 BST > > To: [email protected] > > > > The AFP build failed. See the log at: > > https://ci.isabelle.systems/jenkins/job/isabelle-all/1355/ > > _______________________________________________ > > Isabelle-ci mailing list > > [email protected] > > https://mailman46.in.tum.de/mailman/listinfo/isabelle-ci > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > <build.log>
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
