[isabelle] Manual theory loading



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"
### theory "Draft.Test"
### 0.002s elapsed time, 0.002s cpu time, 0.000s GC time
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

Attachment: test.tgz
Description: application/compressed-tar



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.