Re: [isabelle] libisabelle: embedding on Java-side: ISABELLE_HOME



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 in

   JSystem 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




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