Isabelle/DOF
[maintained]

Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development.

Important Publications §

Isabelle/DOF: Document Preparation Setup

Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development. The manual for Isabelle/DOF 1.3.0/Isabelle2021-1 is available online.

Pre-requisites §

Isabelle/DOF has three major prerequisites:

Installation §

Isabelle/DOF is provided as an Isabelle component. After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this README.md file) and execute (if you executed this command already during the installation of the prerequisites, you can skip it now):

foo@bar:~$ isabelle components -u .

The final step for the installation is:

foo@bar:~$ isabelle build -D .

This will compile Isabelle/DOF and run the example suite.

Usage §

Opening an Example §

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.

Creating a New Project §

The DOF-plugin provides an alternative to Isabelle’s mkroot command. Isabelle projects that use DOF need to be created using

foo@bar:~$ isabelle dof_mkroot

The dof_mkroot 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 dof_mkroot -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 dof_mkroot -h

Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]

  Options are:
    -I           init Mercurial repository and add generated files
    -h           print help
    -n NAME      alternative session name (default: directory base name)
    -o NAMES     list of ontologies, separated by blanks
                 (default: "technical_report scholarly_paper")
    -q           quiet mode: less verbosity
    -t NAME      template (default: "scrreprt-modern")

  Create session root directory for Isabelle/DOF (default: current directory).

Releases §

For releases, signed archives including a PDF version of the Isabelle/DOF manual are available:

Older Releases §

Team §

Main contacts:

Contributors §

  • Idir Ait-Sadoune
  • Paolo Crisafulli
  • Chantal Keller
  • Nicolas Méric

License §

This project is licensed under a 2-clause BSD license.

SPDX-License-Identifier: BSD-2-Clause

Publications §

Upstream Repository §

The upstream git repository, i.e., the single source of truth, for this project is hosted at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.