[isabelle-dev] typrep?

[Tobias Nipkow]

What are these automatically-generated class instances?

And yes, if even experienced users like Amine are confused, we have a
problem.

Tobias

Brian Huffman schrieb:
> Hi Florian,
> 
> I, for one, am rather alarmed at the hurdles that Amine was forced to
> overcome to do a simple merge of two theories. Even before the
> typerep-related problems, merging Isabelle theories was already
> difficult enough! I think that merging theories is one of Isabelle's
> most serious weaknesses, and it has prevented many users from being able
> to borrow, share, and build upon each other's code. (Witness how little
> re-use of code there has been among AFP entries, in spite of the
> recommendation in the submission guidelines, "It is possible and
> encouraged to build on other archive entries in your submission.")
> 
> With this in mind, automatically-generated class instances are a step in
> the wrong direction. Assuming we can find solutions to name-space and
> syntax clashes, the only thing that can make two theories truly
> incompatible is having two different instantiations for overloaded
> constants at the same type. Adding class instantiations can introduce
> theory incompatibilities, and for this reason, adding class
> instantiations should not be taken lightly---and they should certainly
> not be done automatically!
> 
> I think that the automatic class-instantiations should be disabled
> immediately, and replaced with a new top-level command so that these
> instantiations can be done explicitly, and individually.
> 
> Facilitating the merging of theories written by different people should
> be a much higher priority. Arranging theory graphs should not have to be
> nearly so difficult as it is.
> 
> - Brian
> 
> 
> Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 
>> Hi Amine,
>>
>> I guess you are in the following thygraph situation:
>>
>>     Typrep  Real
>>        | /  \ |
>>        |/    \|
>> Complex_Main  FPS
>>        \      /
>>         \    /
>>          \  /
>>           Foo
>>
>> Real defines type real, Typerep class typerep (;-)).  Then both in
>> Complex_Main and FPS and instance for typerep on type real is generated
>> automatically (thanks to generic interpretation), which clash on merge
>> into theory Foo.
>>
>> The solution is too arrange that there is only one meeting point of
>> Typrep and Real in the thygraph.  According to your second email you
>> have already found a way.
>>
>> N.B. arranging the HOL thygraph is a nontrivial task!
>>
>> Cheers,
>>     Florian
> 
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev