[isabelle-dev] Duplicate theory??
traytel at inf.ethz.ch
Fri Apr 5 16:33:33 CEST 2019
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.)
> On 4 Apr 2019, at 17:29, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> And I wonder whether the problem is that
> 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.
>> On 4 Apr 2019, at 15:37, Lawrence Paulson <lp15 at cam.ac.uk> 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"
>> "HOL-Library.Countable_Set" "HOL-Library.Poly_Mapping" "HOL-Library.Equipollence”
>> But any attempt to load it produces the error message
>>> 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev