Re: [isabelle] libisabelle: which sbt ?

Makarius, Lars,

Thank you for help, and in particular thank you for the work which raised my help requests.

This work, a restricted version of PIDE, might be life-giving for various tools, which take advantage of knowledge mechanised within Isabelle without need to extend this knowledge from their side --- and for which restricting PIDE makes sense.

In charge of the isac-project I'm well motivated to contribute to making this work handy for everyone; presently I'm only able to ask questions, on a practical level "PIDE by example" and on a more theoretical level on "questions about PIDE architecture".

So I'll fork this mail thread into the above two "headlines" subsequently.


On 15-02-18 03:48 PM, Makarius wrote:
On Mon, 16 Feb 2015, Walther Neuper wrote:

 # A more capable sbt runner, coincidentally also called sbt.

Before I study this and also Scala Build Tool for Eclipse in order to select the most convenient way, I'd like to ask you:

How do you organize this kind of project involving Java, Scala and Isabelle/ML ?
Which project setup would you recommend ?

It depends which project management tool in the JVM world you like best, or understand, or are forced to use due to other side-conditions (e.g. the IDE).

Many years ago, I have once used the default "ant" setup for Netbeans projects, but it turned out inaccessible and unusable to non-experts of Netbeans. It is now a bit old-fashioned anyway.

Then I made a counter-movement away from JVM-based project management tools, just with minimalistic shell scripts around Isabelle tools. The latter is briefly documented in the "system" manual as follows:

section {* Scala compiler \label{sec:tool-scalac} *}

text {* The @{tool_def scalac} tool is a direct wrapper for the Scala
  compiler; see also @{tool scala} above.  The command line arguments
  are that of the underlying Scala version.

  This allows to compile further Scala modules, depending on existing
  Isabelle/Scala functionality.  The resulting class or jar files can
  be added to the Java classpath using the @{verbatim classpath} Bash
  function that is provided by the Isabelle process environment.  Thus
  add-on components can register themselves in a modular manner, see
  also \secref{sec:components}.

  Note that jEdit \cite{isabelle-jedit} has its own mechanisms for
  adding plugin components, which needs special attention since
  it overrides the standard Java class loader.  *}


On 15-02-18 09:11 PM, Lars Hupel wrote:
I also started to add an operation to be executed for test in, which causes an error.
Just had a quick look at the sources. What seems to be the problem? The
invocation of 'sendCommand' looks correct to me.

With debugging I run into questions about a comfortable project
setup. I see libisabelle/sbt with the comment

# A more capable sbt runner, coincidentally also called sbt.
The naming of that script is rather unfortunate. The "official" build
tool for Scala by Typesafe is "sbt", but it's not very easy to give
cross-platform instructions on how to set it up. The script you've been
looking at is also called "sbt" and is little more than a cross-platform
(well, except Windows) way to download and set up the actual build tool.
None of that is actually relevant for your main project, though, because ...

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'.


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