[isabelle-dev] Duplicate theory??

[Traytel Dmitriy]

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