Re: [isabelle] libisabelle: embedding on ML-side WORKS
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.
JSystem.instance(new File("."), "Protocol");
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
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and