Hi Larry, you are right. I think the best resolution is to make Cardinal_Notations part of HOL-Cardinals. I thought that there are more things in HOL-Cardinals that depend on HOL-Library, but this seems not to be the case. I.e., once Cardinal_Notations is moved there, HOL-Cardinals can be based on HOL (instead of HOL-Library), thus avoiding the cycle.
At least one theory in HOL-Library depends on Cardinal_Notations, but this should be unproblematic. I produced a patch, but run into the problem Jasmin reported today when trying to test it. (I'll write more in the other thread.) Dmitriy > On 4 Apr 2019, at 17:29, Lawrence Paulson <[email protected]> wrote: > > And I wonder whether the problem is that > > Cardinals/Wellorder_Constructions > > imports "HOL-Library.Cardinal_Notations" (Which is a tiny file) which might > create a circular dependence if any theory in Library tried to load something > from Cardinals. Not that I understand how sessions work. > > Larry > >> On 4 Apr 2019, at 15:37, Lawrence Paulson <[email protected]> wrote: >> >> I’m trying to install some material in time for the next release and I've >> got tangled up in some issue connected with session structure. The theory >> header looks like this: >> >> theory "Free_Abelian_Groups" >> imports >> Product_Groups >> "HOL-Cardinals.Cardinal_Arithmetic" >> "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" >> "HOL-Library.Equipollence” >> >> But any attempt to load it produces the error message >> >>> /Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar: >>> Cannot start: >>> *** Duplicate theory "HOL-Cardinals.Cardinal_Arithmetic" vs. >>> "/Users/lp15/isabelle/Repos/src/HOL/Cardinals/Cardinal_Arithmetic.thy” >> >> I note that absolutely nothing in the distribution imports HOL-Cardinals. >> However, it’s imported in a number of places in the AFP. What gives? >> Larry >> >> > > _______________________________________________ > 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
