Re: [isabelle] libisabelle: embedding on ML-side WORKS



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.