[isabelle-dev] Typerep again

[Amine Chaieb]

I completely agree with Brian (even I can not agree to import Main 
instead of theories under Main).

There is only two things I can think of:
  1) You can't be serious about this
  2) We are all sitting back and watching how things get worse.

The bootstrap process of Main *was* fragile. For these new problems I 
must consult the Thesaurus for a better word (I might choose flimsy 
since it stand for both fragile, and unconvincing/implausible).

Amine.

Florian Haftmann wrote:
> Hi Brian,
> 
>>> Our current policy is the Plain, Main and Complex_Main are either
>>> ancestors or descendants of any theory.
>> OK, the requirement for Plain I can understand. For Main, it doesn't
>> seem too unreasonable, assuming it's necessary (since most theory files
>> import Main anyway).
>>
>> But Complex_Main? Are you serious? Implementing this policy would
>> require changes to a LOT of theories: HOLCF, every subdirectory of
>> src/HOL, all the AFP contributions, all user-created Isabelle theories
>> in the entire world that import Main, etc.
> 
> The "any" here is supposed to range over all theories in the HOL image;
>  indeed Complex_Main need not be taken too serious since the fragile
> tool bootstraps are already finished with Main.
> 
> Cheers,
> 	Florian
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev