scala - '未定义常量 : "eq" simpdata. ML' 试图在 Isabelle/HOL 的 scala-isabelle 中加载 Imperative_Quicksort 理论

Question

我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle用于加载和解析 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html - Imperative_Quicksort.thy。我正在使用 IntelliJ 的 scala-isabelle 代码(源路径是 C:\Workspace-IntelliJ\scala-isabelle):

val isabelleHome = "C:\\Homes\\Isabelle2020\\Isabelle2020"
    // Differs from example in README: we skip building to make tests faster
    val setup = Isabelle.Setup(isabelleHome = Path.of(isabelleHome), logic = "HOL", build=false)
    implicit val isabelle: Isabelle = new Isabelle(setup)

    // Load the Isabelle/HOL theory "Main" and create a context object
    //val ctxt = Context("Main")
    //val ctxt = Context("Imperative_Quicksort")
    //val ctxt = Context("C:\\Homes\\Isabelle2020\\Isabelle2020\\src\\HOL\\Imperative_HOL\\ex\\Imperative_Quicksort")
    val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

这种配置会为加载一些必需的理论提供奇怪的错误消息，例如

Exception in thread "main" de.unruh.isabelle.control.IsabelleException: No such file: "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/Old_Datatype.thy"
The error(s) above occurred for theory "HOL-Library.Old_Datatype" (line 10 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/Countable.thy")
(required by "HOL.Imperative_HOL.ex.Imperative_Quicksort" via "HOL.Imperative_HOL.ex.Imperative_HOL" via "HOL.Imperative_HOL.ex.Array" via "HOL.Imperative_HOL.ex.Heap_Monad" via "HOL.Imperative_HOL.ex.Heap" via "HOL-Library.Countable")
    at de.unruh.isabelle.control.Isabelle.de$unruh$isabelle$control$Isabelle$$parseIsabelle(Isabelle.scala:268)

我的猜测是 - 使用引号导入的理论会给出此类错误消息，我通过将所需的理论复制到 C:\Workspace-IntelliJ\scala-isabelle 中来逐一解决此类错误消息。不好，但我正在尝试加载这个理论，所以 - 如果它有效，那就没问题了。
最后需要 simpldata.ML 但 Isabelle 源中有 5 个 simpdata.ML ( ZF / sequents / HOL/Tools / FOL / FOLP )。我从 FOL 复制(因为 FOL.thy 需要 simpdata.ML)但现在我有错误消息:

Exception in thread "main" de.unruh.isabelle.control.IsabelleException: Failed to load theory "ZF.Bool" (unresolved "ZF.pair")
...
Undefined constant: "eq" (line 12 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/simpdata.ML")completionline=12offset=313end_offset=315file=/cygdrive/c/Workspace-IntelliJ/scala-isabelle/simpdata.MLid=258:2:::IFOL.eq::constant:IFOL.eq::Pure.eq::constant:Pure.eq
At command "ML_file" (line 11 of "/cygdrive/c/Workspace-IntelliJ/scala-isabelle/pair.thy")
    at de.unruh.isabelle.control.Isabelle.de$unruh$isabelle$control$Isabelle$$parseIsabelle(Isabelle.scala:268)

我试图复制其他 simpldata.ML 但他们为不同的未定义常量提供了类似的消息。那么 - eq 有什么问题？我的猜测是这是非常基本的功能。
如何解决这个问题 undefined eq ?通过其他一些进口？但是 FOL/simpdata.ML 没有任何导入，也没有报告缺少某些源文件。如何从这里开始？
我的意图是将 Imperative_Quicksort 作为 Context scala-isabelle 变量加载，然后我将尝试反射(reflect)/消化生成的 Context 类树，我将使用图神经网络来编码这个类树(我想这是代表抽象语法树命令_快速排序理论)。
我知道有 Isabelle 邮件组，但这是一个非常技术性的问题，所以 - 它可以/应该在这里解决。
事实补充 1
simpdata.ML 只是包含在 FOL.thy 中的包含文件

ML_file \<open>simpdata.ML\<close>

因此， simpdata.ML 使用封闭 FOL.thy 文件的导入和定义，并且它确实具有 eq 定义(并且在 simpdata.ML 中使用之前大约有 100 行包括):

ML \<open>
  structure Blast = Blast
  (
    structure Classical = Cla
    val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
    val equality_name = \<^const_name>\<open>eq\<close>
    val not_name = \<^const_name>\<open>Not\<close>
    val notE = @{thm notE}
    val ccontr = @{thm ccontr}
    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
  );
  val blast_tac = Blast.blast_tac;
\<close>

所以，也许某些加载顺序存在问题......

Answer 1

似乎有 2 个理论文件(pair.thy 和 FOL.thy - 我已复制到我的 IntelliJ 工作区)使用了它们各自的 simpdata.ML 包含在各自的目录中。所以 - 我已经将 pair.thy 的 simpdata.ML 复制为 simpdata_pair.ML 并将 pair.thy 中的 include 命令修改为:

ML_file \<open>simpdata_pair.ML\<close>

这解决了我的问题，并允许我继续导入理论，这是一种有趣的方式。