Minimal wrapper around Isabelle/PIDE for non-IDE applications
Service | Status |
---|---|
Travis (Linux/Mac CI) | |
AppVeyor (Windows CI) | |
Codacy (code quality) | |
Maven Central | |
Scaladoc |
libisabelle
is a Scala library which talks to Isabelle.
It currently works with Isabelle2014 and Isabelle2015.
Experimental support for Isabelle2016-RC0 is available.
To get started, follow these steps:
- Run the
sbt
script to fetch all required Scala dependencies. After this is done, you are in the SBT shell. - Compile the sources with
compile
. - If you have used an arbitrary snapshot of the sources (e.g. via
git clone
), runpublishLocal
. - Bootstrap an Isabelle installation using
appBootstrap/run --version 2015
, which will download and extract the latest supported Isabelle version for you.
On some systems, you might need to install Perl, Python, and/or some additional libraries.
Note to proficient Isabelle users:
libisabelle
does not respect ISABELLE_HOME
.
Bootstrapping will create a new installation in your home folder (Linux: ~/.local/share
, Windows: %LOCALAPPDATA%
, OS X: ~/Library/Preferences
).
libisabelle
works on all platforms supported by Isabelle (Mac OS X, Linux, Windows).
It can either use an existing installation or bootstrap one (by downloading the appropriate archive from the Isabelle website).
Bootstrapping is automatically tested on all three platforms.
AppVeyor builds libisabelle
on Windows, but only bootstraps an Isabelle installation.
It does not run the integration tests (for now).
Run the sbt
script again, then, in the SBT shell, type test
.
This requires the environment variable ISABELLE_VERSION
to be set.
Another option is to pass the version to the test framework directly.
Example:
$ cd libisabelle
$ ./sbt
...
> testOnly * -- isabelle.version 2015
Make sure to have bootstrapped the installation as described above for the appropriate Isabelle version, otherwise the tests will fail.
The cli
application launches an Isabelle/jEdit instance with a specified logic.
$ cd libisabelle
$ ./sbt
...
> appCli/run --version 2015 HOL-Probability
By default, the HOL
session is selected.
The version has to be specified always.
libisabelle
is cross-built for Scala 2.10.x and 2.11.x.
Drop the following lines into your build.sbt
:
libraryDependencies ++= Seq(
"info.hupel" %% "libisabelle" % "0.2.2",
"info.hupel" %% "libisabelle-setup" % "0.2.2",
"info.hupel" %% "pide-interface" % "0.2.2"
)