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

>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: (1) Modify the "ROOT" file of your
libisabelle copy so that it uses "HOL" instead of "Pure", or (2) move the
theory files from libisabelle to the Isac repository and list it in its
"src/Tools/isac/ROOT" file.

We prefer (1), because we still want to keep apart libisabelle and Isac.
Your suggestion,

    -  session Protocol = Pure +
   + session Protocol = HOL +

however, again raises errors [1].

Another hint would be highly appreciated,

PS: Sorry for still not understanding completely how Isabelle manages file dependencies in sessions.

wneuper at wneuper-w541:~/proto4/libisabelle$ /usr/local/isabisac/bin/isabelle build -D . -bv Started at Mon Jun 15 18:36:24 CEST 2015 (polyml-5.5.2_x86-linux on wneuper-w541)


Session Pure/Pure
Session HOL/HOL (main)
Session Unsorted/Protocol
*** Incoherent imports for theory "Codec":
*** "/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec.thy" (file "/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy") *** "/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Codec.thy" (file "libisabelle/src/main/isabelle/Protocol/Codec_Test.thy") *** "libisabelle/src/main/isabelle/Protocol/Codec.thy" (file "/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy") *** "libisabelle/src/main/isabelle/Protocol/Codec.thy" (file "libisabelle/src/main/isabelle/Protocol/Codec_Test.thy") *** The error(s) above occurred in session "Protocol" (line 1 of "libisabelle/src/main/isabelle/Protocol/ROOT")
Finished at Mon Jun 15 18:36:26 CEST 2015
0:00:02 elapsed time, 0:00:06 cpu time

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