Email Gateway (Aug 23 2022 at 08:48): Email Gateway (Aug 23 2022 at 08:48):From: Mathias Pfeiffer <mathias.pfeiffer@rwth-aachen.de>
Greetings,
I am working with a session B that requires session A through the "session"
keyword (B has further dependencies and cannot make use of the "parent"). I
want to import a theory TheoryA from A into TheoryB of B. The theory
TheoryA lies within a subfolder X of A's directory:
session A in "A" = HOLCF +
theories
"X/TheoryA"
And B properly specifies its dependency:
session B in "B" = HOLCF +
sessions
"A"
theories
"TheoryB"
The import in TheoryB fails in Isabelle2020, succeeds in Isabelle2019:
theory TheoryB
imports A.TheoryA (* Bad theory import "A.TheoryA" *)
...
Is this a bug or intended behavior? If the former, when can we expect a
fix? If the later, where is the appropriate documentation for this behavior
change between the two versions of Isabelle?
Find the minimal working example attached below.
-Mathias
mwe_2020.zip
Email Gateway (Aug 23 2022 at 08:48):From: Makarius <makarius@sketis.net>
On 22/04/2020 13:02, Mathias Pfeiffer wrote:
I am working with a session B that requires session A through the "session"
keyword (B has further dependencies and cannot make use of the "parent"). I
want to import a theory TheoryA from A into TheoryB of B. The theory
TheoryA lies within a subfolder X of A's directory:
Such session-subdirectory arrangements often cause confusion, both to the user
and to the system implementation.
Since Isabelle2017 we have been moving to get more clarity and sanity, but
when brushing it up again for Isabelle2020, I did already see potential for
remaining boundary case that won't work.
The import in TheoryB fails in Isabelle2020, succeeds in Isabelle2019:
theory TheoryB
imports A.TheoryA (* Bad theory import "A.TheoryA" *)
...Is this a bug or intended behavior? If the former, when can we expect a
fix? If the later, where is the appropriate documentation for this behavior
change between the two versions of Isabelle?
The words "bug" and "fix" (and similarly "feature") don't make sense in the
Isabelle context: they are often interchangeable. Trying to "fix" something by
covering odd cases often introduces a "bug" in other cases.
So I never use these words. Instead it is all about simplicity, clarity, and
reduction of odd features.
If you had reported this observation before Isabelle2020 became final on
15-Apr-2020, I could have looked through the implementation to figure out if
it is reasonable to cover that case as well.
The next chance will be in approx. 9 months, when we are heading towards the
next release.
For that, I will seriously consider to disallow session-subdirectories as in
your example: I have already written this down some days ago in a commentary
for Isabelle2020/NEWS that will be presented on the virtual Isabelle Workshop
2020. Here is the preliminary text:
section ‹Distinctive session directories›
paragraph ‹NEWS›
text ‹
▪ Session ▩‹ROOT› files need to specify explicit \isakeyword{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 \isakeyword{sessions}
declarations in the ▩‹ROOT›.)
:black_small_square: Prover IDE startup is now much faster, because theory dependencies are no
longer explored in advance. The overall session structure with its
declarations of \isakeyword{directories} is sufficient to locate theory
files
›
paragraph ‹Trends›
text ‹
▪ Session-qualified theory names have first appeared in Isabelle2017
(October 2017). With Isabelle2020, the main aspects of this reform are now
settled --- it turned out more tricky than anticipated.
:black_small_square: As a future clarification of the session structure, session
sub-directories could be superseded by tags'' to group theories via
topics''. Thus the space of session-qualified theories would directly
correspond to the file-system arrangement, without the potential confusion
via duplicates in different sub-directories. The Prover IDE would present
tags via a suitable GUI presentation, e.g. a ``tag cloud'' instead of an
old-fashioned directory tree.
:black_small_square: A still pending reform is the intra-theory name space: it should the
∗‹long› theory name as prefix instead of the base name (e.g. (e.g.
▩‹HOL.Nat› instead of ▩‹Nat›). This would allow arbitrary merges of theories
across sessions without clashes. To get there, we need to accommodate tools
that impose their own interpretation on full names for entities (types,
consts, theorems etc.), notably traditional ‹Theory.locale.name› vs.
prospective ‹Session.Theory.locale.name›.
›
Find the minimal working example attached below.
Thank you for wrapping up the example nicely.
You can solve your particular problem by smashing the session-subdirectories:
the theory name space for each session is flat anyway.
Makarius
Email Gateway (Aug 23 2022 at 08:50):From: Tobias Nipkow <nipkow@in.tum.de>
I also ran into a problem. Some of the text for our book Concrete Semantics
(http://www.concrete-semantics.org/) comes from sessions in the distribution.
That is, running those sessions generates tex files that are included. However:
Theories that are imported from other sessions are excluded from the current
session document.
How to best deal with this situation?
Thanks
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:50):From: Makarius <makarius@sketis.net>
That is a quite different problem. Already from the beginnings of
session-qualified theory names in Isabelle2017, theories from other sessions
were excluded from the current session document.
The change in Isabelle2020 is that you can no longer "cheat" in this respect:
a directory (with its .thy files) "belongs" to a single session. You cannot
re-use the same files in different sessions.
To imitate the old behaviour for the book, you can try to work with
isabelle build -o document_output=DIR IMP
and include the generated .tex files into the session of the text book, using
a separate "isabelle build" invocation.
I did not find the book's sources, and can't say on the spot how this works
precisely.
Or you do copy the .thy files from the Isabelle distribution, to absorb them
into your book's session directory.
Makarius
Email Gateway (Aug 23 2022 at 09:24):From: Makarius <makarius@sketis.net>
Looking at this again, I found that your example was actually wrong, but the
error message too indirect to see it on the spot: a proper specification
"directories X" was missing in ROOT.
The change
https://isabelle-dev.sketis.net/rISABELLE4768b1facec2367417ff61d26011f37979b67505
in ongoing Isabelle development improves on that, although it is still unclear
how the situation in the next release will be in several months.
You can also see the error in Isabelle2020, if you restrict the selection to
session A of the example:
$ isabelle2020 build -d mwe_2020 A
*** Implicit use of directory "X" for theory "A.TheoryA"
*** Implicit use of session directories: "X"
*** The error(s) above occurred in session "A" (line 1 of
"/home/makarius/tmp/mwe_2020/ROOT")
Makarius
Last updated: Apr 25 2024 at 16:19 UTC