Updated example to use scrartcl class.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Achim D. Brucker 2019-08-04 22:06:30 +01:00
parent 4e2fd09dff
commit c18d2fe350
1 changed files with 26 additions and 28 deletions

View File

@ -64,9 +64,11 @@ The installer will
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2019/ROOTS
* install the Isabelle/DOF-plugin into the Isabelle user directory
(the exact location depends on the Isabelle version).
* check that the AFP has been installed successfully.
* registers Isabelle/DOF as Isabelle component
* install the Isabelle/DOF-plugin into the Isabelle user directory
(the exact location depends on the Isabelle version).
* check that the AFP has been installed successfully.
## Usage
@ -82,7 +84,7 @@ isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApp
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
ontology definitions. If you want to edit the ontology definition,
just open the theory file with the default HOL session:
just open the theory file with the default HOL session:
```console
isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
@ -90,18 +92,18 @@ isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications
While this gives you more flexibility, it might "clutter" your editing
experience, as a lot of internal theories are loaded into Isabelle's
editor.
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
```console
foo@bar:~$ isabelle mkroot_DOF
foo@bar:~$ isabelle mkroot_DOF
```
The ``mkroot_DOF`` command takes the same parameter as the standard
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
command for building documents can be used.
``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
@ -114,43 +116,39 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
Options are:
-h print this help text and exit
-n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: core)
-o ONTOLOGY (default: scholarly_paper)
Available ontologies:
* cenelec_50128
* core
* mathex
* scholarly_paper
-t TEMPLATE (default: DEFAULT_TEMPLATE)
-t TEMPLATE (default: scrartcl)
Available document templates:
* lncs
* scrartcl
* scrreprt
* scrreprt-modern
Prepare session root DIR (default: current directory).
```
For example,
For example,
```console
foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t lncs
foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl
```
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.
creates a setup using the scholarly_paper ontology and the article
class from the KOMA-Script bundle.
## Team
Main contacts:
* [Achim D. Brucker](http://www.brucker.ch/)
* [Burkhart Wolff](https://www.lri.fr/~wolff/)
### Contributors
* Idir Ait-Sadoune
* Paolo Crisafulli
* Idir Ait-Sadoune
* Paolo Crisafulli
* Chantal Keller
## License
@ -163,13 +161,13 @@ SPDX-License-Identifier: BSD-2-Clause
* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
Wolff. [Using The Isabelle Ontology Framework: Linking the Formal
with the Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
In Conference on Intelligent Computer Mathematics (CICM). Lecture
with the Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
In Conference on Intelligent Computer Mathematics (CICM). Lecture
Notes in Computer Science (11006), Springer-Verlag, 2018.
* Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and
Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf).
In Software Engineering and Formal Methods (SEFM). Lecture Notes in
* Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and
Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf).
In Software Engineering and Formal Methods (SEFM). Lecture Notes in
Computer Science, Springer-Verlag, 2019.
## Master Repository