我正在尝试使用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-IntelliJscala-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-IntelliJscala-isabelle中复制所需的理论来逐一解决这样的错误消息。不太好，但我正在尝试加载这个理论，所以-如果它工作，它是好的。
在末尾simpldata。ML是必需的，但有5个简单数据。ML在Isabelle源(ZF / sequents / HOL/Tools / FOL / FOLP)。我从FOL复制(因为简单的数据。ML是必需的folo .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)
我试图复制其他简单数据。但是对于不同的未定义常量，它们给出了相似的信息。那么，eq有什么问题呢?我猜这是一个非常基本的功能。
如何解决这个undefined eq?是其他原因吗?但符合/simpdata。ML没有任何导入，也没有报告缺少一些源文件。从这里开始怎么走?
我的意图是加载Imperative_Quicksort作为上下文scala-isabelle变量，然后我将尝试反映/消化上下文的结果类树，我将使用图神经网络来编码这个类树(我认为这是代表Imperative_Quicksort理论的抽象语法树)。
我知道有Isabelle邮件组，但这是一个相当技术性的问题，所以-它可以/应该在so中解决。
事实添加1
simpdata。ML只是包含文件，包含在FOL中。你与
ML_file <open>simpdata.ML<close>
simpdata。ML使用封闭FOL的导入和定义。这个文件确实有eq定义(在simpdata中使用它之前大约有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>
所以，可能有些加载顺序有问题…
似乎2个理论文件(对)。你和FOL。(我已经复制到我的IntelliJ工作区)使用各自的simpdata。ML包含从它们各自的目录。我复制了simpdata。ML代表配对。这是simpdata_pair。ML和修改后的include命令成对使用。你:
ML_file <open>simpdata_pair.ML<close>
这解决了我的问题，并允许我以这种有趣的方式继续导入理论。