2019-08-10 19:07:52 +00:00
|
|
|
# [Isabelle/DOF](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF): Document Preparation Setup
|
2018-02-07 17:43:15 +00:00
|
|
|
|
2019-08-11 21:26:43 +00:00
|
|
|
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
2022-11-01 20:58:34 +00:00
|
|
|
Isabelle/DOF allows for both conventional typesetting and formal development.
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2019-08-04 12:46:53 +00:00
|
|
|
## Pre-requisites
|
2019-01-05 22:32:17 +00:00
|
|
|
|
2023-02-28 00:50:23 +00:00
|
|
|
Isabelle/DOF has two major prerequisites:
|
|
|
|
|
2023-09-14 05:33:28 +00:00
|
|
|
* **Isabelle 2023:** Isabelle/DOF requires [Isabelle](https://isabelle.in.tum.de/)
|
2023-02-28 00:50:23 +00:00
|
|
|
and several entries from the [Archive of Formal Proofs
|
|
|
|
(AFP)](https://www.isa-afp.org/).
|
2022-06-24 15:58:07 +00:00
|
|
|
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
|
2022-11-01 20:58:34 +00:00
|
|
|
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates
|
|
|
|
applied.
|
2021-03-15 10:24:31 +00:00
|
|
|
|
2019-08-04 12:46:53 +00:00
|
|
|
## Installation
|
2018-02-07 18:44:27 +00:00
|
|
|
|
2023-02-28 00:50:23 +00:00
|
|
|
<!--
|
|
|
|
Isabelle/DOF is available as part of the [Archive of Formal Proofs
|
|
|
|
(AFP)](https://www.isa-afp.org/). This is the most convenient way to install
|
|
|
|
Isabelle/DOF for the latest official release of Isabelle.
|
|
|
|
|
|
|
|
### Installation from the Archive of Formal Proofs (AFP)
|
|
|
|
|
|
|
|
Isabelle/DOF is available in the AFP. Hence, for using Isabelle/DOF with the
|
|
|
|
latest official released version of Isabelle, please download the Isabelle
|
|
|
|
distribution for your operating system from the [Isabelle
|
|
|
|
website](https://isabelle.in.tum.de/). Furthermore, please install the AFP
|
|
|
|
following the instructions given at <https://www.isa-afp.org/help.html>.
|
|
|
|
|
2023-05-14 22:01:30 +00:00
|
|
|
Isabelle/DOF is currently consisting out of three AFP entries:
|
2023-02-28 00:50:23 +00:00
|
|
|
|
|
|
|
* [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry
|
|
|
|
contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
|
2023-04-15 15:55:15 +00:00
|
|
|
* [Isabelle_DOF-Example-I:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-I.html)
|
2023-02-28 00:50:23 +00:00
|
|
|
This entry contains an example of an academic paper written using the
|
|
|
|
Isabelle/DOF system.
|
2023-05-14 22:01:30 +00:00
|
|
|
* [Isabelle_DOF-Example-II:](https://www.isa-afp.org/entries/Isabelle_DOF-Example-II.html)
|
|
|
|
This entry contains an example of an academic paper written using the
|
|
|
|
Isabelle/DOF system.
|
2023-02-28 00:50:23 +00:00
|
|
|
|
|
|
|
-->
|
|
|
|
|
|
|
|
### Installation of the Development Version (Git Repository)
|
|
|
|
|
|
|
|
The development version of Isabelle/DOF that is available in this Git repository
|
|
|
|
provides, over the AFP version, additional ontologies, document templates, and
|
|
|
|
examples that might not yet "ready for general use". Furthermore, as it is
|
|
|
|
provided as an Isabelle component, it can also provide additional tools that
|
|
|
|
cannot be distributed via the AFP. For more details on installing the
|
|
|
|
development version, please consult the
|
|
|
|
[README_DEVELOPMENT.md](./README_DEVELOPMENT.md) file.
|
|
|
|
|
|
|
|
After installing the prerequisites, change into the directory containing
|
|
|
|
Isabelle/DOF (this should be the directory containing this ``README.md`` file)
|
|
|
|
and execute the following command for building the standard sessions of
|
|
|
|
Isabelle/DOF:
|
2019-08-04 12:46:53 +00:00
|
|
|
|
|
|
|
```console
|
2023-02-25 10:28:51 +00:00
|
|
|
foo@bar:~$ isabelle build -D . -x Isabelle_DOF-Proofs -x HOL-Proofs
|
2019-08-17 09:39:42 +00:00
|
|
|
```
|
|
|
|
|
2019-08-17 09:53:04 +00:00
|
|
|
This will compile Isabelle/DOF and run the example suite.
|
2019-08-17 09:39:42 +00:00
|
|
|
|
2023-03-05 23:18:47 +00:00
|
|
|
For building the session ``Isabelle_DOF-Proofs``, the timeout might need to
|
|
|
|
increased to avoid timeouts during building the dependencies:
|
|
|
|
|
|
|
|
```console
|
|
|
|
foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs
|
|
|
|
```
|
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
## Usage
|
|
|
|
|
2023-02-28 00:50:23 +00:00
|
|
|
In the following, we assume that you installed Isabelle/DOF either from the AFP
|
2023-03-15 10:52:23 +00:00
|
|
|
(adding the AFP as a component to your Isabelle system) or from the Git
|
2023-02-28 00:50:23 +00:00
|
|
|
repository of Isabelle/DOF (installing Isabelle/DOF as a component to your
|
|
|
|
Isabelle system).
|
2019-01-06 18:43:23 +00:00
|
|
|
|
2023-02-28 00:50:23 +00:00
|
|
|
Assuming that your current directory contains the example academic paper in the
|
2023-04-15 15:55:15 +00:00
|
|
|
subdirectory ``Isabelle_DOF-Example-I/``, you can open it similar
|
2023-02-28 00:50:23 +00:00
|
|
|
to any standard Isabelle theory:
|
2019-01-06 18:43:23 +00:00
|
|
|
|
|
|
|
```console
|
2023-04-15 15:55:15 +00:00
|
|
|
isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-I/IsaDofApplications.thy
|
2019-01-06 18:43:23 +00:00
|
|
|
```
|
|
|
|
|
2022-11-01 20:58:34 +00:00
|
|
|
This will open an example of a scientific paper using the pre-compiled session
|
2023-02-25 10:28:51 +00:00
|
|
|
``Isabelle_DOF``, i.e., you will not be able to edit the default ontologies
|
|
|
|
defined in the ``Isabelle_DOF`` session. If you want to edit the ontology definition,
|
|
|
|
just open the theory file with the session ``Functional-Automata``:
|
2019-01-06 18:43:23 +00:00
|
|
|
|
|
|
|
```console
|
2023-04-15 15:55:15 +00:00
|
|
|
isabelle jedit -l Functional-Automata Isabelle_DOF-Example-I/IsaDofApplications.thy
|
2019-01-06 18:43:23 +00:00
|
|
|
```
|
|
|
|
|
|
|
|
While this gives you more flexibility, it might "clutter" your editing
|
2022-11-01 20:58:34 +00:00
|
|
|
experience, as a lot of internal theories are loaded into Isabelle's editor.
|
2019-01-06 18:43:23 +00:00
|
|
|
|
2023-02-25 10:28:51 +00:00
|
|
|
## Repository Structure
|
|
|
|
|
|
|
|
The ``main`` branch of this Repository is developed using the latest official
|
2023-02-28 00:50:23 +00:00
|
|
|
release of Isabelle. This is also the main development branch. In addition, he
|
|
|
|
``Isabelle_dev`` branch is used for testing Isabelle/DOF with the latest
|
|
|
|
development version of Isabelle.
|
2023-02-25 10:28:51 +00:00
|
|
|
|
|
|
|
This repository is structured into several Isabelle sessions, each of which is stored
|
|
|
|
in a subdirectory:
|
|
|
|
|
|
|
|
* [Isabelle_DOF](./Isabelle_DOF/): This is the main session, providing the
|
|
|
|
Isabelle/DOF system. Furthermore, this session is currently under
|
|
|
|
consideration for a submission to the AFP.
|
2023-04-15 15:55:15 +00:00
|
|
|
* [Isabelle_DOF-Example-I](./Isabelle_DOF-Example-I/):
|
2023-02-25 10:28:51 +00:00
|
|
|
This session provides an example document written Isabelle/DOF. It only
|
|
|
|
requires the core ontologies provided by the ``Isabelle_DOF`` session.
|
|
|
|
Furthermore, this session is currently under consideration for a submission to
|
|
|
|
the AFP.
|
|
|
|
* [Isabelle_DOF-Ontologies](./Isabelle_DOF-Ontologies/): This session provided
|
|
|
|
additional ontologies and document templates.
|
|
|
|
* [Isabelle_DOF-Unit-Tests](./Isabelle_DOF-Unit-Tests/): This session includes
|
|
|
|
various tests for the Isabelle/DOF system, partly depending on the ontologies
|
|
|
|
provided by the ``Isabelle_DOF-Ontologies`` session.
|
2023-05-15 11:03:52 +00:00
|
|
|
* [Isabelle_DOF-Examples-Extra](./Isabelle_DOF-Examples-Extra/): This directory
|
2023-02-25 10:28:51 +00:00
|
|
|
contains additional example documents written using the Isabelle/DOF systems,
|
|
|
|
each of which is defined in an own subdirectory.
|
|
|
|
* [Isabelle_DOF-Proofs](./Isabelle_DOF-Proofs/): This session provides the
|
|
|
|
Isabelle/DOF systems with proof objects. This is required for the deep
|
|
|
|
ontology embedding.
|
2019-08-18 13:05:00 +00:00
|
|
|
|
2023-02-28 00:50:23 +00:00
|
|
|
## Releases
|
|
|
|
|
|
|
|
For releases, signed archives including a PDF version of the Isabelle/DOF manual
|
|
|
|
are available. The latest release is **Isabelle/DOF 1.3.0/Isabelle2021-1**:
|
|
|
|
|
|
|
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
|
|
|
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz)
|
|
|
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc)
|
|
|
|
|
|
|
|
Older releases are available [here.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/)
|
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
## Team
|
|
|
|
|
|
|
|
Main contacts:
|
2019-08-04 21:06:30 +00:00
|
|
|
|
2018-06-12 22:28:20 +00:00
|
|
|
* [Achim D. Brucker](http://www.brucker.ch/)
|
|
|
|
* [Burkhart Wolff](https://www.lri.fr/~wolff/)
|
|
|
|
|
|
|
|
### Contributors
|
|
|
|
|
2019-08-04 21:06:30 +00:00
|
|
|
* Idir Ait-Sadoune
|
|
|
|
* Paolo Crisafulli
|
2018-06-12 22:28:20 +00:00
|
|
|
* Chantal Keller
|
2022-06-24 15:58:07 +00:00
|
|
|
* Nicolas Méric
|
2018-06-12 22:28:20 +00:00
|
|
|
|
|
|
|
## License
|
|
|
|
|
|
|
|
This project is licensed under a 2-clause BSD license.
|
|
|
|
|
|
|
|
SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
|
|
|
|
## Publications
|
|
|
|
|
2022-11-01 20:58:34 +00:00
|
|
|
* 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 Notes in
|
|
|
|
Computer Science (11006), Springer-Verlag, 2018.
|
2019-08-18 20:39:43 +00:00
|
|
|
[doi:10.1007/978-3-319-96812-4_3](https://doi.org/10.1007/978-3-319-96812-4_3).
|
|
|
|
|
2019-08-04 21:06:30 +00:00
|
|
|
* Achim D. Brucker and Burkhart Wolff. [Isabelle/DOF: Design and
|
|
|
|
Implementation](https://www.brucker.ch/bibliography/download/2019/brucker.ea-isabelledof-2019.pdf).
|
2022-11-01 20:58:34 +00:00
|
|
|
In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer
|
|
|
|
Science (11724), Springer-Verlag, 2019.
|
2019-08-18 20:39:43 +00:00
|
|
|
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
|
2019-07-05 15:09:34 +00:00
|
|
|
|
2022-11-01 20:58:34 +00:00
|
|
|
* 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 Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918).
|
|
|
|
Springer-Verlag 2019.
|
2019-12-06 13:25:00 +00:00
|
|
|
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
|
|
|
|
|
2022-11-01 20:58:34 +00:00
|
|
|
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff.
|
|
|
|
[Making Agile Development Processes fit for V-style Certification
|
|
|
|
Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document). In ERTS
|
|
|
|
2018. <https://hal.archives-ouvertes.fr/hal-01702815>
|
2021-03-22 00:12:00 +00:00
|
|
|
|
2022-03-17 08:48:25 +00:00
|
|
|
## Upstream Repository
|
2019-06-17 09:32:51 +00:00
|
|
|
|
2022-11-01 20:58:34 +00:00
|
|
|
The upstream git repository, i.e., the single source of truth, for this project
|
|
|
|
is hosted at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.
|