[isabelle] libisabelle: embedding on Java-side



Hi Lars,

Since libisabelle's embedding works on the ML-side, we have turned to the Java-side.

Now we run into nasty situations for a while, give a report about our state (where we face obstacles from Eclipse (1) | Java coding (2)) and conclude with a question (3):

(0) Embedding libisabelle's initialisation into our isabisac/isac-java gives no syntax/semantics errors in Eclipse, if libisabelle-full.jar is included as a library in isabisac/isac-java:
   :
   import edu.tum.cs.isabelle.japi.JSystem;
   import edu.tum.cs.isabelle.japi.Operations;
   import isabelle.XML;
   import java.io.File;
   :
   JSystem sys = JSystem.instance(new File("."), "Protocol");
   :
The unsolved problem, however, is how to set ISABELLE_HOME for libisabelle:

(1) Eclipse provides isac-java > Run > Configurations > Environment:
    Variable: ISABELLE_HOME
    Value: /usr/local/isabisac
but running isac-java causes the error we already know from running Hello_PIDE:

Exception in thread "main" java.lang.RuntimeException: Unknown Isabelle home directory

(2) We still haven't found a way to "export ISABELLE_HOME=/usr/local/isabisac" from within Java code. The problem seems to be, that Java opens a new shell at any contact with the operating system; anyway, we always get the same error as in (1).

(3) Overcoming (1..2) we let Eclipse export to isac-java.jar and use the shell:
   isac-java$ export ISABELLE_HOME=/usr/local/isabisac
isac-java$ java -jar dist/isac-java.jar ./src/java/properties/BridgeMain.properties
     Starting Bridge...
Exception in thread "main" java.lang.RuntimeException: Bad session root directory: "/home/wneuper/proto4/repos/isac-java"

The message "Bad session root directory" comes from libisabelle/pide-core/../build.scala:

What does this message mean here, after libisabelle-full.jar has been created by ./sbt without errors ?

Cheers,
Walther


PS: We are working on (1) and (2), because (3) forces to resign debugging.





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