Isabelle2023运行afp-2019-08-19中Incompleteness会话报错求助

尝试在Isabelle2023中运行afp-2019-08-19中的Incompleteness会话，其ROOT文件内容如下：

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"

运行时出现错误：

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

尽管HereditarilyFinite和Nominal2与Incompleteness在同一目录下，Isabelle仍无法识别，仅内置会话（如HOL、HOL-Light）可正常使用。

• 完整解压AFP归档
  不要单独提取Incompleteness子目录，将整个afp-2019-08-19归档解压到一个固定路径（例如/home/your-user/afp-2019），确保所有依赖的会话目录（HereditarilyFinite、Nominal2等）都在AFP根目录下。

• 配置Isabelle的AFP路径

  1. 打开Isabelle2023，点击菜单栏File > Isabelle Options
  2. 在General标签页找到AFP directory选项，填入你解压的AFP根目录路径
  3. 点击Apply保存设置，重启Isabelle生效

• 验证依赖并重建会话

  1. 确认HereditarilyFinite和Nominal2的ROOT文件存在且格式正确（比如HereditarilyFinite的ROOT应基于HOL会话定义）
  2. 打开Incompleteness的ROOT文件，点击工具栏的Build按钮（或快捷键Ctrl+B）重新构建会话

AFP会话并非独立可运行的单元，它们依赖整个AFP库的目录结构，且需要Isabelle明确知晓AFP根路径。即使依赖项与目标会话同目录，Isabelle默认只会搜索内置会话和已配置的库路径，因此必须通过配置AFP目录让Isabelle识别所有AFP会话。

内容的提问来源于stack exchange，提问作者God bless