Stream: Beginner Questions

Topic: Document preparation: bad parent session

Hanna Lachnitt (Oct 27 2020 at 01:06):

When I use isabelle build -D . I get the following error message:

*** Bad parent session "Jordan_Normal_Form" for "My_Session" (line 1 of "/opt/afp-2020-09-19/thys/Isabelle_marries_Dirac/ROOT")

I have run:

echo "/opt/afp-2020-09-19/thys" >> ~/.isabelle/Isabelle2020/ROOTS

My root file looks like this:

session "My_Session" (AFP) = "Jordan_Normal_Form" +
  sessions
    Matrix_Tensor
  theories
     B
     C
     D
  document_files
    "root.tex"

Even if I use HOL instead of the parent directory Jordan_Normal_Form and move it to sessions, I get a Bad imports session error.

Mathias Fleury (Oct 27 2020 at 05:37):

Can you check with isabelle build -v -D . that the AFP theories are really found? The verbose option-v lists all sessions.

Mathias Fleury (Oct 27 2020 at 05:43):

In my case, I get

$ isabelle build -v -D .
Started at Tue Oct 27 06:41:42 GMT+1 2020 (polyml-5.8.1_x86_64_32-linux on archlinux)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/home/<redacted_user_name>/.isabelle/contrib/polyml-5.8.1-20200228/x86_64_32-linux"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session FOL/FOL
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Cardinals (timing)
Session HOL/HOL-Library (main timing)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Finger-Trees (AFP)
...

showing that the AFP is found.

Mathias Fleury (Oct 27 2020 at 05:57):

The path Isabelle_marries_Dirac looks a bit suspicious too. The more standard Isabelle way is Isabelle_Marries_Dirac (this matters only if you file system is case-sensitive...)

Hanna Lachnitt (Oct 29 2020 at 18:39):

Thank you, renaming Isabelle_marries_Dirac to Isabelle_Marries_Dirac solved the issue.

Last updated: Dec 21 2024 at 16:20 UTC