[isabelle] Isabelle2018-RC1: No error when loading same theory under two names

[Dominique Unruh]

Hi,

I think the following should (depending on the intended semantics of
sessions) either give an error or have a different behavior.

In a specific setup (see below) involving sessions, the Draft session, and
a symlinked directory, jEdit will load the same theory file twice, once as
A.A and once as Draft.A. There will be no error message. Both A's in the
theory panel will open the same file, but editing that file will affect
only one of the two instances of A in the Isabelle backend. (E.g., typing
nonsense will produce red marks in the theory panel in only one of the
A's.) The other A is effectively read-only.

How to reproduce?

- Untar the attached tgz (in Linux).
- It contains a session root directory dir1, and a symlink dir2 to dir1
- The session root contains a session A with A.thy, a session B = A +
B.thy, and a sessionless file Test.thy (e.g., a scratch file) importing
A.thy without qualification
- Run Isabelle with parameters "jedit -d dir2 dir2/B.thy dir2/Test.thy

Observations:

- The effect does not occur when first cd'ing into dir2.
- The effect can also be avoided by always using qualified imports in
scratch-theories (like Test.thy)
- The effect can be avoided by avoiding symlinks
- Possibly the theory import as I did it is "improper" user behavior
(although convenient for experimentation), this is why I wrote that there
should probably an error message.


Best wishes,
Dominique.

[Makarius]

Post by Dominique Unruh
I think the following should (depending on the intended semantics of
sessions) either give an error or have a different behavior.
In a specific setup (see below) involving sessions, the Draft session, and
a symlinked directory, jEdit will load the same theory file twice, once as
A.A and once as Draft.A. There will be no error message. Both A's in the
theory panel will open the same file, but editing that file will affect
only one of the two instances of A in the Isabelle backend. (E.g., typing
nonsense will produce red marks in the theory panel in only one of the
A's.) The other A is effectively read-only.
How to reproduce?
- Untar the attached tgz (in Linux).
- It contains a session root directory dir1, and a symlink dir2 to dir1
- The session root contains a session A with A.thy, a session B = A +
B.thy, and a sessionless file Test.thy (e.g., a scratch file) importing
A.thy without qualification
- Run Isabelle with parameters "jedit -d dir2 dir2/B.thy dir2/Test.thy

Somehow the attachment did not get on the mailing list.

Post by Dominique Unruh
- The effect does not occur when first cd'ing into dir2.
- The effect can also be avoided by always using qualified imports in
scratch-theories (like Test.thy)
- The effect can be avoided by avoiding symlinks
- Possibly the theory import as I did it is "improper" user behavior
(although convenient for experimentation), this is why I wrote that there
should probably an error message.

I can imagine various inconvenient situations, especially with symlinks:
I don't think the system works properly in the general situation, but
the example might be sufficiently easy to make it more robust (for a
release after Isabelle2018).

Concerning improper imports of theories from other sessions, without
using the session-qualified names, Isabelle2018 is likely to cause
problems for users who did not take the corresponding NEWS entries in
Isabelle2017 and Isabelle2018 seriously, or just did not read them --
this might be actually the majority.

We probably need to rethink the theory import scheme one again, i.e.
remove further degrees of freedom from the user, and allow theory files
to reside only in the session directory itself. This would also speed up
the exploration of theory dependencies in the Prover IDE, to map plain
files to formal session-qualified names.


Makarius

[Dominique Unruh]

Hi,

Post by Makarius
Somehow the attachment did not get on the mailing list.

I forgot to attach it. Unfortunately, I don't seem to have the example any
more.

Concerning improper imports of theories from other sessions, without

Post by Makarius
using the session-qualified names, Isabelle2018 is likely to cause
problems for users who did not take the corresponding NEWS entries in
Isabelle2017 and Isabelle2018 seriously, or just did not read them --
this might be actually the majority.

Even when following those instruction, there can be some confusion in
jEdit/PIDE (short: jEdit), I think.
While for the build process, I think everything is clear (when reading
enough of the documentation), in jEdit, I am not sure it's totally clear
how jEdit determines dynamically which theory file is in which session.
(E.g., with Isabelle 2018, I have had a number of times the situation that
I created a new theory file (which then jEdit assumes to be in Draft), then
imported it from another theory (which is already in a named session X),
and then the new theory should be in the X (not in Draft anymore), but it
takes a bit of closing of files and clicking the Purge button until jEdit
realizes this. In the process, I see duplicated theories in the theory
view, etc.) All those problems are transient though (in the sense that they
vanish when restarting jEdit).

Best wishes,
Dominique.

Post by Makarius

Post by Dominique Unruh
I think the following should (depending on the intended semantics of
sessions) either give an error or have a different behavior.
In a specific setup (see below) involving sessions, the Draft session,

and

Post by Dominique Unruh
a symlinked directory, jEdit will load the same theory file twice, once

as

Post by Dominique Unruh
A.A and once as Draft.A. There will be no error message. Both A's in the
theory panel will open the same file, but editing that file will affect
only one of the two instances of A in the Isabelle backend. (E.g., typing
nonsense will produce red marks in the theory panel in only one of the
A's.) The other A is effectively read-only.
How to reproduce?
- Untar the attached tgz (in Linux).
- It contains a session root directory dir1, and a symlink dir2 to

dir1

Post by Dominique Unruh
- The session root contains a session A with A.thy, a session B = A +
B.thy, and a sessionless file Test.thy (e.g., a scratch file)

importing

Post by Dominique Unruh
A.thy without qualification
- Run Isabelle with parameters "jedit -d dir2 dir2/B.thy dir2/Test.thy

Somehow the attachment did not get on the mailing list.

Post by Dominique Unruh
- The effect does not occur when first cd'ing into dir2.
- The effect can also be avoided by always using qualified imports in
scratch-theories (like Test.thy)
- The effect can be avoided by avoiding symlinks
- Possibly the theory import as I did it is "improper" user behavior
(although convenient for experimentation), this is why I wrote that

there

Post by Dominique Unruh
should probably an error message.

I don't think the system works properly in the general situation, but
the example might be sufficiently easy to make it more robust (for a
release after Isabelle2018).
Concerning improper imports of theories from other sessions, without
using the session-qualified names, Isabelle2018 is likely to cause
problems for users who did not take the corresponding NEWS entries in
Isabelle2017 and Isabelle2018 seriously, or just did not read them --
this might be actually the majority.
We probably need to rethink the theory import scheme one again, i.e.
remove further degrees of freedom from the user, and allow theory files
to reside only in the session directory itself. This would also speed up
the exploration of theory dependencies in the Prover IDE, to map plain
files to formal session-qualified names.
Makarius

[Makarius]

Post by Dominique Unruh
Even when following those instruction, there can be some confusion in
jEdit/PIDE (short: jEdit), I think.
While for the build process, I think everything is clear (when reading
enough of the documentation), in jEdit, I am not sure it's totally clear
how jEdit determines dynamically which theory file is in which session.
(E.g., with Isabelle 2018, I have had a number of times the situation that
I created a new theory file (which then jEdit assumes to be in Draft), then
imported it from another theory (which is already in a named session X),
and then the new theory should be in the X (not in Draft anymore), but it
takes a bit of closing of files and clicking the Purge button until jEdit
realizes this.

Do you have more symlinks here?

Anyway, it is very difficult to have a discussion with non-standard
terminology. The standard one is as follows:

* VSCode: a text editor by Microsoft
* jEdit: a text editor by the jEdit project team
* PIDE: some Isabelle infrastructure for Prover IDEs
* Isabelle/VSCode: Isabelle Prover IDE based on VSCode
* Isabelle/jEdit: Isabelle Prover IDE based on jEdit

Recently I have tried hard to make the behaviour of Isabelle/VSCode and
Isabelle/jEdit agree, concerning the mapping of plain file names to
formal session-qualified theory names, but there might be still oddities
somewhere. Figuring that out, requires to look very closely what really
happens, and where.


Makarius

[Dominique Unruh]

Sorry, I mixed up the names. I meant Isabelle/jEdit when I said jEdit/PIDE.

Do you have more symlinks here?
The environment where I work on my main development has a symlink, so I
cannot tell whether it's part of the cause.
Unfortunately, I don't know how to reliably reproduce the problem, so I
cannot test it in a symlink-free directly.
So it may or may not be related to symlinks.


But I did find the tgz for the prior example. (Attached. Please add .tgz to
the file name, GMail didn't allow me to send it with the correct file
ending.)
I am attaching it.
I would like to stress that that example does not "use" the symlinks.
That is, I never refer to the same file via two different paths.
I only refer to dir2 (never dir1).
So my guess is that there is some inconsistency in when paths are
normalized and when not.

The specific case is quite exotic, so I don't think it needs to be fixed
for it's own sake (I can work around it).
I posted it mainly because I thought it might indicate some bug somewhere
in the handling of paths that could lead to confusion in other cases, too.

Best wishes,
Dominique.

----
In a specific setup (see below) involving sessions, the Draft session, and
a symlinked directory, jEdit will load the same theory file twice, once as
A.A and once as Draft.A. There will be no error message. Both A's in the
theory panel will open the same file, but editing that file will affect
only one of the two instances of A in the Isabelle backend. (E.g., typing
nonsense will produce red marks in the theory panel in only one of the
A's.) The other A is effectively read-only.

How to reproduce?

- Untar the attached tgz (in Linux).
- It contains a session root directory dir1, and a symlink dir2 to dir1
- The session root contains a session A with A.thy, a session B = A +
B.thy, and a sessionless file Test.thy (e.g., a scratch file) importing
A.thy without qualification
- Run Isabelle with parameters "jedit -d dir2 dir2/B.thy dir2/Test.thy

Observations:

- The effect does not occur when first cd'ing into dir2.
- The effect can also be avoided by always using qualified imports in
scratch-theories (like Test.thy)
- The effect can be avoided by avoiding symlinks
- Possibly the theory import as I did it is "improper" user behavior
(although convenient for experimentation), this is why I wrote that there
should probably an error message.

Post by Makarius

Post by Dominique Unruh
Even when following those instruction, there can be some confusion in
jEdit/PIDE (short: jEdit), I think.
While for the build process, I think everything is clear (when reading
enough of the documentation), in jEdit, I am not sure it's totally clear
how jEdit determines dynamically which theory file is in which session.
(E.g., with Isabelle 2018, I have had a number of times the situation

that

Post by Dominique Unruh
I created a new theory file (which then jEdit assumes to be in Draft),

then

Post by Dominique Unruh
imported it from another theory (which is already in a named session X),
and then the new theory should be in the X (not in Draft anymore), but it
takes a bit of closing of files and clicking the Purge button until jEdit
realizes this.

Do you have more symlinks here?
Anyway, it is very difficult to have a discussion with non-standard
* VSCode: a text editor by Microsoft
* jEdit: a text editor by the jEdit project team
* PIDE: some Isabelle infrastructure for Prover IDEs
* Isabelle/VSCode: Isabelle Prover IDE based on VSCode
* Isabelle/jEdit: Isabelle Prover IDE based on jEdit
Recently I have tried hard to make the behaviour of Isabelle/VSCode and
Isabelle/jEdit agree, concerning the mapping of plain file names to
formal session-qualified theory names, but there might be still oddities
somewhere. Figuring that out, requires to look very closely what really
happens, and where.
Makarius

[Makarius]

Post by Makarius
Do you have more symlinks here?
The environment where I work on my main development has a symlink, so I
cannot tell whether it's part of the cause.
Unfortunately, I don't know how to reliably reproduce the problem, so I
cannot test it in a symlink-free directly.
So it may or may not be related to symlinks.
But I did find the tgz for the prior example. (Attached. Please add .tgz to
the file name, GMail didn't allow me to send it with the correct file
ending.)
I am attaching it.
I would like to stress that that example does not "use" the symlinks.
That is, I never refer to the same file via two different paths.
I only refer to dir2 (never dir1).
So my guess is that there is some inconsistency in when paths are
normalized and when not.
The specific case is quite exotic, so I don't think it needs to be fixed
for it's own sake (I can work around it).
I posted it mainly because I thought it might indicate some bug somewhere
in the handling of paths that could lead to confusion in other cases, too.

These are interesting corner cases, concerning the mapping of file names
to session-qualified theory names, and naming theories in the first place.

I have updated the test-archive slighty, to print the resulting formal
theory name within the context. E.g. in "isabelle build" the messages
end up in the session log gz files.

One problem with the symlink dir2 -> dir1 is that in one place it gets
normalized (e.g. isabelle.Sessions.Known.files) and in another place
this is omitted (e.g. isabelle.Sessions.directories). I have now updated
that for the next release (after Isabelle2018) as follows:

changeset: 68745:f95e2f145ea5
user: wenzelm
date: Wed Aug 15 13:02:48 2018 +0200
files: src/Pure/Thy/sessions.scala
description:
canonical session directories in correspondence to Known.files;


This avoids the duplication of theory A in Isabelle/jEdit, but that is
actually wrong! When you import just "A" from theory B.B, it should
become B.A: you can see that in the "isabelle build" log gz file.

The mistake is importing "A" from B.B instead of "A.A": it is a "general
user error", but the system could be more friendly in checking that and
pointing that out.

I think for the next release we really need a plain and simple scheme
where session theory files may reside, and rule out such odd situations
where a base directory contains files for different sessions.


Makarius

Post by Makarius
In a specific setup (see below) involving sessions, the Draft session, and
a symlinked directory, jEdit will load the same theory file twice, once as
A.A and once as Draft.A. There will be no error message. Both A's in the
theory panel will open the same file, but editing that file will affect
only one of the two instances of A in the Isabelle backend. (E.g., typing
nonsense will produce red marks in the theory panel in only one of the
A's.) The other A is effectively read-only.
How to reproduce?
- Untar the attached tgz (in Linux).
- It contains a session root directory dir1, and a symlink dir2 to dir1
- The session root contains a session A with A.thy, a session B = A +
B.thy, and a sessionless file Test.thy (e.g., a scratch file) importing
A.thy without qualification
- Run Isabelle with parameters "jedit -d dir2 dir2/B.thy dir2/Test.thy
- The effect does not occur when first cd'ing into dir2.
- The effect can also be avoided by always using qualified imports in
scratch-theories (like Test.thy)
- The effect can be avoided by avoiding symlinks
- Possibly the theory import as I did it is "improper" user behavior
(although convenient for experimentation), this is why I wrote that there
should probably an error message.