4.2 KiB
Isabelle/DOF: Instructions on Using the Development Version
Pre-requisites
Isabelle/DOF has three major prerequisites:
- Isabelle: Isabelle/DOF requires Isabelle 2022. Please download the Isabelle 2022 distribution for your operating system from the Isabelle website.
- AFP: Isabelle/DOF requires several entries from the Archive of Formal Proofs (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 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 . -x Isabelle_DOF-Proofs -x HOL-Proofs
This will compile Isabelle/DOF and run the example suite.
Usage
Overall, the use of the development version follows the description available for the AFP version. Hence, for details please consult the Isabelle/DOF manual.
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).