Email Gateway (Aug 22 2022 at 09:50): Email Gateway (Aug 22 2022 at 09:50):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
thanks for continuous support with libisabelle, the wrapper around
Isabelle/PIDE for non-IDE applications [1].
Since a test example is successfully implemented [2], the next questions
are about embedding libisabelle into our application. Embedding concerns
2 sides, (1) our Java front-end and (2) our back-end in Isabelle.
The latter seems to be covered by libisabelle's operation USE_THYS,
which allows to determine the theories loaded in Isabelle.
With (1), however, we see a principal obstacle: Translation from Scala's
XML.Tree into Java objects requires import of the objects' definitions
(somewhere in libisabelle/examples).
These imports need to be handled by libisabelle/sbt such that the
objects are identified; but I am still unable to appropriately change
the respective code in sbt ---
--- can we get help here, or do we have to learn this from scratch?
Or do you see other possibilities (1a)?
Walther
(1a) Another possibility is to configure compilation in the Scala IDE,
but here we are only partially successful, too.
We still hope to finally use libisabelle-full.jar as a library for our
front-end, where the library knows as little as possible about the
front-end.
[1] https://github.com/larsrh/libisabelle
[2] https://github.com/wneuper/libisabelle
Email Gateway (Aug 22 2022 at 09:51):From: Lars Hupel <hupel@in.tum.de>
However, with (1) we see a principal obstacle: Translation from Scala's
XML.Tree into Java objects requires import of the objects' definitions
somewhere in libisabelle/examples.
The "examples" module already depends on all that, so importing that
should work, at least from Scala. From Java, the situation is more
difficult because of the intricacies of how Scala nested classes/objects
are being compiled to JVM class files.
(1a) Another possibility is to configure compilation in the Scala IDE,
but here we are only partially successful, too.
We still hope to finally use libisabelle-full.jar as a library for our
front-end, where the library knows as little as possible about the
front-end.
That is indeed the goal. Ideally, the 'libisabelle' sources should
remain unchanged and applications can just include that JAR file and add
operations, handlers, ...
If that doesn't work, something is wrong on my side. Does the full JAR
not include everything, or does Eclipse doesn't like it?
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:52):From: Walther Neuper <wneuper@ist.tugraz.at>
On 2015-05-18 10:25, Lars Hupel wrote:
However, with (1) we see a principal obstacle: Translation from Scala's
XML.Tree into Java objects requires import of the objects' definitions
somewhere in libisabelle/examples.
The "examples" module already depends on all that, so importing that
should work, at least from Scala. From Java, the situation is more
difficult because of the intricacies of how Scala nested classes/objects
are being compiled to JVM class files.
Right, that works all perfectly and is more or less transparent for us.
My question was more general:
Translation Scala's XML.Tree <---> Isac's Java objects directly in a
Scala file (near libisabelle/examples), which would require imports of
the objects in the Scala file ---
--- and these imports can only be resolved if sbt sets some additional
paths.
So we presently decompose Isac's Java objects, transfer the primitve
datatypes, compose to XML.Tree (and the same back again); direct
translation within one method for one direction would be more concise.
Would it be possible to extend sbt such that is can take such additional
paths???
We still hope to finally use libisabelle-full.jar as a library for our
front-end, where the library knows as little as possible about the
front-end.
That is indeed the goal. Ideally, the 'libisabelle' sources should
remain unchanged and applications can just include that JAR file and add
operations, handlers, ...If that doesn't work, something is wrong on my side. Does the full JAR
not include everything, or does Eclipse doesn't like it?
libisabelle-full.jar does all what we want: if given to Eclipse,
respective imports work and we have IDE feedback in coding.
Thanks,
Walther
Email Gateway (Aug 22 2022 at 10:11):From: Lars Hupel <hupel@in.tum.de>
Hi,
when the prover is loaded with a particular session (in your case, it's
probably the session defined in 'libisabelle'), you can't change it
later. You can only load further theories.
However, you can easily start up the prover with a combined session of
all the things you need. You need to make sure that your modified
'Protocol.thy' is included in your 'ROOT' file (either via a theory
import or by listing it explicitly) and then use:
JSystem sys = JSystem.instance(new File("/path/to/isac"), "Isac");
Cheers
Lars
Last updated: Apr 30 2024 at 16:19 UTC