Burkhart Wolff bfb8dd901c | ||
---|---|---|
document-generator | ||
examples | ||
old | ||
ontologies | ||
patches | ||
test | ||
.gitignore | ||
Assert.thy | ||
AssertLong.thy | ||
CITATION | ||
Isa_DOF.thy | ||
LICENSE | ||
MyCommentedIsabelle.thy | ||
README.md | ||
ROOT | ||
RegExp.thy | ||
TODO | ||
install |
README.md
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.
Installation
In most case, the DOF-plugin can be installed as follows:
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:
foo@bar:~$ ./install /usr/local/Isabelle2016-1/bin/isabelle
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
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):
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,
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:
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.