nipkow at in.tum.de
Tue Jan 20 21:49:03 CET 2009
What are these automatically-generated class instances?
And yes, if even experienced users like Amine are confused, we have a
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
>> \ /
>> \ /
>> \ /
>> 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!
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev