伊莎贝尔的糟糕会议

Question

我正在尝试在 Isabelle2023 上从

Incompleteness

运行

afp-2019-08-19

。当我打开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"⌂

谷歌搜索错误没有返回有用的结果。最初，我假设 Isabelle 找不到项目

HereditarilyFinite

和

Nominal2

，但它们与

Incompleteness

位于同一目录中。我可能只是不知道如何搜索/启用会话，因为使用另一个会话工作定义的no会话。 （注意：使用

"HOL"

、

"HOL-Light"

定义的会话以及其他可能内置的会话确实有效。）

这个错误对我来说似乎很奇怪，因为我认为下载的法新社档案应该开箱即用。

Answer 1

有关

isabelle components -u ...

工作原理的答案可以在 https://proofassistants.stackexchange.com/questions/4225/bad-session-in-isabelle/4293#4293 找到，其中也提出了同样的问题。