Isabelle：如果一个会话需要多个父会话怎么办？

Question

我开发了一套同时使用 Eisbach 和 HOL 库的理论。 Isabelle/jEdit 内一切正常。但是，当尝试使用 isabelle build 构建相应的会话时，找不到 Eisbach 和 HOL 库。过去，当我还不需要 HOL 库时，我通过在 ROOT 文件中指定 HOL-Eisbach 而不是 HOL 作为父会话来解决这个问题。由于需要 HOL 库，这一技巧不再有效，因为您不能拥有多个父会话。

如何构建同时使用 Eisbach 和 HOL 库的会话？

Answer 1

您可以在 ROOT 文件的 sessions 块中指定您的会话所依赖的其他会话，例如（取自法新社的例子）：

session Zeta_Function (AFP) = Dirichlet_Series +
  options [timeout = 600]
  sessions
    Euler_MacLaurin
    Bernoulli
  theories [document = false]
    "Dirichlet_Series.Dirichlet_Series_Analysis"
  theories
    Zeta_Function
  document_files
    "root.tex"

此会话有 Dirichlet_Series 个 parent 会话，另外还取决于会话 Euler_MacLaurin 和 Bernoulli。

那么您如何决定您的哪些依赖项应该是 parent 会话？嗯，请记住，为了构建您的会话，必须首先构建 parent 会话，但是一旦 parent 会话可用，您就可以直接使用它而无需额外费用。这就是为什么我们默认让事情依赖于 HOL：它通常可用 pre-built.

这也意味着如果您只使用它的一小部分，那么选择一个会话作为您的 parent 没有多大意义。这就是我避免选择 HOL-Library 作为 parent 会话的原因。通常，一个人只需要其中的一两个理论，可以在几秒钟内轻松处理，但是如果您选择它作为您的 parent，则用户必须构建 all 的 HOL-Library 才能使用您的会话。

所以，我会说你应该这样选择 parent：

列出您依赖的所有会话，并从中使用大量 material
选择该列表中最大的会话作为 parent

如果您最终得到的 parent 非常小（例如 HOL-Eisbach），您实际上不会从选择它作为 parent 中获得太多好处。你可以这样做，但你也可以选择HOL。

Isabelle：如果一个会话需要多个父会话怎么办？

Isabelle: What if a session needs more than one parent session?

isabelle