Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Session.Theory question

Email Gateway (Aug 22 2022 at 16:08):

From: Tobias Nipkow <nipkow@in.tum.de>
Take the following concrete example, session HOL-IMP in HOL. These days the ROOT
file says

session "HOL-IMP" (timing) in IMP = "HOL-Library" + ...

Everything works fine. But if I base IMP on HOL itself

session "HOL-IMP" (timing) in IMP = HOL +

I get

*** No such file: "/Users/nipkow/Isabelle2017/src/HOL/IMP/HOL-Library.Extended.thy"

because IMP imports HOL-Library.Extended. What do I need to change to make this
work? More generally: how do I import theories that are not in the image I build on?

Thanks
Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 16:08):

From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Dear Tobias,

Thanks for raising that question. I was asking that myself for my own
theory development and could not quickly find examples of ROOT files
in the AFP that just answered how to properly write ROOT files with
the new Isabelle version.

Lukas

Email Gateway (Aug 22 2022 at 16:08):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
As far as I understand, to import theories from sessions that are not
contained in the base image, you have to add a »sessions« declaration to
ROOT, e.g. in the case of IMP

session "HOL-IMP" (timing) in IMP = "HOL" +
options [document_variants = document]
sessions
"HOL-Library"
theories [document = false]

instead of

session "HOL-IMP" (timing) in IMP = "HOL-Library" +
options [document_variants = document]
theories [document = false]

Maybe the following analogy is helpful:

• Session dependencies form a DAG.
• Image dependencies form a spanning tree of that DAG.
• Hence there are main edges (given after »=«) and side edges (given
  after »sessions«)

Hope this helps,
Florian

Am 18.09.2017 um 12:01 schrieb Lukas Bulwahn:

Dear Tobias,

Thanks for raising that question. I was asking that myself for my own
theory development and could not quickly find examples of ROOT files
in the AFP that just answered how to properly write ROOT files with
the new Isabelle version.

Lukas

On Mon, Sep 18, 2017 at 11:55 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:

Take the following concrete example, session HOL-IMP in HOL. These days the
ROOT file says

session "HOL-IMP" (timing) in IMP = "HOL-Library" + ...

Everything works fine. But if I base IMP on HOL itself

session "HOL-IMP" (timing) in IMP = HOL +

I get

*** No such file:
"/Users/nipkow/Isabelle2017/src/HOL/IMP/HOL-Library.Extended.thy"

because IMP imports HOL-Library.Extended. What do I need to change to make
this work? More generally: how do I import theories that are not in the
image I build on?

Thanks
Tobias

signature.asc

Email Gateway (Aug 22 2022 at 16:08):

From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi Florian, hi others,

your hint resolved my issue, and I can build my theories again with a
ROOT file like this:

session MySession (AFP) = "HOL-Library" +
  sessions
     AFP_Session_1
     AFP_Session_2
...

Unfortunately, building the same theories with this ROOT file does not work:

session MySession (AFP) = "HOL" +
  sessions
     "HOL-Library"
     AFP_Session_1
     AFP_Session_2
...

It fails with:

*** exception THEORY raised (line 230 of "context.ML"):
*** Duplicate theory name
*** {..., Conditionally_Complete_Lattices, Binomial, Main,
Cancellation, HOL-Library.Multiset}
*** {..., Conditionally_Complete_Lattices, Binomial, Main,
Cancellation, MySession.Multiset}
*** At command "theory" (line 5 of "~/MyIsabelleTheories/SomeTheory.thy")

So there seems to be another constraint for composing the images,
sessions and theories that I am not yet aware of.

Best regards,

Lukas

Email Gateway (Aug 22 2022 at 16:08):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lukas,

Probably there is a mix of old-style path-based imports and new-style session-based
imports of some theory in HOL-Library. You should only use one style, otherwise the
theories will be loaded twice and you get the merge error.

Andreas

Email Gateway (Aug 22 2022 at 16:09):

From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi Andreas,

thanks for that further hint.

I had some old-style theory references in my ROOT file, such as:

theories
   "~~/src/HOL/Library/Theory1"
   "~~/src/HOL/Library/Theory2"
   "$AFP/Entry1/Theory1"

After replacing them by the new-style session-based names:

theories
   "HOL-Library.Theory1"
   "HOL-Library.Theory2"
   "Entry1.Theory1"

the build process now works fine.

By the way, there was no need to touch the theory files, but probably
I can now also clean them up with the new-style imports as well.

Lukas

Last updated: Apr 20 2024 at 04:19 UTC