Email Gateway (Aug 22 2022 at 16:50): Email Gateway (Aug 22 2022 at 16:50):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm currently trying to figure out whether it is feasible to provide an
opentheory interface as a "pure Isabelle theory" (in the sense that it
can be loaded in a .thy file and doesn't require an external component).
Opentheory itself builds with Poly/ML just fine.
My first approach was to take all the source files that are listed in
the Makefile and turn them into a sequence of "SML_file ..." as
indicated in the reference manual.
Unfortunately, it doesn't quite work.
When I load the so-generated theory file, I can't access the hidden
"PolyML" structure.
My second approach was then to bundle everything into a "ROOT.ML" file
and load that from a theory file with "SML_file". This almost works:
When I open that "ROOT.ML" file in Isabelle/jEdit, I can see markup etc.
However, for the theory file, I get:
ML error (line 1 of "~/work/opentheory/opentheory/src/ROOT.ML"):
Value or constructor (SML_file) has not been declared
Here's the code (just the changes):
https://github.com/gilith/opentheory/compare/master...larsrh:topic/isabelle
Can be cloned from the "topic/isabelle" branch of
"https://github.com/larsrh/opentheory.git".
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:19):From: Lars Hupel <hupel@in.tum.de>
For posterity:
When I load the so-generated theory file, I can't access the hidden
"PolyML" structure.
The only required operation from "PolyML" is "pointerEq":
SML_import \<open>structure PolyML = struct val pointerEq = pointer_eq
end;\<close>
With that prefixed before loading the other files, it works. Makarius
figured this out.
Last updated: Apr 19 2024 at 08:19 UTC