[isabelle-dev] Two problems

[Lawrence Paulson]

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 <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:
> 
>      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