2018-06-12 22:28:20 +00:00
|
|
|
# Isabelle/DOF: Document Preparation Setup
|
2018-02-07 17:43:15 +00:00
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
Isabelle/DOF is a novel Document Ontology Framework on top of
|
|
|
|
Isabelle. Isabelle/DOF allows for both conventional typesetting as
|
|
|
|
well as formal development.
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2019-01-05 22:32:17 +00:00
|
|
|
## Prerequisites
|
|
|
|
|
|
|
|
### Isabelle 2017
|
|
|
|
|
|
|
|
Isabelle/DOF requires [Isabelle 2017](http://isabelle.in.tum.de/website-Isabelle2017/).
|
|
|
|
Please download the Isabelle 2017 distribution for your operating
|
|
|
|
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2017/).
|
|
|
|
|
|
|
|
After unpacking the Isabelle distribution, replace the file
|
|
|
|
``Isabelle2017/src/Pure/Thy/thy_output.ML`` in the Isabelle
|
|
|
|
distribution with the file ``patches/thy_output.ML`` from the
|
|
|
|
Isabelle/DOF distribution:
|
|
|
|
|
|
|
|
```console
|
|
|
|
cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/
|
|
|
|
```
|
|
|
|
|
|
|
|
### AFP Entries
|
|
|
|
|
|
|
|
Moreover, Isabelle/DOF requires the two entries from the Archive of
|
|
|
|
Formal Proofs. Please download the [AFP for Isabelle
|
|
|
|
2017](https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz")
|
|
|
|
and follow the [instructions for installing the AFP as Isabelle
|
|
|
|
component](https://www.isa-afp.org/using.html). If you have extracted
|
|
|
|
the AFP archive into the directory to `/home/myself/afp`, you should
|
|
|
|
run the following command to make the AFP session `ROOTS` available to
|
|
|
|
Isabelle:
|
|
|
|
|
|
|
|
```console
|
|
|
|
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2018/ROOTS
|
|
|
|
```
|
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
## Installation
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
In most case, the DOF-plugin can be installed as follows:
|
|
|
|
```console
|
|
|
|
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
|
|
|
|
argument to the ``install`` script:
|
|
|
|
```console
|
2018-12-06 17:38:15 +00:00
|
|
|
foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
|
|
|
|
```
|
2018-06-12 22:28:20 +00:00
|
|
|
|
|
|
|
The DOF-plugin will be installed in the Isabelle user directory
|
|
|
|
(the exact location depends on the Isabelle version).
|
|
|
|
|
|
|
|
## Usage
|
|
|
|
|
|
|
|
The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
|
|
|
|
Isabelle projects that use DOF need to be created using
|
|
|
|
```console
|
|
|
|
foo@bar:~$ isabelle DOF_mkroot -d
|
|
|
|
```
|
|
|
|
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 (use ``-h`` to obtain a list of all installed setups):
|
|
|
|
```console
|
|
|
|
foo@bar:~$ isabelle DOF_mkroot -h
|
|
|
|
|
|
|
|
Usage: isabelle DOF_mkroot [OPTIONS] [DIR]
|
|
|
|
|
|
|
|
Options are:
|
|
|
|
-h print this help text and exit
|
|
|
|
-d enable document preparation
|
|
|
|
-n NAME alternative session name (default: DIR base name)
|
|
|
|
-o ONTOLOGY (default: core)
|
|
|
|
Available ontologies:
|
|
|
|
* cenelec_50126
|
|
|
|
* core
|
|
|
|
* mathex
|
|
|
|
* scholarly_paper
|
|
|
|
-t TEMPLATE (default: DEFAULT_TEMPLATE)
|
|
|
|
Available document templates:
|
|
|
|
* lncs
|
|
|
|
* scrreprt
|
|
|
|
|
|
|
|
Prepare session root DIR (default: current directory).
|
|
|
|
```
|
|
|
|
For example,
|
|
|
|
```console
|
|
|
|
foo@bar:~$ isabelle DOF_mkroot -d -o scholarly_paper -t lncs
|
|
|
|
```
|
|
|
|
creates a setup using the scholarly_paper ontology and Springer's
|
|
|
|
LNCS LaTeX class as document class. Note that the generated setup
|
|
|
|
does not include the actual ``llncs.cls`` file. This is due to
|
|
|
|
license restrictions. You need to obtain the file from Springer's
|
|
|
|
website and either copy it in you ``texmf`` directory or the ``root``
|
|
|
|
folder. In the latter case, you also need to add it in the ``ROOT`` file
|
|
|
|
as dependency.
|
|
|
|
|
|
|
|
## Team
|
|
|
|
|
|
|
|
Main contacts:
|
|
|
|
* [Achim D. Brucker](http://www.brucker.ch/)
|
|
|
|
* [Burkhart Wolff](https://www.lri.fr/~wolff/)
|
|
|
|
|
|
|
|
|
|
|
|
### Contributors
|
|
|
|
|
|
|
|
* Idir Ait-Sadoune
|
|
|
|
* Paolo Crisafulli
|
|
|
|
* Chantal Keller
|
|
|
|
|
|
|
|
## 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, Springer-Verlag, 2018.
|