Stream: Beginner Questions

Topic: Theories in subdirectories

view this post on Zulip Hanno Becker (Aug 16 2023 at 05:12):

Hi all. Do subdirectories have to be associated with separate sessions? I tried organizing the theories of a session into multiple subdirectories, referencing them from the (single) ROOT file by means of their relative path. Isabelle/jEdit was happy with this, but a command line build failed with "Implicit use of FOO directory"...

view this post on Zulip Kevin Kappelmann (Aug 16 2023 at 06:22):

No, they don't need separate sessions. You should specify the directories that you use in your ROOT file. Say you have the following structure:

./
| My_Main.thy
| ROOT
|
|--Algebra
|        | Fractions.thy
|
|--Topology
         | Measures.thy

And assume that My_Main.thy contains the main results that you want to publish. Then your ROOT file should like like this:

session My_Session = "HOL" +
  directories
    "Algebra"
    "Topology"
  theories
    My_Main

view this post on Zulip Hanno Becker (Aug 28 2023 at 07:56):

Sorry for the late reply, Kevin. This solved my issue, thank you very much as usual :pray:

Last updated: Apr 27 2024 at 16:16 UTC