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.
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.