Email Gateway (Aug 22 2022 at 10:20): Email Gateway (Aug 22 2022 at 10:20):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
thank you for your efforts to support bootstrapping Isabelle/Isac, where
bootstrapping systems usually involve specific efforts on unusual problems.
Just found one culprit for the confusion: isabisac/ROOTS contained
".../Protocol" from the various trials, and
libisabelle$ /usr/local/isabisac/bin/isabelle build -D . -bv
complained about that duplicate session.
########## AND NOW libisabelle WORKS ON THE ML-SIDE :
Anyway, maybe using "." as path instead of $ISABELLE_HOME works.
Right, with
JSystem.instance(new File("."), "Protocol");
and
theory Protocol
imports
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec"
"~~/src/Tools/isac/Frontend/Frontend"
we only have to suffer the absolute path to "Code". I hope we can live
with this during bootstrapping.
Now I see the arguments for establishing Isac an Isabelle component ...
It is a bit odd since you're including a "user-space" theory in a
"system-space" theory, but since all theories in an image are "equal"
regardless of their provenance, but conceptually, I don't see why this
shouldn't work.
I take it that "/usr/local/isabisac" contains the full Isabelle
distribution with added Isac? I was expecting that you would specify
just the subdirectory of the Isac component.
... where presently Isac is just inserted into the Isabelle code and not
separated as a component.
Before I look into Isabelle components I'm eager to see libisabelle
embedded on Java-side.
Thanks a lot,
Walther
Last updated: Apr 24 2024 at 01:07 UTC