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

Question

I am trying to use 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. I am using scala-isabelle code from IntelliJ (path to source is 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")

Such configuration give strange error message for loading some required theories, e.g.

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)

My guess is - that theories that are imported using quotes give such error messages and I resolve such error messages one-by-one by copying the required theories in my C:\Workspace-IntelliJ\scala-isabelle. Not good, but I am trying to load this theory, so - if it works, it is fine.

At the end simpldata.ML was required but there are 5 simpdata.ML in Isabelle source (ZF / sequents / HOL/Tools / FOL / FOLP). I copied from FOL (because simpdata.ML was required by FOL.thy) but now I have error message:

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)

I tried to copy other simpldata.ML but they gave similar messages for different undefined constants. So - whats wrong with eq? My guess is that is is very basic function.

How to resolve this undefined eq? By some other import? But FOL/simpdata.ML does not have any imports and neither the lack of some source file is reported. How to proceed from here?

My intention was to load Imperative_Quicksort as the Context scala-isabelle varible, then I will try to reflect/digest the resulting class tree of Context and I will use graph neural networks to encode this class tree (I suppose that is represents the abstract syntax tree of Imperative_Quicksort theory).

I am aware that there is Isabelle mailing group but this is pretty technical question, so - it can/should be resolved here in SO.

Facts added 1

simpdata.ML is just include file which is included in FOL.thy with

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

So, simpdata.ML uses the imports and definitions of the enclosing FOL.thy file and it has eq definition indeed (and which is some 100 lines before its use in simpdata.ML include):

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>

So, maybe there are problems with some load order...

TomR TomR · Accepted Answer · 2021-03-05T23:46:55

It appeared that 2 theory files (pair.thy and FOL.thy - that I have copied to my IntelliJ workspace) used their respective simpdata.ML includes from their respective directories. So - I have copied simpdata.ML for pair.thy as simpdata_pair.ML and modified include command in pair.thy as:

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

This resolved my issue and allowed me to proceed with importing theory is this funny manner.

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

1 Answers