Isabelle_DOF/Isabelle_DOF
0
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting as well as formal development.
2,124 Commits 20 Branches 11 Tags 78 MiB
Isabelle 56%
TeX 42.3%
Scala 0.9%
Shell 0.8%
Isabelle_DOF-Zenodo-2025
Go to file
Achim D. Brucker d9457d4fde Fixed Isabelle version in heading.
2025-04-24 09:07:51 +01:00
Isabelle_DOF-add_ons-2025 Fixed Isabelle version in heading. 2025-04-24 09:07:51 +01:00
Isabelle_DOF-Scaffold-2025 Restructured archive. 2025-03-16 18:49:42 +00:00
Isabelle_DOF-2025.pdf Initial commit. 2025-04-24 08:17:31 +01:00
README.md Fixed Isabelle version in heading. 2025-04-24 09:07:51 +01:00

README.md

Isabelle/DOF 2025 Add-Ons

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

This repository contains add-ons to the Isabelle/DOF core package available in the Archive of Formal Proofs (AFP). In particular, the following add-ons are provided:

  • Additional document ontologies and LaTeX templates (in the session Isabelle_DOF-Ontologies).
  • Additional examples using various Ontologies and LaTeX template.
  • A tool for creating new Isabelle/DOF projects (isabelle dof_mkroot).

These add-ons are provided in the archive Isabelle_DOF-add_ons-2025.tar.xz. Additional, this entry contains a scaffold that allows for easily starting a new project with the version of Isabelle/DOF provided in the AFP (i.e., without the add ons installed). This scaffold is provided in the archive Isabelle_DOF-Scaffold-2025.

Pre-requisites

Isabelle/DOF has two major prerequisites:

Installation

Installation of Isabelle

Please download Isabelle 2025 from the Isabelle Website and follow the system specific instructions for its installation.

Installation from the Archive of Formal Proofs (AFP)

The core of Isabelle/DOF is available in the AFP. Hence, for using the Isabelle/DOF Add-Ons package, please install the AFP for Isabelle 2025 following the instructions given at https://www.isa-afp.org/help.html. In the following, we assume that the AFP has been registered as Isabelle component.

Isabelle/DOF is provided as one AFP entry:

  • Isabelle_DOF: This entry contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.

Isabelle/DOF Add-Ons

Unpack the archive Isabelle_DOF-add_ons-2025.tar.xz and change into the directory containing the content of the archive. In this directory, execute the following command to register these add-ons as Isabelle components:

foo@bar:Isabelle_DOF-add_ons-2025$ isabelle components -u .

for building the standard session of Isabelle/DOF, execute the following command:

foo@bar:~$ isabelle build -D . -x Isabelle_DOF-Proofs -x HOL-Proofs

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

For building the session Isabelle_DOF-Proofs, the timeout might need to be increased to avoid timeouts during building the dependencies:

foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs

Usage

Assuming that your current directory contains the example academic paper in the subdirectory Isabelle_DOF-Example-I/, you can open it similar to any standard Isabelle theory:

isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-I/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 default ontologies defined in the Isabelle_DOF session. If you want to edit the ontology definition, just open the theory file with the session Functional-Automata:

isabelle jedit -l Functional-Automata Isabelle_DOF-Example-I/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).

Directory Structure of the Isabelle/DOF Add-Ons Archive

The Isabelle/DOF Add-Ons Archive is structured into several Isabelle sessions, each of which is stored in a subdirectory:

  • Isabelle_DOF: This is the main session, providing the Isabelle/DOF system. Furthermore, this session is currently under consideration for a submission to the AFP.
  • Isabelle_DOF-Example-I: This session provides an example document written Isabelle/DOF. It only requires the core ontologies provided by the Isabelle_DOF session. Furthermore, this session is currently under consideration for a submission to the AFP.
  • Isabelle_DOF-Ontologies: This session provided additional ontologies and document templates.
  • Isabelle_DOF-Unit-Tests: This session includes various tests for the Isabelle/DOF system, partly depending on the ontologies provided by the Isabelle_DOF-Ontologies session.
  • Isabelle_DOF-Examples-Extra: This directory contains additional example documents written using the Isabelle/DOF systems, each of which is defined in an own subdirectory.
  • Isabelle_DOF-Proofs: This session provides the Isabelle/DOF systems with proof objects. This is required for the deep ontology embedding.

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, containing the latest development version (and the the single source of truth), for this project is hosted at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.