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



Hi Lars,

since my last mail indicates, that there are principal questions about Isabelle's session management (and not with settings of isabisac (= Isabelle2014+Isac)), this question comes up:

Why not leave (PS(4))

   JSystem.instance(new File("."), "Protocol");

as it was originally and import from isabisac this way (PS(2,3))

   theory Protocol
   imports Codec "~~/src/Tools/isac/Frontend/Frontend"

???
Wouldn't that agree better with your advice (On 2015-06-15 10:54)

 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 [...]

Thank you very much for continuous support with the libisabelle component, which is so important for Isac.

Walther

PS the full procedere:
(1) export ISABELLE_HOME=/usr/local/isabisac  #= Isabelle2014+Isac
(2) theory Protocol
      imports Codec "~~/src/Tools/isac/Frontend/Frontend"
     (* "~~" refers to "/usr/local/isabisac" in (3), right? *)
(3) /usr/local/isabisac/bin/isabelle build -D . -bv
(4) edit Hello_PIDE:
       JSystem sys = JSystem.instance(new File("."), "Protocol");
//JSystem sys = JSystem.instance(new File("/usr/local/isabisac"), "Isac");
     //"isabelle build -D . -bv" imports from isabisac via (2)
(5) edit libisabelle/../ROOT:
     session Protocol = HOL +
(6) ./sbt full/assembly
(7) java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
     java -cp full/target/scala-2.11/libisabelle-full.jar Mini_Test

ad (3) however, as discussed in previous mails, this causes the error:

wneuper at wneuper-w541:~/proto4/libisabelle$ /usr/local/isabisac/bin/isabelle build -D . -bv Started at Mit Jun 24 08:30:46 CEST 2015 (polyml-5.5.2_x86-linux on wneuper-w541)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/isabisac/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"

*** Duplicate session "Protocol" (line 1 of "libisabelle/src/main/isabelle/Protocol/ROOT") (line 1 of "/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/ROOT")
Finished at Mit Jun 24 08:30:47 CEST 2015
0:00:01 elapsed time, 0:00:02 cpu time

Another question: How can one tell (3) about the relation to (5-6)? Wouldn't that be necessary?

Notes:
(a) both paths in the error message are correct:
"libisabelle/src/main/isabelle/Protocol/ROOT"
"/home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/ROOT"
(b) I see ISABELLE_BUILD_OPTIONS="" and continue investigations here.












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