diff --git a/README.md b/README.md index 04e05ad..f8806a4 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,32 @@ # [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 allows for both conventional typesetting as well as formal -development. The manual for [Isabelle/DOF 1.3.0/Isabelle2021-1 is available +Isabelle/DOF allows for both conventional typesetting and formal development. +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) ## Pre-requisites Isabelle/DOF has three major prerequisites: -* **Isabelle:** Isabelle/DOF requires [Isabelle 2022](http://isabelle.in.tum.de/website-Isabelle2022/). - Please download the Isabelle 2022 distribution for your operating - system from the [Isabelle +* **Isabelle:** Isabelle/DOF requires [Isabelle + 2022](http://isabelle.in.tum.de/website-Isabelle2022/). Please download the + Isabelle 2022 distribution for your operating system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2022/). -* **AFP:** Isabelle/DOF requires two entries from the [Archive of - Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the - AFP following the instructions given at - . +* **AFP:** Isabelle/DOF requires two entries from the [Archive of Formal Proofs + (AFP)](https://www.isa-afp.org/). Please install the AFP following the + instructions given at . * **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 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 (if you executed -this command already during the installation of the pre-requisites, you -can skip it now): +this command already during the installation of the prerequisites, you can skip +it now): ```console foo@bar:~$ isabelle components -u `pwd` @@ -44,25 +44,24 @@ This will compile Isabelle/DOF and run the example suite. ### 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: +If you want to work with or extend one of the examples, e.g., you can open it +similar to any standard Isabelle theory: ```console 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 -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: +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: ```console isabelle jedit -d . -l HOL examples/scholarly_paper/2018_cicm/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. +experience, as a lot of internal theories are loaded into Isabelle's editor. ### Creating a New Project @@ -73,23 +72,22 @@ Isabelle projects that use DOF need to be created using foo@bar:~$ isabelle dof_mkroot ``` -The ``dof_mkroot`` command takes the same parameter as the standard -``mkroot`` command of Isabelle. Thereafter, the normal Isabelle -command for building documents can be used. +The ``dof_mkroot`` command takes the same parameter as the standard ``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 -can be selected. For example, +Using the ``-o`` option, different ontology setups can be selected and using the +``-t`` option, different LaTeX setups can be selected. For example, ```console foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl ``` -creates a setup using the scholarly_paper ontology and the article -class from the KOMA-Script bundle. +creates a setup using the scholarly_paper ontology and the article class from +the KOMA-Script bundle. -The help (option ``-h``) show a list of all supported ontologies and -document templates: +The help (option ``-h``) show a list of all supported ontologies and document +templates: ```console foo@bar:~$ isabelle dof_mkroot -h @@ -114,7 +112,7 @@ are available: * [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 +### Older Releases * Isabelle/DOF 1.2.0/Isabelle2021 * [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf) @@ -155,28 +153,32 @@ 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](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, 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. [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 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 (11724), Springer-Verlag, 2019. + 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](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 - Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. +* 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. [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 - Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document) - In ERTS 2018. +* 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. ## Upstream Repository -The upstream git repository, i.e., the single source of truth, for this project is hosted -at . +The upstream git repository, i.e., the single source of truth, for this project +is hosted at .