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



>    imports Complex_Main
> by imports "~~/src/HOL/Complex_Main"
> in Isac's sources.
> 
> Should we replace imports by "~~/..." in the Isabelle sources, too?
> Or: What are we doing wrong in [1]?

>From a brief glance at the build log, it appears that you first try to
build the "Protocol" session, but that one imports theories from Isac,
which in turn depends on HOL.

There are two ways to fix this: Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or move the
theory files from libisabelle to the Isac repository and list it in its
"src/Tools/isac/ROOT" file.

By the way, is there a reason why the Isac repository is a clone of
Isabelle? Have you considered pulling the specific parts out and
registering it as an Isabelle component (according to Â1.1.3 of the
system manual)?

Cheers
Lars




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