Now that I'm beginning to understand what typerep is, I most certainly agree that it is too specialized to force it on everybody.
Tobias Alexander Krauss wrote: > Brian Huffman wrote: >> I, for one, am rather alarmed at the hurdles that Amine was forced to >> overcome to do a simple merge of two theories. > > I agree. > >> 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. > > In fact, "typerep" is not the only class that is instantiated > automatically. Another one is "size", which is also of a technical > nature. But it never posed problems, I think, because it is installed > early enough that everybody inherits from it. > > I think that automatic class instantiations are acceptable provided that > a) the class is for "internal" use of some tools and manual > instantiation is discouraged, and b) The mechanism is installed early > enough to avoid the merge issue. > > IMO the options are > > 1) Make the whole Typerep theory optional, to be loaded together with > the Imperative HOL theories. > > 2) Typerep provides a top-level command for generating the instantiations. > > 3) Move Typerep up the hierarchy, such that it is always present and > there are no merge problems. > > Note that 1 and 2 do not actually solve the problem but only limit it to > theories that use Imperative HOL (in 1) or the top-level command (in 2). > I think I nevertheless prefer option 1, since Typerep is really a > specialized thing. > > The cleanest, but also the hardest solution would be to make class > instances "applicative" instead of "generative" (I may be streching the > terms a bit far here), such that equal class instances do *not* collide > at a later merge. > > Alex > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
