Email Gateway (Aug 19 2022 at 17:03): Email Gateway (Aug 19 2022 at 17:03):From: Walther Neuper <wneuper@ist.tugraz.at>
Lars,
Thanks for private mail shortening my struggle with git. My response
times are still slow, because I'm busy with studies on scala and
respective project setup.
These studies became necessary because my trials with new operations in
libisabelle typecheck correctly, see
https://github.com/wneuper/libisabelle/commit/98206ed12423e7819f4df7f77e571c1450a6df71
but throw exceptions as soon as I try to return XML (test_2 and
Iterator, the latter not reached):
wneuper@ProBook:~/proto4/libisabelle$ java -cp full/target/scala-
2.11/libisabelle-full.jar Hello_PIDE
Hello world
--- test_1:
111
--- test_2:
###tracing val string: ts = toString...???
Exception in thread "main" isabelle.XML$XML_Body:
at isabelle.XML$Decode$$anonfun$9.apply(xml.scala:333)
at isabelle.XML$Decode$$anonfun$9.apply(xml.scala:328)
at edu.tum.cs.isabelle.japi.JSystem.sendCommand(System.scala:36)
at Hello_PIDE.main(Hello_PIDE.java:13)
^C
wneuper@ProBook:~/proto4/libisabelle$
My attempts with debugging are stuck presently:
(1) using the "more capable sbt" with tracing added to the scala code
would imho require a separate project for trials; after including
full/target/scala-2.11/libisabelle-full.jar
as a "Linked Resource" in the build path all trials with "import
XML.Encode._" etc (ERROR "not found object XML") fail.
(2) replacing the "more capable sbt" by code from the standard Scala
Build Tool for setup of a project in the Scala IDE was only partially
successful.
Looking at https://github.com/larsrh/libisabelle shows me, that your
work started without the "more capable sbt"; hints for the respective
project setup would be appreciated.
I'd rely on your choice, whether (1) or (2) is simpler to continue with.
In case of (1) a hint of how to import,
in case of (2) hints about setup of the Scala project ...
... both again out of scope of the mailing list, sorry
Cheers,
Walther
Email Gateway (Aug 19 2022 at 17:04):From: Lars Hupel <hupel@in.tum.de>
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 19 2022 at 17:17):From: Walther Neuper <wneuper@ist.tugraz.at>
https://github.com/wneuper/libisabelle, which causes an error.
The invocation of 'sendCommand' looks correct to me.
Good to hear of "looks correct", but there is need for debugging ...
wneuper@ProBook:~/proto4/libisabelle$ ./sbt full/assembly
[info] Loading project definition from
/home/wneuper/proto4/libisabelle/project
[info] Set current project to root (in build
file:/home/wneuper/proto4/libisabelle/)
[info] Compiling 3 Scala sources to
/home/wneuper/proto4/libisabelle/libisabelle/target/scala-2.11/classes...
[error]
/home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/System.scala:36:
Unmatched closing brace '}' ignored here
[error] }
[error] ^
[error]
/home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/System.scala:39:
expected start of definition
[error] private def mkPhaseListener(session: Session, phase:
Session.Phase)(implicit ec: ExecutionContext): Future[Unit] = {
[error] ^
[error]
/home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/System.scala:51:
expected start of definition
[error] private def sendOptions(session: Session, options:
Options)(implicit ec: ExecutionContext): Future[Unit] =
[error] ^
[error]
/home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/System.scala:56:
expected start of definition
[error] private def startSession(path: Option[Path], sessionName:
String)(implicit ec: ExecutionContext): Future[Session] = {
[error] ^
[error]
/home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/System.scala:74:
eof expected but '}' found.
[error] }
[error] ^
[error] 5 errors found
[error] (libisabelle/compile:compile) Compilation failed
[error] Total time: 6 s, completed 19-Feb-2015 1:48:19 PM
wneuper@ProBook:~/proto4/libisabelle$
... where this "more capable sbt" seems not the right tool: the error
System.scala:36: Unmatched closing brace '}'
cannot been cause System.scala:36 has not been changed. So, what could
be the error and how can I find another one myself next time ?
Walther
PS: And thank you for confirmation, what I hoped for:
How do you organize this kind of project involving Java, Scala and
Isabelle/ML ?
... for 'libisabelle' specifically I would recommend to just treat the
generated JAR file ('libisabelle-full.jar') as "just another dependency"
and drop it into some suitable folder of your usual Isac project
directory. There's no need to combine everything together into one big
project. Ideally, you wouldn't even change the source code of 'libisabelle'.
Email Gateway (Aug 19 2022 at 17:17):From: Lars Hupel <hupel@in.tum.de>
cannot been cause System.scala:36 has not been changed. So, what could
be the error and how can I find another one myself next time ?
I introduced that problem. Looks like I made a faulty commit which I
didn't test before pushing.
I corrected that error in 6949b35.
Cheers
Lars
Last updated: Apr 25 2024 at 12:23 UTC