Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development. The manual for Isabelle/DOF 1.0.0/Isabelle2019 is available online.
As an alternative to installing Isabelle/DOF locally, the latest official release Isabelle/DOF is also available on Docker Hub. Thus, if you have Docker installed and your installation of Docker supports X11 application, you can start Isabelle/DOF as follows:
foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
logicalhacking/isabelle_dof-1.0.0_isabelle2019 isabelle jedit
Isabelle/DOF has two major pre-requisites:
In most case, the DOF-plugin can be installed as follows:
foo@bar:~$ ./install
If a specific Isabelle version should be used (i.e., not the default
one), the full path to the isabelle
command needs to be passed as
using the --isabelle
command line argument of the install
script:
foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020/bin/isabelle
For further command line options of the installer, please use the built-in help:
foo@bar:~$ ./install --help
A final step for the installation is:
foo@bar:~$ isabelle build -D .
This will compile Isabelle/DOF and run the example suite.
If you want to work with or extend one of the examples, e.g., you can open it similar to any standard Isabelle theory:
isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
This will open an example of a scientific paper using the pre-compiled
session Isabelle_DOF
, i.e., you will not be able to edit the
ontology definitions. If you want to edit the ontology definition,
just open the theory file with the default HOL session:
isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
While this gives you more flexibility, it might “clutter” your editing experience, as a lot of internal theories are loaded into Isabelle’s editor.
The DOF-plugin provides an alternative to Isabelle’s mkroot
command.
Isabelle projects that use DOF need to be created using
foo@bar:~$ isabelle mkroot_DOF
The mkroot_DOF
command takes the same parameter as the standard
mkroot
command of Isabelle. Thereafter, the normal Isabelle
command for building documents can be used.
Using the -o
option, different ontology setups can be
selected and using the -t
option, different LaTeX setups
can be selected. For example,
foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl
creates a setup using the scholarly_paper ontology and the article class from the KOMA-Script bundle.
The help (option -h
) show a list of all supported ontologies and
document templates:
foo@bar:~$ isabelle mkroot_DOF -h
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
Options are:
-h print this help text and exit
-n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: scholarly_paper)
Available ontologies:
* cenelec_50128
* mathex
* scholarly_paper
-t TEMPLATE (default: scrartcl)
Available document templates:
* lncs
* scrartcl
* scrreprt
* scrreprt-modern
Prepare session root DIR (default: current directory).
For releases, signed archives including a PDF version of the Isabelle/DOF manual are are available:
Main contacts:
This project is licensed under a 2-clause BSD license.
SPDX-License-Identifier: BSD-2-Clause
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff. Using The Isabelle Ontology Framework: Linking the Formal with the Informal. In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in Computer Science (11006), Springer-Verlag, 2018. doi:10.1007/978-3-319-96812-4_3.
Achim D. Brucker and Burkhart Wolff. Isabelle/DOF: Design and Implementation. In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science (11724), Springer-Verlag, 2019. doi:10.1007/978-3-030-30446-1_15.
Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification] (https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. doi:10.1007/978-3-030-34968-4_4
The master git repository for this project is hosted https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.