Of course a full solution might be a lot of work. But merely to detect the presence of two identically-named theories (in the spirit of detecting instances of a variable with two different types) might be straightforward, even if the only response is a fatal error. Since otherwise the outcome might be very confusing.
Larry On 8 Dec 2012, at 13:18, Makarius <[email protected]> wrote: > On Mon, 3 Dec 2012, Lawrence Paulson wrote: > >> Surely the existence of two theories of the same name can be detected? > > The deeper problem here is that theories still have the ancient flat name > space. So the file-system paths in the source are ultimately stripped to the > base name when doing comparisons. > > > We are still moving (extremely slowly) towards fully-qualified theory names > of the form SESSION.THEORY, e.g. "HOL.Main", "HOLCF.HOLCF" with some ways to > omit the prefix within the same session, say. > > The isabelle build reform from this summer already introduces an authentic > name space for (unqualified) session names. > > Here are some of the remaining obstacles to prefix session names to theory > names: > > * Too many ways to manage theory dependencies. There are old and new > theory loader variants and combinations: isabelle tty, build, emacs, > jedit all do it slightly differently. Ultimately, I would like to see > just one way in Isabelle/Scala, and even Proof General would use that > without taking notice. > > * Proof tools that assume that the long names for formal entities look > like this: > > THEORY.NAME > THEORY.LOCALE.NAME > > Larry himself introduced this assumption some years ago, but it was > not there in 1998 when I introduced the name space concept in > Isabelle. ML tools should not guess at the layout of full names. > This is an abstract datatype that happens to be implemented as > "string" for historical reasons. > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
