Email Gateway (Aug 22 2022 at 10:48): Email Gateway (Aug 22 2022 at 10:48):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
while this makes very optimistic ...
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)
!!!!!!!!!!!!
we just found something not implemented with a path relative to
libisabelle: thus we'll face another problem when developing within Eclipse:
Run Configurations in Eclipse) as a library
libisabelle$ java -jar /home/wneuper/proto4/dist/isac-java.jar
/home/wneuper/proto4/repos/isac-java/src/java/properties/BridgeMain.properties
... which works, but changing the directory still raises an error:
/home/wneuper/proto4/dist/isac-java.jar
/home/wneuper/proto4/repos/isac-java/src/java/properties/BridgeMain.properties
Exception in thread "main" java.lang.RuntimeException: Bad session
root directory: "/home/wneuper/proto4" at
isabelle.Library$ERROR$.apply(library.scala:20)
So there seems to be something concerning session management in
libisabelle [1], which is not relative to the directory libisabelle, still.
Assuming the above is right, could you, please, look at it together with
ISABELLE_HOME ...
but luckily, Isabelle's Scala code allows setting the path in a
different way. I'll put it on my list.
With best wishes,
Walther
[1] This refers to
https://github.com/larsrh/libisabelle/commit/29bce1cdb2efe7d9f21e1a5d87f710299600c75f
and
https://github.com/wneuper/libisabelle/commit/cba0cf519d1d761a54144c2bca0cd0de478da0a6
Email Gateway (Aug 22 2022 at 10:50):From: Lars Hupel <hupel@in.tum.de>
Assuming the above is right, could you, please, look at it together with
ISABELLE_HOME ...but luckily, Isabelle's Scala code allows setting the path in a
different way. I'll put it on my list.
Try the following code (untested):
isabelle.Isabelle_System.init("/path/to/isabelle_home", "")
In your case, it would go right before the creation of the "JSystem"
instance. This should allow you to start your program without
ISABELLE_HOME set.
https://github.com/wneuper/libisabelle/commit/cba0cf519d1d761a54144c2bca0cd0de478da0a6
It looks like there is a typo in that file ... Did you really mean to use
/home/wneuper/proto4/libisabelle./
instead of
/home/wneuper/proto4/libisabelle/
?
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:50):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
thank you very much for continuous support!
Try the following code (untested):
isabelle.Isabelle_System.init("/path/to/isabelle_home", "")
In your case, it would go right before the creation of the "JSystem"
instance. This should allow you to start your program without
ISABELLE_HOME set.
Great, this worked immediately !!!
(to be precise: we don't get the error "Unknown Isabelle home directory"
any more; whether it works as intended will become evident when
continuing development now within Eclipse)
Thanks,
Walther
PS: you were right ...
It looks like there is a typo in that file ... Did you really mean to use
/home/wneuper/proto4/libisabelle./
... this works now with: /home/wneuper/proto4/libisabelle/.
Email Gateway (Aug 22 2022 at 11:06):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
since libisabelle's [1] usability is quite pleasing ...
..., it's embedding on the Isabelle/Isac-side is sufficient for the
present phase and the first step of embedding on the Java-side is done,
we give a summary of our experiences:
(1) Embedding on the Isabelle-side would benefit from libisabelle as an
Isabelle component: then one could drop the very specific ./sbt, which
enforces at least one absolute path in theory imports [2].
(2) Embedding on the Java-side benefits from the Scala IDE, which
smootly combines Java files and Scala files [3].
(3) Scala's pattern matching nicely handles transformation from XML.Tree
to Java Objects and vice versa [4, 5, 6].
And finally two questions:
(1) As you say, libisabelle is dedicated to "non-IDE applications" So
the synchronous Protocol makes sense. However, Isac is designed for an
asynchronous communication between Java frontend and the Isabelle/Isac
backend -- what are the obstacles to have libisabelle with asynchronous
communication?
(2) Could you, please, include an example in libisabelle, where you ship
a lambda-term through PIDE/xml in both directions ?
Eagerly awaiting libisabelle's new version running on Isabelle2015,
Walther
[1] https://github.com/larsrh/libisabelle
[2]
https://github.com/wneuper/libisabelle/blob/master/libisabelle/src/main/isabelle/Protocol/Protocol.thy#L3
[3]
https://intra.ist.tugraz.at/hg/isac/file/419b45750882/isac-java/src/java/isac/bridge/xml
[4]
https://intra.ist.tugraz.at/hg/isac/file/419b45750882/isac-java/src/java/isac/bridge/xml/DataTypes.scala
[5]
https://intra.ist.tugraz.at/hg/isac/file/419b45750882/isac-java/src/java/isac/bridge/xml/IsaToJava.scala
[6]https://intra.ist.tugraz.at/hg/isac/file/419b45750882/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala
Email Gateway (Aug 22 2022 at 11:07):From: Lars Hupel <hupel@in.tum.de>
Hi,
(1) Embedding on the Isabelle-side would benefit from libisabelle as an
Isabelle component: then one could drop the very specific ./sbt, which
enforces at least one absolute path in theory imports [2].
that is a good point which I haven't considered before. It will probably
not get rid of the './sbt' script but I can see how it would be useful in
general.
And finally two questions:
(1) As you say, libisabelle is dedicated to "non-IDE applications" So
the synchronous Protocol makes sense. However, Isac is designed for an
asynchronous communication between Java frontend and the Isabelle/Isac
backend -- what are the obstacles to have libisabelle with asynchronous
communication?
It is completely asynchronous internally. It uses a concept of "futures"
which is available in both ML [*] and Scala []. Simply speaking,
whenever a new operation is invoked from Scala, it is sent to the prover
asynchronously and processed by some thread in a worker farm.
The libisabelle Java API only appears to be synchronous because there,
I've added "barriers" which block on the results from the prover. By
switching to the Scala API, you could leverage concurrency and
parallelism. Java 8 supports a "future"-like concept now, so in principle
this arbitrary restriction could be dropped. In practice I haven't
investigated yet how good the interoperability between Java 8 and Scala is
in that regard.
Could you describe how the asynchronous communication worked previously in
Isac?
(2) Could you, please, include an example in libisabelle, where you ship
a lambda-term through PIDE/xml in both directions ?
What exactly do you mean here? An Isabelle term? Or are you talking about
an ML or a Scala function?
Eagerly awaiting libisabelle's new version running on Isabelle2015
Isabelle2015 support is there (for the Scala API), I just need to figure
out how to reconstruct Java support without breaking the previous API
much.
Lars
[*] See the introductory paragraphs in
<http://docs.scala-lang.org/sips/completed/futures-promises.html>
[**] Sec 3.1 in <http://www4.in.tum.de/~wenzelm/papers/itp-smp.pdf>
Last updated: Apr 19 2024 at 04:17 UTC