Email Gateway (Aug 22 2022 at 17:06): Email Gateway (Aug 22 2022 at 17:06):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I was wondering whether there was any official (and non-workaround) way
to find out the "minimal" session qualifier for an imported theory.
For example:
Say theory A is part of some huge Isabelle project that has a ROOT file
(in session directory $D) with many sessions (S1, ..., SN) and
furthermore, A is not mentioned explicitly in the ROOT file but is just
some implicit dependency of one of the sessions.
Now I have a theory file B.thy containing:
theory B
imports "$D/A"
begin
end
and would like to replace the import by a qualified one.
However, as I said I do not (without spending some effort and lots of
build time) know which session A belongs to.
Assuming SN is the final session in the hierarchy, I could probably just
build SN then "imports A" and afterwards Ctrl-Click on A to get the
qualifier (not sure whether this really works)?
But is there an easy/fast way to find out which Si is the first one in
which A is present so that I end up with
theory B
imports Si.A
begin
end
without actually building anything and without having to manually
inspect theory files?
cheers
chris
Email Gateway (Aug 22 2022 at 17:46):From: Makarius <makarius@sketis.net>
When doing the conversion for Isabelle + AFP for the Isabelle2017
release, I used "isabelle imports" a lot, as sketched in NEWS and the
"system" manual.
In the forthcoming Isabelle2018 release, the rules for qualified theory
names are more strict: unqualified import from the parent session is no
longer allowed. This could make the conversion more difficult -- or
sometimes easier, because there is only one way to do it.
I am still not fully satisfied with the situation in Isabelle2018: maybe
the import scheme needs to become even more strict, and insist that
theory files reside exactly in the session directory (no
sub-directories, no outside directories). One could still allow for
exceptions that are specifies in the session ROOT entry of 'theories'.
The latter scheme would also speed-up the inversion of file-names to
session-qualified theory names in the Prover IDE: presently one can wait
0.5 .. 1.5 min for that (esp. for AFP).
Makarius
Last updated: Apr 19 2024 at 12:27 UTC