Re: [isabelle] libisabelle: embedding on ML-side
struggling with the error message
libisabelle$ java -cp full/target/scala-2.11/libisabelle-full.jar
Exception in thread "main" java.lang.RuntimeException: Duplicate
session "RAW" (line 3 of "/usr/local/isabisac/src/Pure/ROOT") (line 3 of
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)
theory files from libisabelle to the Isac repository and list it in its
We prefer (1), because we still want to keep apart libisabelle and Isac.
My question now: There is something wrong with the sessions  ---
--- isn't there some kind of mirror of libisabelle/../ROOT required in
isabisac (= Isabelle2014+Isac)?
Sorry not to be able to minimize the problem,
PS: The error occurs in src/Pure/ROOT at "structure Distribution".
If I add to isabisac/ROOTS
the error remains the same, while isabisac accepts this +
PS: Summary of the situation:
# isabisac imports Protocol
# The settings of isabisac (Isabelle2014 + Isac) are correct now, I have
# The libisabelle-side in the mail applies to ...
# ... with respective updates:
* session Protocol = (*Pure*) HOL +
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