What about your ~/.isabelle/etc/settings? Is there an init_component in there with afp-devel?
Cheers, Gerwin > On 08.04.2019, at 21:06, Lawrence Paulson <[email protected]> wrote: > > Here’s a funny thing. I tried deleting Countable_Set_Type from Library.thy > and got a different error (see below). > > So it involved the AFP. So I updated the AFP and it works again. That’s > already odd, but… > > My .isabelle/etc/components is blank! No reference to afp_devel. What the > hell?? > > Larry > >> On 8 Apr 2019, at 11:42, Lawrence Paulson <[email protected]> wrote: >> >> No, no changes >> Larry > > Cannot load theory "HOL-Library.Cardinal_Notations" > The error(s) above occurred for theory "HOL-Library.Cardinal_Notations" > (required by "BNF_CC.Operation_Examples" via "BNF_CC.Composition" via > "BNF_CC.Axiomatised_BNF_CC") (line 8 of > "/Users/lp15/isabelle/afp/devel/thys/BNF_CC/Axiomatised_BNF_CC.thy") > No such file: "HOL-Library.Cardinal_Notations" > The error(s) above occurred in session "BNF_CC" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/BNF_CC/ROOT") > Cannot load theory "HOL-Library.Countable_Set_Type" > The error(s) above occurred for theory "HOL-Library.Countable_Set_Type" > (required by "Nested_Multisets_Ordinals.Unary_PCF") (line 11 of > "/Users/lp15/isabelle/afp/devel/thys/Nested_Multisets_Ordinals/Unary_PCF.thy") > No such file: "HOL-Library.Countable_Set_Type" > The error(s) above occurred in session "Nested_Multisets_Ordinals" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Nested_Multisets_Ordinals/ROOT") > Cannot load theory "HOL-Library.Countable_Set_Type" > The error(s) above occurred for theory "HOL-Library.Countable_Set_Type" > (required by "CryptHOL.Misc_CryptHOL" via > "Monomorphic_Monad.Monomorphic_Monad") (line 7 of > "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy") > No such file: "HOL-Library.Countable_Set_Type" > The error(s) above occurred in session "CryptHOL" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/CryptHOL/ROOT") > Cannot load theory "HOL-Library.Countable_Set_Type" > The error(s) above occurred for theory "HOL-Library.Countable_Set_Type" > (required by "Monomorphic_Monad.Monomorphic_Monad") (line 7 of > "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy") > No such file: "HOL-Library.Countable_Set_Type" > The error(s) above occurred in session "Monomorphic_Monad" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/ROOT") > Cannot load theory "HOL-Library.Countable_Set_Type" > The error(s) above occurred for theory "HOL-Library.Countable_Set_Type" > (required by "Sort_Encodings.Encodings" via "Sort_Encodings.G" via > "Sort_Encodings.T_G_Prelim" via "Sort_Encodings.Mcalc" via > "Sort_Encodings.Mono" via "Sort_Encodings.CM" via "Sort_Encodings.M" via > "Sort_Encodings.TermsAndClauses" via "Sort_Encodings.Preliminaries") (line 4 > of "/Users/lp15/isabelle/afp/devel/thys/Sort_Encodings/Preliminaries.thy") > No such file: "HOL-Library.Countable_Set_Type" > The error(s) above occurred in session "Sort_Encodings" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/Sort_Encodings/ROOT") > Cannot load theory "HOL-Library.Countable_Set_Type" > The error(s) above occurred for theory "HOL-Library.Countable_Set_Type" > (required by "UTP-Toolkit.utp_toolkit" via "UTP-Toolkit.Countable_Set_Extra") > (line 12 of > "/Users/lp15/isabelle/afp/devel/thys/UTP/toolkit/Countable_Set_Extra.thy") > No such file: "HOL-Library.Countable_Set_Type" > The error(s) above occurred in session "UTP-Toolkit" (line 12 of > "/Users/lp15/isabelle/afp/devel/thys/UTP/ROOT") > Cannot load theory "HOL-Library.Cardinal_Notations" > The error(s) above occurred for theory "HOL-Library.Cardinal_Notations" (line > 8 of "/Users/lp15/isabelle/afp/devel/thys/BNF_Operations/ROOT") > No such file: "HOL-Library.Cardinal_Notations" > The error(s) above occurred in session "BNF_Operations" (line 3 of > "/Users/lp15/isabelle/afp/devel/thys/BNF_Operations/ROOT") > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
