[isabelle-dev] Duplicate theory??

[Klein, Gerwin (Data61, Kensington NSW)]

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 <lp15 at cam.ac.uk> 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 <lp15 at cam.ac.uk> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev