Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] libisabelle: which sbt ?


view this post on Zulip Email Gateway (Aug 19 2022 at 17:15):

From: Walther Neuper <wneuper@ist.tugraz.at>
Hi Lars,

Thank you for help, libisabelle says "hello world". I also started to
add an operation to be executed for test in
https://github.com/wneuper/libisabelle, which causes an error.

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.

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 ?

Walther

PS: We have the Java-part of isac in Eclipse since ever and I now have
started with Scala IDE for Eclipse.

view this post on Zulip Email Gateway (Aug 19 2022 at 17:16):

From: Makarius <makarius@sketis.net>
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. *}

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 17:16):

From: Lars Hupel <hupel@in.tum.de>

I also started to add an operation to be executed for test in
https://github.com/wneuper/libisabelle, 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'.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 17:17):

From: Walther Neuper <wneuper@ist.tugraz.at>
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.

Walther


Last updated: Apr 26 2024 at 20:16 UTC