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.