如何构建同时依赖Eisbach与HOL库的Isabelle会话？

嗨，这个问题其实很好解决——你可能没注意到，HOL-Eisbach本身就是基于HOL的扩展会话，它已经自动包含了HOL的所有依赖，所以根本不需要同时指定多个父会话。下面是具体的解决方案：

1. 正确配置ROOT文件 #

直接将你的会话父会话设置为HOL-Eisbach即可，它会自动继承HOL的所有理论，同时提供Eisbach库支持。一个典型的ROOT文件示例如下：

session My_Custom_Theory = HOL-Eisbach +
  options [document = false]  # 根据你的需求调整文档生成选项
  theories
    "My_Main_Theory"  # 这里替换成你的主理论文件名

2. 验证理论文件的导入 #

确保你的.thy理论文件中正确导入了所需模块，比如：

theory My_Main_Theory
imports
  HOL.Main  # HOL核心库（其实HOL-Eisbach已经默认包含，可省略）
  Eisbach.Eisbach  # Eisbach核心库
begin
(* 你的理论内容 *)
end

即使你不写HOL.Main，因为父会话是HOL-Eisbach，HOL的基础理论也会被自动加载。

3. 测试构建命令 #

在你的项目根目录（包含ROOT文件的目录）运行以下命令：

isabelle build -D .

这时候Isabelle会自动解析HOL-Eisbach的依赖链，加载HOL和Eisbach的所有库，不会再出现找不到库的问题。

补充说明 #

如果你好奇为什么HOL-Eisbach能同时覆盖两个库的需求，可以去Isabelle的安装目录下查看HOL-Eisbach/ROOT文件，里面的父会话就是HOL——也就是说它是HOL的超集，继承了HOL的所有内容并添加了Eisbach的扩展。

内容的提问来源于stack exchange，提问作者Wolfgang Jeltsch