sbt-libisabelle

Service Status
Travis (Linux/Mac CI) Build Status
AppVeyor (Windows CI) Build status
Gitter (Chat) Gitter

Usage

In your project/plugins.sbt, add this line:

// sbt 0.13.x
addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.5.1")

// sbt 1.0.x
addSbtPlugin("info.hupel" % "sbt-libisabelle" % "0.6.0")

To enable the plugin for a build, add this to your build.sbt:

enablePlugins(LibisabellePlugin)

Now, you can configure the following keys:

isabelleVersions := Seq("2016", "2016-1")
isabelleSessions in Compile := Seq("Example")

If unset, isabelleVersions defaults to the content of the environment variable ISABELLE_VERSION.

This allows you to put Isabelle source files (including ROOT) into src/main/isabelle. In the sbt shell, you can type isabelleBuild to build the Example session for both Isabelle2016 and Isabelle2016-1. Furthermore, you can use isabelleJEdit Example 2016 to open a jEdit instance with the Example session loaded.

The plugin also allows you to package and publish artifacts containing Isabelle sources as usual JAR files (with some metadata added).

Note that this plugin pulls in a dependency to sbt-assembly and configures a setting due to the way Isabelle artifacts are packaged.

Combined usage with libisabelle

The plugin does not add a compile-time dependency on libisabelle to your project. It only allows you to control Isabelle from within sbt. In case you want to use libisabelle's features (most likely you want to do that), you need to add this as a libraryDependency yourself. Look below for compatible versions.

You may also want to check out isabelle-irc-bot, which contains a full-blown demo project using both libisabelle and sbt-libisabelle.

Compatibility matrix

sbt-libisabelle version sbt versions libisabelle version Isabelle versions
0.4.x 0.13.x 0.6.x 2016
0.5.0 0.13.x 0.7.x – 1.0.x 2016, 2016-1
0.5.1 0.13.x, 1.0.x 0.7.x – 1.0.x 2016, 2016-1
0.6.0 1.0.x 0.7.x – 1.0.x 2016, 2016-1, Generic
0.6.1 1.0.x 0.7.x – 1.0.x 2016, 2016-1, 2017, Generic
0.7.0 (upcoming) 1.0.x 0.7.x – 1.0.x 2017, 2018 (upcoming), Generic

Generic means that arbitrary versions are supported (not on Windows), as long as they have a bin/isabelle executable. This is tested on Linux and macOS and should work with Isabelle since at least 2013.

sbt-libisabelle only requires the "generic" tier of Isabelle support from libisabelle. For runtime compatibility, refer to libisabelle's README.