Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Updated README.md documenting the preliminaries.

This commit is contained in:
Achim D. Brucker 2019-01-05 22:32:17 +00:00
parent dfa2581f06
commit 45012da116
1 changed files with 32 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
README.md
View File

@ -4,6 +4,38 @@ Isabelle/DOF is a novel Document Ontology Framework on top of
Isabelle. Isabelle/DOF allows for both conventional typesetting as
well as formal development.
## 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
```
## Installation
In most case, the DOF-plugin can be installed as follows:
@ -20,13 +52,6 @@ foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
The DOF-plugin will be installed in the Isabelle user directory
(the exact location depends on the Isabelle version).
Additionally, you have to replace the file
```Isabelle2017/src/Pure/Thy/thy_output.ML```
by the file you find in the Isabelle_DOF-distribution:
```patches/thy_output.ML```
When starting up, Isabelle will recompile itself and integrating this
file (which modifies about 10 lines in the LaTeX generator...).
## Usage
The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
@ -88,8 +113,6 @@ Main contacts:
* Paolo Crisafulli
* Chantal Keller
## License
This project is licensed under a 2-clause BSD license.