Email Gateway (Aug 22 2022 at 10:47): Email Gateway (Aug 22 2022 at 10:47):From: Walther Neuper <wneuper@ist.tugraz.at>
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.
Email Gateway (Aug 22 2022 at 10:47):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
sorry for the noise ...
(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"
... Executing java at the appropriate directory works with absolute
paths now:
libisabelle$ java -jar /home/wneuper/proto4/dist/isac-java.jar
/home/wneuper/proto4/repos/isac-java/src/java/properties/BridgeMain.properties
However, now this question comes up:
Is there eventually a chance (if (1) or (2) are solved) to run our
application from Eclipse, if libisabelle is so sensible with respect to
paths?
PS: We are working on (1) and (2), because (3) forces to resign
debugging.
Cheers, Walther
Email Gateway (Aug 22 2022 at 10:47):From: Lars Hupel <hupel@in.tum.de>
... Executing java at the appropriate directory works with absolute
paths now:
libisabelle$ java -jar /home/wneuper/proto4/dist/isac-java.jar
/home/wneuper/proto4/repos/isac-java/src/java/properties/BridgeMain.properties
I suspect this can be solved by adapting the path in
JSystem sys = JSystem.instance(new File("."), "Protocol");
(instead of ".", use the appropriate path)
However, now this question comes up:
Is there eventually a chance (if (1) or (2) are solved) to run our
application from Eclipse, if libisabelle is so sensible with respect to
paths?
In principle, this should be possible. Environment variables in Java are
tricky, but luckily, Isabelle's Scala code allows setting the path in a
different way. I'll put it on my list.
Cheers
Lars
Last updated: Apr 25 2024 at 20:15 UTC