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



Hi Lars,

struggling with the error message

libisabelle$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE

Exception in thread "main" java.lang.RuntimeException: Duplicate session "RAW" (line 3 of "/usr/local/isabisac/src/Pure/ROOT") (line 3 of "/usr/local/isabisac/src/Pure/ROOT")

when following  your suggestionfor Hello_PIDE
   JSystem sys = JSystem.instance(new File("/path/to/isac"), "Isac");

I see now, that I did not completely understand your fix:
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.

My question now: There is something wrong with the sessions [1] ---
--- isn't there some kind of mirror of libisabelle/../ROOT required in isabisac (= Isabelle2014+Isac)?

Sorry not to be able to minimize the problem,
Walther


PS[1]: The error occurs in src/Pure/ROOT at "structure Distribution".
          If I add to isabisac/ROOTS
+ /home/wneuper/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol the error remains the same, while isabisac accepts this + without error.
           Etc ...

PS[2]: Summary of the situation:
# isabisac imports Protocol
https://intra.ist.tugraz.at/hg/isa/file/eeb0940e0329/src/Tools/isac/Build_Isac.thy#l54
# The settings of isabisac (Isabelle2014 + Isac) are correct now, I have solved
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-June/msg00122.html

# The libisabelle-side in the mail applies to ...
https://github.com/wneuper/libisabelle/commit/9e02c862175458867d492f3f0dd0aa7c79bd2d9f
# ... with respective updates:
  * session Protocol = (*Pure*) HOL +
  * Hello_PIDE:
      JSystem sys = JSystem.instance(new File("."), "Protocol");
JSystem sys = JSystem.instance(new File("/usr/local/isabisac"), "Isac");






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