Stream: Beginner Questions

Topic: Isabelle Build Error: "Bad imports session" in ROOT file

view this post on Zulip Sana I. (Feb 06 2025 at 01:42):

I am working on a beginner Isabelle project and trying to build my session 'ProjectA'. However, I keep getting the following error when running 'isabelle build -D .':

Bad imports session "-" for "ProjectA" (line 1 of "~/ROOT")

I have checked my ROOT file in my directory named ProjectA, and it looks like this:

session ProjectA = HOL +
options [document = pdf]
sessions
HOL-Library
HOL-Algebra
HOL-Eisbach
theories
TheoryA
TheoryB
TheoryC

My questions:

  1. What does "Bad imports session '-'"mean in this context?
  2. Is there something wrong with my ROOT file?
  3. Should I change the directory structure?
  4. Is my AFP setup incorrect even though it shows up in ISABELLE_COMPONENTS?

view this post on Zulip Mathias Fleury (Feb 06 2025 at 05:53):

You need " around stuff with a -, exactly like in the imports in theory files

Last updated: Mar 09 2025 at 12:28 UTC