[isabelle-dev] Two problems
lp15 at cam.ac.uk
Sat Dec 8 19:50:47 CET 2012
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.
On 8 Dec 2012, at 13:18, Makarius <makarius at sketis.net> 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:
> 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.
More information about the isabelle-dev