Email Gateway (Jul 28 2025 at 09:18): Email Gateway (Jul 28 2025 at 09:18):From: Vincent Jackson <vjjac@student.unimelb.edu.au>
Hello all,
Recently I tried to build an old project (in Isabelle 2025, but which
last built on Isabelle 2019), and got a "Duplicate use of directory"
error. This problem appears to show up whenever there are two sessions
in the same ROOT file, but which use different theory files from the
current directory.
In which Isabelle edition did this error become a thing, and what is the
intended way we should structure our sessions now? I do not understand
why this is now an error; I find it strange that it now seems necessary
to mirror the session hierarchy in our directory hierarchy. Is there a
way to build different sessions from the same directory that I am not
aware of, or is this the intent of the change?
Also, this behaviour does not seem to be documented in the Isabelle
System Manual (at least, not in §2.1), so that should be updated.
Thanks,
Vincent Jackson
Ph.D. Student
School of Computing and Information Systems
The University of Melbourne
P.S.
I have constructed a minimal example of the problem as follows:
$ cat A.thy
theory A
imports Main
begin
end
$ cat B.thy
theory B
imports A
begin
end
$ cat ROOT
session A = Main +
theories
"A"
session B = A +
theories
"B"
and the error that results is
/home/admin/.isabelle/Isabelle2025/jedit/jars/isabelle_jedit_main.jar:
Cannot start:
*** Duplicate use of directory "/home/admin/Development/Isabelle/Theories"
*** for session "A" (line 2 of "/home/admin/Development/Isabelle/Theories/ROOT")
*** vs. session "B" (line 6 of "/home/admin/Development/Isabelle/Theories/ROOT")
Email Gateway (Jul 28 2025 at 10:44):From: Makarius <makarius@sketis.net>
On 28/07/2025 07:02, Vincent Jackson wrote:
Recently I tried to build an old project (in Isabelle 2025, but which last
built on Isabelle 2019), and got a "Duplicate use of directory" error. This
problem appears to show up whenever there are two sessions in the same ROOT
file, but which use different theory files from the current directory.In which Isabelle edition did this error become a thing, and what is the
intended way we should structure our sessions now?
See the NEWS file, as for any new Isabelle release. The relevant entry is:
"""
New in Isabelle2020 (April 2020)
* General *
Also, this behaviour does not seem to be documented in the Isabelle System
Manual (at least, not in §2.1), so that should be updated.
I do see this text in §2.1:
"""
directories dirs specifies additional directories for import of theory files
via theories within ROOT or imports within a theory; dirs are relative
to the main session directory (cf. session . . . in dir). These directories
need to be exclusively assigned to a unique session, without implicit
sharing of file-system locations.
"""
Makarius
Email Gateway (Jul 28 2025 at 12:37):From: Makarius <makarius@sketis.net>
On 28/07/2025 14:27, Vincent Jackson wrote:
I think it would be good to note explicitly in the "session"
syntax documentation (or maybe the "session ... in ..." syntax documentation)
that every session has an associated directory (which, as already explained in
the documentation, is either explicitly given using the "in ..." syntax or
defaults to the current directory) and that each directory so associated must
be assigned to only one session.
This documentation is unusually clear and explicit. I won't add even more text.
Makarius
Email Gateway (Jul 30 2025 at 09:11):From: Vincent Jackson <vjjac@student.unimelb.edu.au>
I see. Thanks for finding that.
That documentation could be better placed. The listing you have
identified is for the "directories" syntax, which is why I,
unfortunately, overlooked it. (As I did not use that syntax element.)
The documentation also says these directories are "additional", but the
duplicate directory exclusion also applies to the default directory.
(And one can traverse additional directories via the "in ..." syntax too.)
I think it would be good to note explicitly in the "session"
syntax documentation (or maybe the "session ... in ..." syntax
documentation) that every session has an associated directory (which, as
already explained in the documentation, is either explicitly given using
the "in ..." syntax or defaults to the current directory) and that each
directory so associated must be assigned to only one session.
In any case, thanks for answering my questions.
Vincent
On 28/7/25 20:44, Makarius wrote:
On 28/07/2025 07:02, Vincent Jackson wrote:
Recently I tried to build an old project (in Isabelle 2025, but which
last built on Isabelle 2019), and got a "Duplicate use of directory"
error. This problem appears to show up whenever there are two
sessions in the same ROOT file, but which use different theory files
from the current directory.In which Isabelle edition did this error become a thing, and what is
the intended way we should structure our sessions now?See the NEWS file, as for any new Isabelle release. The relevant entry
is:"""
New in Isabelle2020 (April 2020)
* General *
- Session ROOT files need to specify explicit 'directories' for import
of theory files. Directories cannot be shared by different sessions.
(Recall that import of theories from other sessions works via
session-qualified theory names, together with suitable 'sessions'
declarations in the ROOT.)
"""Also, this behaviour does not seem to be documented in the Isabelle
System Manual (at least, not in §2.1), so that should be updated.I do see this text in §2.1:
"""
directories dirs specifies additional directories for import of theory
files
via theories within ROOT or imports within a theory; dirs are relative
to the main session directory (cf. session . . . in dir). These
directories
need to be exclusively assigned to a unique session, without implicit
sharing of file-system locations.
"""Makarius
Last updated: Aug 20 2025 at 20:23 UTC