Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ROOT file for imported theory

Email Gateway (Nov 12 2020 at 14:12):

From: Buday Gergely via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,

I import a theory from the HOL directory:

imports "~~/src/HOL/IMP/Big_Step"

and name it in the ROOT file:

session induction = HOL +
  options [document = pdf, document_output = "output"]
  theories [document = false]
    "~~/src/HOL/IMP/Big_Step"
  theories
    "Induction"
  document_files
    "root.tex" "build"

but then I get:

$ isabelle build -D .
*** Implicit use of directory
"/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP" for theory "induction.AExp"
*** Implicit use of directory
"/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP" for theory "induction.BExp"
*** Implicit use of directory
"/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP" for theory "induction.Com"
*** Implicit use of directory
"/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP" for theory
"induction.Big_Step"
*** Implicit use of session directories:
"/cygdrive/d/isabelle/Isabelle2020/src/HOL/IMP"

I get this even without mentioning the imported theory file in ROOT.

What shall I do?

I use Isabelle 2020.

• Gergely

Email Gateway (Nov 12 2020 at 14:37):

From: Jakub Kądziołka <kuba@kadziolka.net>
If I understand correctly, the correct way to include a dependency
outside of your session would be to do this:

sessions
"HOL-IMP"
theories [document = false]
"HOL-IMP.Big-step"

However, you might want to base your entire session on HOL-IMP instead
of just HOL. This will result in better caching;

session induction = "HOL-IMP" +
...

Regards,
Jakub Kądziołka

Email Gateway (Nov 13 2020 at 07:17):

From: Buday Gergely via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
11/12/2020 3:25 PM keltezéssel, Jakub Kądziołka írta:

Thanks for your help. At last it was enough to refer to the HOL-IMP
session in ROOT:

sessions

"HOL-IMP"

there was no need to name the imported theory.

The key step was to refer to the imported theory in my theory file via
the session name, not the file system path. When I entered Big_Step.thy
into my import clause, Isabelle/Jedit autocompleted it into
HOL-IMP.Big_Step. And it works:

imports "HOL-IMP.Big_Step"

Interestingly, when I based my session on "HOL-IMP" with

session induction = "HOL-IMP" +

and invoked

isabelle -c -D .

it started to rebuild HOL-Library which I really didn't want.

• Gergely

Last updated: Jan 04 2025 at 20:18 UTC