brianh at cs.pdx.edu
Tue Jan 20 21:28:33 CET 2009
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.
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!
More information about the isabelle-dev