1
$\begingroup$

This is a follow-up to ROOT file for building a heap image in Isabelle .

I have a main directory where my main theory resides. I have a ROOT file there:

session MAINSESSION = HOL +
  theories [document = false]
    MainTheory

and an app subdirectory from there with another ROOT file:

session APPLICATION = HOL + 
  sessions
     MAINSESSION
  directories 
     ".."
  theories [document = false]
     Application

Now, running

app$ isabelle build -v -D .

I get

*** Bad imports session "MAINSESSION" for "APPLICATION" (line 1 of "app/ROOT")

What is the problem here and how can I make this work?

$\endgroup$
0

1 Answer 1

1
$\begingroup$

The correct way to proceed seems to be declaring both your main session and the application in the same ROOT file at the main directory:

session MAINSESSION = HOL +
  theories [document = false]
    MainTheory

session APPLICATION in app = HOL + 
  sessions
     MAINSESSION
  theories [document = false]
     Application

The directories option does not seem to apply here, since it refers to “additional directories for import of theory files via theories within ROOT or imports within a theory”, as per the system manual.

In general, sessions sharing directories are apparently frowned upon.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.