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
