Achim D. Brucker 86152c374b | ||
---|---|---|
.woodpecker | ||
Isabelle_DOF | ||
Isabelle_DOF-Example-Extra | ||
Isabelle_DOF-Example-Scholarly_Paper | ||
Isabelle_DOF-Ontologies | ||
Isabelle_DOF-Proofs | ||
Isabelle_DOF-Unit-Tests | ||
etc | ||
scala | ||
.gitattributes | ||
.gitignore | ||
CHANGELOG.md | ||
CITATION | ||
LICENSE | ||
README.md | ||
ROOTS | ||
install-afp |
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 and formal development. The manual for Isabelle/DOF 1.3.0/Isabelle2021-1 is available online.
Pre-requisites
Isabelle/DOF has three major prerequisites:
- Isabelle: Isabelle/DOF requires Isabelle 2022. Please download the Isabelle 2022 distribution for your operating system from the Isabelle website.
- AFP: Isabelle/DOF requires several entries from the Archive of Formal Proofs (AFP). Please install the AFP following the instructions given at https://www.isa-afp.org/using.html.
- LaTeX: Isabelle/DOF requires a modern LaTeX installation, i.e., at least TeX Live 2022 with all available updates applied.
Installation
Isabelle/DOF is provided as an Isabelle component. 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:
foo@bar:~$ isabelle build -D . -x Isabelle_DOF-Proofs -x HOL-Proofs
This will compile Isabelle/DOF and run the example suite.
Usage
Opening an Example
If you want to work with or extend one of the examples, e.g., you can open it similar to any standard Isabelle theory:
isabelle jedit -d . -l Isabelle_DOF Isabelle_DOF-Example-Scholarly_Paper/IsaDofApplications.thy
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 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
:
isabelle jedit -d . -l Functional-Automata Isabelle_DOF-Example-Scholarly_Paper/IsaDofApplications.thy
While this gives you more flexibility, it might "clutter" your editing experience, as a lot of internal theories are loaded into Isabelle's editor.
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
- Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz
- Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc
Older releases are available here.
Repository Structure
The main
branch of this Repository is developed using the latest official
release of Isabelle (which is, at point of writing, Isabelle 2022). 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.
This repository is structured into several Isabelle sessions, each of which is stored in a subdirectory:
- 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.
- Isabelle_DOF-Example-Scholarly_Paper:
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: This session provided additional ontologies and document templates.
- 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. - Isabelle_DOF-Example-Extra: This directory contains additional example documents written using the Isabelle/DOF systems, each of which is defined in an own subdirectory.
- Isabelle_DOF-Proofs: This session provides the Isabelle/DOF systems with proof objects. This is required for the deep ontology embedding.
Team
Main contacts:
Contributors
- Idir Ait-Sadoune
- Paolo Crisafulli
- Chantal Keller
- Nicolas Méric
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 (11006), Springer-Verlag, 2018. doi:10.1007/978-3-319-96812-4_3.
-
Achim D. Brucker and Burkhart Wolff. Isabelle/DOF: Design and Implementation. In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science (11724), Springer-Verlag, 2019. doi:10.1007/978-3-030-30446-1_15.
-
Achim D. Brucker, Burkhart Wolff. Using Ontologies in Formal Developments Targeting Certification. In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. doi:10.1007/978-3-030-34968-4_4
-
Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. Making Agile Development Processes fit for V-style Certification Procedures.. In ERTS 2018. https://hal.archives-ouvertes.fr/hal-01702815
Upstream Repository
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.