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
