Email Gateway (Aug 22 2022 at 10:48): Email Gateway (Aug 22 2022 at 10:48):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
thank you very much for continuous support!
Having slept on your suggestionfor anight ...
... 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 inJSystem sys = JSystem.instance(new File("."), "Protocol");
(instead of ".", use the appropriate path)
... now I "suspect" we have understood the interdependencies between the
many paths in relation with the many tools (Java, sbt, Eclipse) and now
tell libisabelle-full.jar the path to the ROOT of Protocol ...
JSystem sys = JSystem.instance(new
File("/home/wneuper/proto4/libisabelle/."), "Protocol");
... and become free to run java from any directory "xxx" we want:
xxx$ java -cp
/home/wneuper/proto4/libisabelle/full/target/scala-2.11/libisabelle-full.jar
examples.src.main.java.Mini_Test
!!!!!!!!!!!!!!! THUS DEVELOPMENT WITHIN Eclipse BECOMES POSSIBLE,
because the paths are free now (to be set in some property file [1])
!!!!!!!!!!!!!!!
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.
Yeahhhhhh, one of the two obstacles for using Eclipse, the paths, is
removed. Now only the second obstacle, ISABELLE_HOME, is remaining:
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.
Setting ISABELLE_HOME via libisabelle would be **very helpful,
immediately** because our development appears to be too complicated [2]
to be done without Eclipse.
So each day setting ISABELLE_HOME would slide towards top on your list
would be highly appreciated!
Walther
[1] "examples.src.main.java.Mini_Test" is relative to
"libisabelle-full.jar". The "package examples.src.main.java" turned out
necessary for "import examples.src.main.java.ConvertXML" from isac-java.
ConvertXML.scala is located in the same directory with Mini_Test, which
could be changed, of course.
[2] The operation_setup for our minimal example reflects the Java-side,
which has not been designed for the present situation:
https://github.com/wneuper/libisabelle/blob/master/libisabelle/src/main/isabelle/Protocol/Protocol.thy
Last updated: Apr 29 2024 at 20:15 UTC