'Undefined constant: "eq" simpdata.ML' 尝试在 Isabelle/HOL 的 scala-isabelle 中加载 Imperative_Quicksort 理论

Question

我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle for loading and parsing 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 来源 (ZF / sequents / HOL/Tools / FOL / FOLP) 中有 5 simpdata.ML。我从 FOL 复制（因为 simpdata.ML 是 FOL.thy 所要求的）但现在我收到错误消息：

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 作为上下文 scala-isabelle 变量，然后我将尝试 reflect/digest 上下文的结果 class 树，我将使用图形神经网络编码这个 class 树（我想它代表了 Imperative_Quicksort 理论的抽象语法树）。

我知道有 Isabelle 邮件组，但这是一个非常技术性的问题，所以 - 它 can/should 在 SO 中解决。

添加事实 1

simpdata.ML 只是包含在 FOL.thy 和

中的包含文件

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

所以，simpdata.ML 使用封闭的 FOL.thy 文件的导入和定义，它确实有 eq 定义（并且在之前大约 100 行它在 simpdata.ML 中的使用包括：

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 中的包含命令修改为：

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

这解决了我的问题，让我能够以这种有趣的方式继续导入理论。

'Undefined constant: "eq" simpdata.ML' 尝试在 Isabelle/HOL 的 scala-isabelle 中加载 Imperative_Quicksort 理论

'Undefined constant: "eq" simpdata.ML' while trying to load Imperative_Quicksort theory in scala-isabelle of Isabelle/HOL

scala

isabelle