nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Linting.

This commit is contained in:
Achim D. Brucker 2022-11-01 20:58:34 +00:00
parent fc575a5be5
commit ab1877ce8e
1 changed files with 47 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

90
README.md
View File

@ -1,32 +1,32 @@
# [Isabelle/DOF](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF): Document Preparation Setup # [Isabelle/DOF](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF): Document Preparation Setup
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
Isabelle/DOF allows for both conventional typesetting as well as formal Isabelle/DOF allows for both conventional typesetting and formal development.
development. The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf) online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
## Pre-requisites ## Pre-requisites
Isabelle/DOF has three major prerequisites: Isabelle/DOF has three major prerequisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle 2022](http://isabelle.in.tum.de/website-Isabelle2022/). * **Isabelle:** Isabelle/DOF requires [Isabelle
Please download the Isabelle 2022 distribution for your operating 2022](http://isabelle.in.tum.de/website-Isabelle2022/). Please download the
system from the [Isabelle Isabelle 2022 distribution for your operating system from the [Isabelle
website](http://isabelle.in.tum.de/website-Isabelle2022/). website](http://isabelle.in.tum.de/website-Isabelle2022/).
* **AFP:** Isabelle/DOF requires two entries from the [Archive of * **AFP:** Isabelle/DOF requires two entries from the [Archive of Formal Proofs
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the (AFP)](https://www.isa-afp.org/). Please install the AFP following the
AFP following the instructions given at instructions given at <https://www.isa-afp.org/using.html>.
<https://www.isa-afp.org/using.html>.
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied. [TeX Live 2022](https://www.tug.org/texlive/) with all available updates
applied.
## Installation ## Installation
Isabelle/DOF is provided as an Isabelle component. After installing the Isabelle/DOF is provided as an Isabelle component. After installing the
prerequisites, change into the directory containing Isabelle/DOF (this should be prerequisites, change into the directory containing Isabelle/DOF (this should be
the directory containing this `README.md` file) and execute (if you executed the directory containing this `README.md` file) and execute (if you executed
this command already during the installation of the pre-requisites, you this command already during the installation of the prerequisites, you can skip
can skip it now): it now):
```console ```console
foo@bar:~$ isabelle components -u `pwd` foo@bar:~$ isabelle components -u `pwd`
@ -44,25 +44,24 @@ This will compile Isabelle/DOF and run the example suite.
### Opening an Example ### Opening an Example
If you want to work with or extend one of the examples, e.g., you can If you want to work with or extend one of the examples, e.g., you can open it
open it similar to any standard Isabelle theory: similar to any standard Isabelle theory:
```console ```console
isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy isabelle jedit -d . -l Isabelle_DOF examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
``` ```
This will open an example of a scientific paper using the pre-compiled This will open an example of a scientific paper using the pre-compiled session
session ``Isabelle_DOF``, i.e., you will not be able to edit the ``Isabelle_DOF``, i.e., you will not be able to edit the ontology definitions.
ontology definitions. If you want to edit the ontology definition, If you want to edit the ontology definition, just open the theory file with the
just open the theory file with the default HOL session: default HOL session:
```console ```console
isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
``` ```
While this gives you more flexibility, it might "clutter" your editing While this gives you more flexibility, it might "clutter" your editing
experience, as a lot of internal theories are loaded into Isabelle's experience, as a lot of internal theories are loaded into Isabelle's editor.
editor.
### Creating a New Project ### Creating a New Project
@ -73,23 +72,22 @@ Isabelle projects that use DOF need to be created using
foo@bar:~$ isabelle dof_mkroot foo@bar:~$ isabelle dof_mkroot
``` ```
The ``dof_mkroot`` command takes the same parameter as the standard The ``dof_mkroot`` command takes the same parameter as the standard ``mkroot``
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle command of Isabelle. Thereafter, the normal Isabelle command for building
command for building documents can be used. documents can be used.
Using the ``-o`` option, different ontology setups can be Using the ``-o`` option, different ontology setups can be selected and using the
selected and using the ``-t`` option, different LaTeX setups ``-t`` option, different LaTeX setups can be selected. For example,
can be selected. For example,
```console ```console
foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl
``` ```
creates a setup using the scholarly_paper ontology and the article creates a setup using the scholarly_paper ontology and the article class from
class from the KOMA-Script bundle. the KOMA-Script bundle.
The help (option ``-h``) show a list of all supported ontologies and The help (option ``-h``) show a list of all supported ontologies and document
document templates: templates:
```console ```console
foo@bar:~$ isabelle dof_mkroot -h foo@bar:~$ isabelle dof_mkroot -h
@ -155,28 +153,32 @@ SPDX-License-Identifier: BSD-2-Clause
## Publications ## Publications
* Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart * Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff.
Wolff. [Using The Isabelle Ontology Framework: Linking the Formal [Using The Isabelle Ontology Framework: Linking the Formal with the
with the Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf). Informal](https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf).
In Conference on Intelligent Computer Mathematics (CICM). Lecture In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in
Notes in Computer Science (11006), Springer-Verlag, 2018. Computer Science (11006), Springer-Verlag, 2018.
[doi:10.1007/978-3-319-96812-4_3](https://doi.org/10.1007/978-3-319-96812-4_3). [doi:10.1007/978-3-319-96812-4_3](https://doi.org/10.1007/978-3-319-96812-4_3).
* Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and * Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and
Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf). Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf).
In Software Engineering and Formal Methods (SEFM). Lecture Notes in In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer
Computer Science (11724), Springer-Verlag, 2019. Science (11724), Springer-Verlag, 2019.
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15). [doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In * Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments
Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. Targeting
Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf).
In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918).
Springer-Verlag 2019.
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4) [doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development * Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff.
Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document) [Making Agile Development Processes fit for V-style Certification
In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815> Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document). In ERTS
2018. <https://hal.archives-ouvertes.fr/hal-01702815>
## Upstream Repository ## Upstream Repository
The upstream git repository, i.e., the single source of truth, for this project is hosted The upstream git repository, i.e., the single source of truth, for this project
at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>. is hosted at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.