Isabelle/DOF: Document Preparation Setup

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.2.0/Isabelle2021 is available online.

Pre-requisites

Isabelle/DOF has three major pre-requisites:

• Isabelle: Isabelle/DOF requires Isabelle 2021-1. Please download the Isabelle 2021-1 distribution for your operating system from the Isabelle website.
• AFP: Isabelle/DOF requires two entries from the Archive of Formal Proofs (AFP). Please install the AFP following the instructions given at https://www.isa-afp.org/using.html. For your convenience, we also provide a script that only installs the two entries required by Isabelle/DOF into the local Isabelle/DOF directory. You can use this script as follows:

  foo@bar:~$ isabelle env ./install-afp
  

• LaTeX: Isabelle/DOF requires a modern LaTeX installation, i.e., at least TeX Live 2022 with all available updates applied.

Installation

Isabelle/DOF is provided as a Isabelle component. After installing the pre-requisites the Isabelle/Archive needs to be unpacked and registered. Change into the directory you unpacked Isabelle/DOF (this should be the directory containing this README.md file) and execute

foo@bar:~$ isabelle components -u `pwd`

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 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).

Releases

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

• Isabelle/DOF 1.2.0/Isabelle2021
  • Isabelle_DOF-1.2.0_Isabelle2021.pdf
  • Isabelle_DOF-1.2.0_Isabelle2021.tar.xz
  • Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc
• Isabelle/DOF 1.1.0/Isabelle2021
  • Isabelle_DOF-1.1.0_Isabelle2021.pdf
  • Isabelle_DOF-1.1.0_Isabelle2021.tar.xz
  • Isabelle_DOF-1.1.0_Isabelle2021.tar.xz.asc
• Isabelle/DOF 1.1.0/Isabelle2020
  • Isabelle_DOF-1.1.0_Isabelle2020.pdf
  • Isabelle_DOF-1.1.0_Isabelle2020.tar.xz
  • Isabelle_DOF-1.1.0_Isabelle2020.tar.xz.asc
• Isabelle/DOF 1.0.0/Isabelle2019
  • Isabelle_DOF-1.0.0_Isabelle2019.pdf
  • Isabelle_DOF-1.0.0_Isabelle2019.tar.xz
  • Isabelle_DOF-1.0.0_Isabelle2019.tar.xz.asc

Team

Main contacts:

• Achim D. Brucker
• Burkhart Wolff

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

• 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. In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. doi:10.1007/978-3-030-34968-4_4

• Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. Making Agile Development Processes fit for V-style Certification Procedures. In ERTS 2018. https://hal.archives-ouvertes.fr/hal-01702815

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.