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é <[email protected]> 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 <[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> > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
