Email Gateway (Aug 19 2022 at 17:10): Email Gateway (Aug 19 2022 at 17:10):From: Lars Hupel <hupel@in.tum.de>
Dear list,
inspired by the obsoleted "tty" mode and a two-months old thread [1], I
decided to implement a proof-of-concept library demonstrating the
minimum amount of code needed to manage and communicate with an Isabelle
process. You can find the code at
<https://github.com/larsrh/libisabelle>
Right now this is just a weekend project, but I'm interested to hear
your opinions and feature requests, or if you have any use case for this.
Except for a working Isabelle installation (and ISABELLE_HOME set), the
code is self-contained. You can reproduce a round-trip between Java and
ML with the following instructions:
1) Build an image of "Hello_PIDE"
$ $ISABELLE_HOME/bin/isabelle build -d . -bv Hello_PIDE
2) Build the JAR file
$ ./sbt full/assembly
3) Execute the example
$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
What the above does is starting up an Isabelle instance, sending a
command, waiting for the reply, and tearing the instance down again. The
code to achieve that is just 3 lines of Java and some more lines of ML
and can be found in the 'examples' folder.
Right now, it supports the following:
Possible extensions include:
session management (invocation of 'isabelle build' ahead-of-time and
just-in-time)
support of multiple Isabelle versions (e.g. parallel operation of
Isabelle2014 and 2015)
Cheers
Lars
[1]
<http://article.gmane.org/gmane.science.mathematics.logic.isabelle.user/10011>
Email Gateway (Aug 19 2022 at 17:11):From: Walther Neuper <wneuper@ist.tugraz.at>
I decided to implement a proof-of-concept library demonstrating the
minimum amount of code needed to manage and communicate with an Isabelle
process. You can find the code at
Thank you very much for this extensive work, it promises the survival of
our project!
Your code presents lots of new stuff; I also studied system.pdf.
But I got stuck with this:
1) Build an image of "Hello_PIDE"
$ $ISABELLE_HOME/bin/isabelle build -d . -bv Hello_PIDE
which results in:
Started at Wed Feb 11 13:18:40 CET 2015 (polyml-5.5.2_x86-linux on ProBook)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
*** Duplicate session "RAW" (line 3 of "src/Pure/ROOT") (line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT")
Finished at Wed Feb 11 13:18:45 CET 2015
0:00:05 elapsed time, 0:00:04 cpu time
Renaming "RAW" in "pide-core/src/main/scala/Tools/build.scala" renaming
is no way out; so what can I do ?
Walther
Email Gateway (Aug 19 2022 at 17:11):From: Lars Hupel <hupel@in.tum.de>
Started at Wed Feb 11 13:18:40 CET 2015 (polyml-5.5.2_x86-linux on ProBook)
ISABELLE_BUILD_OPTIONS=""ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"*** Duplicate session "RAW" (line 3 of "src/Pure/ROOT") (line 3 of
"/usr/local/Isabelle2014/src/Pure/ROOT")
Finished at Wed Feb 11 13:18:45 CET 2015
0:00:05 elapsed time, 0:00:04 cpu time
This looks like a problem with your Isabelle installation. Can you build
anything at all? That is, if you go to some different folder (let's say,
$HOME) and invoke:
$ISABELLE_HOME/bin/isabelle build -bv HOL
Renaming "RAW" in "pide-core/src/main/scala/Tools/build.scala" renaming
is no way out; so what can I do ?
When building 'Hello_PIDE', none of the code in that repository is
actually being executed. What's more, everything in 'pide-core' is
basically copied verbatim from the official Isabelle distribution, so
changes in there shouldn't ever be necessary.
Cheers
Lars
smime.p7s
Email Gateway (Aug 19 2022 at 17:11):From: Walther Neuper <wneuper@ist.tugraz.at>
wneuper@ProBook:~$ /usr/local/Isabelle2014/bin/isabelle build -bv HOL
Started at Wed Feb 11 15:59:56 CET 2015 (polyml-5.5.2_x86-linux on ProBook)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86-linux"
ML_SYSTEM="polyml-5.5.2"
ML_OPTIONS="-H 500"
Session Pure/Pure
Session HOL/HOL (main)
Finished at Wed Feb 11 16:00:03 CET 2015
0:00:07 elapsed time, 0:00:17 cpu time, factor 2.42
... but doesn't that indicate, that the session Pure and HOL have
already been created successfully (actually, since months I'm working in
Isabelle2014 without problems)?
Many thanks for your help,
Walther
Email Gateway (Aug 19 2022 at 17:11):From: Lars Hupel <hupel@in.tum.de>
1) Build an image of "Hello_PIDE"
$ $ISABELLE_HOME/bin/isabelle build -d . -bv Hello_PIDE
Another shot in the dark: Did you issue that command while being in
$ISABELLE_HOME? That's the only reason I know of which could produce
that error message.
I should've been clearer, but the given steps are supposed to happen
while being in the checked-out copy of the repository.
Cheers
Lars
smime.p7s
Email Gateway (Aug 19 2022 at 17:11):From: Walther Neuper <wneuper@ist.tugraz.at>
the given steps are supposed to happen
while being in the checked-out copy of the repository.
Thanks a lot: from within the copy of the repository these steps ...
wneuper@ProBook:~/proto4/libisabelle$
/usr/local/Isabelle2014/bin/isabelle build -d . -bv Hello_PIDE
wneuper@ProBook:~/proto4/libisabelle$ ./sbt full/assembly
seem to have worked; I still have to study what extensive work these two
lines have accomplished.
But now I am stuck again with
wneuper@ProBook:~/proto4/libisabelle$ java -cp
full/target/scala-2.11/libisabelle-full.jar Hello_PIDE Exception in
thread "main" java.lang.RuntimeException: Unknown Isabelle home
directory at isabelle.Library$ERROR$.apply(library.scala:20) at
isabelle.Library$.error(library.scala:24) at
isabelle.Basic_Library$$anonfun$2.apply(library.scala:172) at
isabelle.Basic_Library$$anonfun$2.apply(library.scala:172) at
isabelle.Isabelle_System$.init(isabelle_system.scala:101) at
isabelle.Isabelle_System$.settings(isabelle_system.scala:56) at
isabelle.Isabelle_System$.getenv(isabelle_system.scala:137) at
isabelle.Isabelle_System$.getenv_strict(isabelle_system.scala:141) at
isabelle.Isabelle_System$.components(isabelle_system.scala:540) at
isabelle.Options$.init_defaults(options.scala:126) at
isabelle.Options$.init(options.scala:132) at
edu.tum.cs.isabelle.System$.startSession(System.scala:99) at
edu.tum.cs.isabelle.System$.instance(System.scala:16) at
edu.tum.cs.isabelle.japi.JSystem$.instance(System.scala:15) at
edu.tum.cs.isabelle.japi.JSystem$.instance(System.scala:18) at
edu.tum.cs.isabelle.japi.JSystem.instance(System.scala) at
Hello_PIDE.main(Hello_PIDE.java:8) wneuper@ProBook:~/proto4/libisabelle$
because I see that "libisabelle-full.jar" has been created at the right
place, because ISABELLE_HOME seems to be known
wneuper@ProBook:~/proto4/libisabelle$ /usr/local/Isabelle2014/bin/isabelle env
:
ISABELLE_HOME=/usr/local/Isabelle2014
and because I don't find the java argument "-cp" at
http://docs.oracle.com/javase/tutorial/essential/environment/cmdLineArgs.html
So once again: thank you very much for help!
Walther
Email Gateway (Aug 19 2022 at 17:12):From: Lars Hupel <hupel@in.tum.de>
seem to have worked; I still have to study what extensive work these two
lines have accomplished.
Not much, really: just building a tiny Isabelle session (whose only
purpose is to echo the input it receives) and then compiling some Scala
sources, producing a JAR file.
But now I am stuck again with
wneuper@ProBook:~/proto4/libisabelle$ java -cp
full/target/scala-2.11/libisabelle-full.jar Hello_PIDE Exception in
thread "main" java.lang.RuntimeException: Unknown Isabelle home
directory at isabelle.Library$ERROR$.apply(library.scala:20) at
This requires
$ export ISABELLE_HOME=/usr/local/Isabelle2014
because ISABELLE_HOME seems to be known
wneuper@ProBook:~/proto4/libisabelle$
/usr/local/Isabelle2014/bin/isabelle env
:
ISABELLE_HOME=/usr/local/Isabelle2014
The way 'ISABELLE_HOME' is determined is slightly tricky. As far as I
can tell, there are at least three ways:
1) when running Isabelle via the 'bin/isabelle' wrapper, in which case
the path is determined by the location of the wrapper
2) when starting Isabelle via PIDE, in which case the path is read from
the 'ISABELLE_HOME' environment variable
3) when starting Isabelle via PIDE, in which case the path can be
overriden via some internal mechanism
Right now, I'm using 2 but I really should be using 3.
and because I don't find the java argument "-cp" at
http://docs.oracle.com/javase/tutorial/essential/environment/cmdLineArgs.html
'-cp' tells Java where to find its class files. In this case, it just
consists of one JAR file.
Cheers
Lars
smime.p7s
Email Gateway (Aug 22 2022 at 09:19):From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,
after merging your last commit Apr.12 2015 from
https://github.com/larsrh/libisabelle
into our repository [1] we checked your and Makarius' suggestions about
development environments for Java / Scala / SML and now find it most
convenient to compile with your
$ $ISABELLE_HOME/bin/isabelle build -D . -bv
$ ./sbt
into *.jar (the former for the ML side and the latter for Java / Scala),
edit our files in Eclipse (Protocol.thy and Operation(s).scala for both
sides respectively), and execute Hello_PIDE.java from the command line
(with paths to respective *.jar). This setup seems sufficient for our
trials within libisabelle before integration into Isac.
For the above setup we can successfully transfer strings back and forth;
however we cannot figure out, how to return an XML.tree ---
--- could you, please, have a look at the last commit e3dd289
<https://github.com/wneuper/libisabelle/commit/e3dd289cde20e269a4dd1504f00309f407c5a1dc>
to [1]: there all compiles without errrors, because the questionable
operation is out-commented in all files.
Walther
[1] https://github.com/wneuper/libisabelle
Email Gateway (Aug 22 2022 at 09:20):From: Walther Neuper <wneuper@ist.tugraz.at>
On 2015-04-21 16:38, Walther Neuper wrote:
Hi Lars,
after merging your last commit Apr.12 2015 from
https://github.com/larsrh/libisabelle
into our repository [1] we checked your and Makarius' suggestions
about development environments for Java / Scala / SML and now find it
most convenient to compile with your$ $ISABELLE_HOME/bin/isabelle build -D . -bv
$ ./sbtinto *.jar (the former for the ML side and the latter for Java /
Scala), edit our files in Eclipse (Protocol.thy and Operation(s).scala
for both sides respectively), and execute Hello_PIDE.java from the
command line (with paths to respective *.jar). This setup seems
sufficient for our trials within libisabelle before integration into
Isac.For the above setup we can successfully transfer strings back and
forth; however we cannot figure out, how to return an XML.tree ---
[error] /home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/Operation.scala:14: type tree is not a member of object isabelle.XML
[error] val Iterator = implicitlyInt, XML.tree
[error] ^
i.e.: what type declaration is required here ?
--- could you, please, have a look at the last commit e3dd289
<https://github.com/wneuper/libisabelle/commit/e3dd289cde20e269a4dd1504f00309f407c5a1dc>
to [1]:there all compiles without errrors, because the questionable
operation is out-commented in all files.Walther
[1] https://github.com/wneuper/libisabelle
On 2015-02-24 11:56, Lars Hupel wrote:
but throw exceptions as soon as I try to return XML (test_2 and
Iterator, the latter not reached):
The reason why that fails is that by default, the 'sendCommand' function
tries to parse Isabelle's response as string. If you want the raw XML
block back, use 'sendCommandXML', which converts neither input nor
output.I'm not sure how convenient it would be to produce XML trees in Java. In
Scala, it would look like this:XML.Encode.int(222)
(This is completely symmetric to 'XML.Decode.int' in Isabelle/ML, which
you're already using.)Shot in the dark for Java:
isabelle.XML$.Encode$.int.apply(222);
I may need to add some convenience functions to make that more visually
pleasing.By the way, there should be no need to use 'XML.parse' in Isabelle/ML.
Instead, you can construct your response like this:XML.Elem (("CALCTREE", []),
[XML.Elem (("CALCID", []), [XML.Text "foo"])])Cheers
Lars
Email Gateway (Aug 22 2022 at 09:22):From: Lars Hupel <hupel@in.tum.de>
The Isabelle code looks correct (and indeed, it builds fine).
As for the Scala code, there are two problems, but they can be easily fixed:
Conceptually, an ML 'int' can have an arbitrary size, but a JVM 'Int' is
only 32 bits. Hence, it is modelled as a BigInt. Additionally, the
'XML.Tree' is uppercase.
I also guess that you're not going to need the 'ITERATOR' declaration in
the Java API, unless you want to use the Java API.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:24):From: Walther Neuper <wneuper@ist.tugraz.at>
Conceptually, an ML 'int' can have an arbitrary size, but a JVM 'Int' is
only 32 bits. Hence, it is modelled as a BigInt.
In Scala there is a conversion
apply(x:BigInteger): BigInt
but the error is thrown by arguments' type declaration -- how can we get
these right ?
Thanks again for help,
Walther
PS:
I also guess that you're not going to need the 'ITERATOR' declaration in
the Java API, unless you want to use the Java API.
right, so we can use the identifier "Iterator" for our own purposes.
Email Gateway (Aug 22 2022 at 09:24):From: Lars Hupel <hupel@in.tum.de>
The problem is a type mismatch ... the operation is declared for
'scala.math.BigInt', but you're trying to use it as a
'java.lang.BigInteger'. There should be no problem with consistently
using the former even in Java code, since the conversion is trivial:
scalaBigInt.bigInteger() // returns Java BigInteger
new scala.math.BigInt(javaBigInt) // constructs Scala BigInt
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:34):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
Thanks a lot for your help to get started with libisabelle ...
... which compiles a test perfectly [1] now.
In order to run the test in Hello_PIDE.java I'm looking for some
libisabelle*.jar.
Now I see, that the build has changed and libisabelle/full is empty; and
I couldn't find the target where ./sbt compiles to [2].
So I kindly ask once more for help to get started.
Walther
[1]
https://github.com/wneuper/libisabelle/commit/a957bc38bca645d602fd61137e732f93b3e410f1
[2] So far my best guess might be:
~/proto4/libisabelle$ java -cp
./libisabelle/target/resolution-cache/cs.tum.edu.isabelle/libisabelle_2.11
./examples/target/scala-2.11/classes/Hello_PIDE
Error: Could not find or load main class
..examples.target.scala-2.11.classes.Hello_PIDE
while we have:
~/proto4/libisabelle$ ls -l
./examples/target/scala-2.11/classes/Hello_PIDE.class
-rwxrw-r-- 1 wneuper wneuper 952 Apr 30 13:38
./examples/target/scala-2.11/classes/Hello_PIDE.class
Email Gateway (Aug 22 2022 at 09:45):From: Lars Hupel <hupel@in.tum.de>
Now I see, that the build has changed and libisabelle/full is empty; and
I couldn't find the target where ./sbt compiles to [2].
I didn't (consciously) change anything, but sometimes SBT is rather
mysterious ...
Try running './sbt full/assembly', it should produce a JAR file located
at 'full/target/scala-2.11/libisabelle-full.jar'. It also includes the
example:
$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
Hello world
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC