calculus-toolbox

A set of tools for generating calculi in Isabelle and supporting tools through a JSON description file

To try to make setting up the calculus toolbox as simple as possible, we now recommend installing the toolbox using Docker. Please install Docker for your platform and then follow the setup guide below.

Compiled toolboxes

If you just want to test out a toolbox GUI generated from a JSON description file, compiled toolboxes for the D.EAK calculus and a version of an LK Sequent calculus fragment are available as Scala JAR files (these have been tested on Linux and macOS):

• DEAK-calculus-tool
• Sequent-calculus-tool

Please ensure you have Java 8.0 or older and Scala 2.12.0 or older on your system. In order to launch the toolbox, run

scala DEAK.jar

or

scala Sequent.jar

Installing Docker

• macOS: For macOS, simply download the Docker CE desktop app and install it on your system.
• Ubuntu: Follow this guide to install Docker on Ubuntu
• Other Linux: Check the Docker documentation for install instructions for other Linux distributions.
• Windows 10: Download Docker CE for Windows and install it on your system. Please see the docs for further information on installing and using Docker on Windows.

Setup

First, download or fork this repository, then, inside the repo, run:

./run.sh

This script will download and compile all the dependencies and launch a sandboxed environment shell for building custom calculi toolboxes.

---

Windows

If on Windows, you will have to run the commands inside the bash script run.sh manually. First open PowerShell, navigate to the calculus-toolbox folder and run:

docker build -t calculus-toolbox .

Once the build is finished, launch the sandboxed shell by running:

docker run -ti -v %cd%/calculi:/root/calculi calculus-toolbox

---

The JSON description files can be found in the calculi folder and this also where you should save your own JSON description files. To build a calculus from a description file, simply run:

./build.py -c calculi/<your_json_file>.json

The JSON file will be compiled into the gen_calc folder. In order to generate a JAR file of the custom calculus toolbox, run the following commands:

cd gen_calc
./build
mv calc.jar ../calculi/calc.jar

To exit the Docker sandbox shell, press Control (Command on Mac) + D. In order to run the compiled JAR file, run:

scala calculi/calc.jar

(This is assuming that you have Java 8.0 or older and Scala 2.12.0 or older installed on your system)

For more information on how the toolbox works, head to the Introduction page.

OLD SETUP:

Get started

To get started, fork the github repository or download the project as a zip file and then head over to the Introduction page.

If you are using an older version of Isabelle (2014/2015), switch to the isabelle2015 branch via git checkout isabelle2015.

System requirements

To run the tools in the Calculus Toolbox, you need the following:

• Isabelle2016 (isabelle needs to be added to bash PATH) (if running Isabelle2014, please use the --isa2014 flag when compiling the calculus)
• Scala (preferred 2.10 or higher)
• Python (2.7 or higher)
• (optional) npyscreen and watchdog python modules