isabelle

Bad session in Isabelle


I am trying to run Incompleteness from afp-2019-08-19 on Isabelle2023. When I open the ROOT file

chapter AFP

session Incompleteness (AFP) = HereditarilyFinite +
  description "The Incompleteness Theorems"
  options [timeout = 2400]
  sessions
    Nominal2
  theories
    Goedel_I
    Goedel_II
  document_files
    "root.bib"
    "root.tex"

I get the following errors:

Bad session "HereditarilyFinite"⌂ 
Bad session "Nominal2"⌂

Googling the error returned no useful results. Initially, I assumed that Isabelle cannot find the projects HereditarilyFinite and Nominal2, but they are in the same directory as Incompleteness. I probably just don't know how to search for/enable sessions, since no sessions defined with another session work. (Note: sessions defined with "HOL", "HOL-Light" and other presumably in-built sessions do work.)

This error seems strange to me, as I assumed that the downloaded AFP archive should work out-of-the-box.


Solution

  • An answer on the workings of isabelle components -u ... and imports in Isabelle can be found at https://proofassistants.stackexchange.com/questions/4225/bad-session-in-isabelle/4293#4293, where the same question has been asked.