Email Gateway (Aug 22 2022 at 17:30): Email Gateway (Aug 22 2022 at 17:30):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
I'm trying to update libisabelle to use qualified theory names. While
doing that, I noticed some odd behaviour.
Assume the following "ROOT" file:
session Test = Pure +
theories
"a/Test"
And the theory file "a/Test.thy":
theory Test imports Pure begin
end
$ isabelle console -d . -l Pure
Poly/ML> use_thy "Test.Test";
*** No such file: "/tmp/test/Test.thy"
*** The error(s) above occurred for theory "Test.Test"
Exception- TOPLEVEL_ERROR raised
Poly/ML> use_thy "a/Test";
Loading theory "Draft.Test"
val it = (): unit
I would expect both invocations to succeed. It becomes a problem when
there are two sessions, where one of them imports another one qualified.
I have attached an archive file with a small example:
Poly/ML> use_thy "b/Test2";
*** No such file: "/tmp/test/Test.thy"
*** The error(s) above occurred for theory "Test.Test" (line 1 of
"/tmp/test/b/Test2.thy")
*** (required by "Draft.Test2")
Exception- TOPLEVEL_ERROR raised
... and I'm not sure how I can make this work. Is this expected to work,
even?
(It appears this behaviour is identical in 2017 and 2018-RC0.)
Cheers
Lars
test.tgz
Email Gateway (Aug 22 2022 at 17:31):From: Lars Hupel <hupel@in.tum.de>
I would expect both invocations to succeed. It becomes a problem when
there are two sessions, where one of them imports another one qualified.
To answer my own question: It doesn't work with "isabelle console", but
it does work from Isabelle/Scala, by passing the "all_known = true" flag
when computing the session base.
Email Gateway (Aug 22 2022 at 17:31):From: Makarius <makarius@sketis.net>
all_known = true is the default in "isabelle jedit", but it can be very
slow when AFP is included.
all_known = false in "isabelle console", for reasons of minimality, but
it can lead into situations where certain qualified theory names are
inaccessible.
Instead of "all_known" there is a more recent parameter to specify
"include_sessions" in Isabelle/Scala. I will add options to the above
command-line tools to add sessions selectively: see the emerging
Isabelle2018-RC1.
Makarius
Last updated: Apr 20 2024 at 12:26 UTC