Merge branch 'main' into isabelle_nightly

README.md

@@ -7,7 +7,7 @@ Isabelle/DOF allows for both conventional typesetting and formal development.
 
 Isabelle/DOF has two major prerequisites:
 
-* **Isabelle (Development Version):** Isabelle/DOF requires [Isabelle](https://isabelle.in.tum.de/)
+* **Isabelle 2025:** Isabelle/DOF requires [Isabelle](https://isabelle.in.tum.de/)
   and several entries from the [Archive of Formal Proofs
   (AFP)](https://www.isa-afp.org/).
 * **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
@@ -33,7 +33,12 @@ Isabelle/DOF is provided as one AFP entry:
 * [Isabelle_DOF:](https://www.isa-afp.org/entries/Isabelle_DOF.html) This entry
   contains the Isabelle/DOF system itself, including the Isabelle/DOF manual.
 
-### Installation of the Development Version (Git Repository)
+### Installation of Add-On Packages and Examples
+
+Add-ons to Isabelle/DOF, in particular, additional ontologies, document templates, 
+and examples, are provided on [Zenodo](https://doi.org/10.5281/zenodo.3370482). 
+
+## 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
@@ -65,9 +70,8 @@ foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs
 ## Usage
 
 In the following, we assume that you installed Isabelle/DOF either from the AFP
-(adding the AFP as a component to your Isabelle system) or from the Git
-repository of Isabelle/DOF (installing Isabelle/DOF as a component to your
-Isabelle system).
+(adding the AFP as a component to your Isabelle system) with the add-ons 
+available on Zenodo (or from the Git repository of Isabelle/DOF). 
 
 Assuming that your current directory contains the example academic paper in the
 subdirectory ``Isabelle_DOF-Example-I/``, you can open it similar
@@ -121,12 +125,9 @@ in a subdirectory:
 
 ## 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)
+Since Isabelle 2024, Isabelle/DOF synchronises its releases with the releases
+of Isabelle. The core of Isabelle/DOF is part of the Archive of Formal Proofs
+and several add-on packages are released on Zenodo. 
 
 Older releases are available [here.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/)
 
@@ -152,6 +153,19 @@ SPDX-License-Identifier: BSD-2-Clause
 
 ## Publications
 
+* Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Parametric
+  ontologies in formal software engineering. Sci. Comput. Program. 241: 103231
+  (2025). [do:10.1016/j.scico.2024.103231](https://doi.org/10.1016/j.scico.2024.103231)
+
+* Nicolas Méric: An Ontology Framework for Formal Libraries: Doctoral Thesis at
+  the University Pris-Saclay. (Conception et Implémentation d'un Environnement
+  d'Ontologie pour des Bibliothèques Formelles). University of Paris-Saclay,
+  France, 2024. <https://tel.archives-ouvertes.fr/tel-04870527>
+
+* Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Using Deep
+  Ontologies in Formal Software Engineering. ABZ 2023: 15-32.
+  [doi:10.1007/978-3-031-33163-3_2](https://doi.org/10.1007/978-3-031-33163-3_2)
+
 * 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).

README_DEVELOPMENT.md

@@ -4,7 +4,7 @@
 
 Isabelle/DOF has three major prerequisites:
 
-* **Isabelle:** Isabelle/DOF requires [the latest development version of Isabelle]
+* **Isabelle:** Isabelle/DOF requires [Isabelle 2025]
   (https://isabelle.in.tum.de).
 * **AFP:** Isabelle/DOF requires several entries from the [development version of the Archive of Formal Proofs
   (AFP)](https://devel.isa-afp.org/).

install-afp

@@ -0,0 +1,187 @@
+#!/usr/bin/env bash
+# Copyright (c) 2018-2019 The University of Sheffield.
+#               2019-2020 The University of Exeter. 
+#               2018-2020 The University of Paris-Saclay. 
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Redistributions of source code must retain the above copyright
+#    notice, this list of conditions and the following disclaimer.
+# 2. Redistributions in binary form must reproduce the above copyright
+#    notice, this list of conditions and the following disclaimer in
+#    the documentation and/or other materials provided with the
+#    distribution.
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+# POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+#set -e
+shopt -s nocasematch
+
+
+print_help()
+{
+    echo "Usage: isabelle env ./install-afp [OPTION] "
+    echo ""
+    echo "Warning: This tools is deprecated."
+    echo ""
+    echo "Run ..."
+    echo ""
+    echo "  --help, -h                display this help message"
+}
+
+
+
+exit_error() {
+    echo ""
+    echo "  *** Local AFP installation FAILED, please check the README.md for help ***"
+    echo ""
+    exit 1
+}
+
+confirm_usage() {
+    echo "* From Isabelle2021-1 on, the recommended method for making the whole AFP "
+    echo "  available to Isabelle is the isabelle components -u command."
+    echo "  For doing so, please follow the instructions at: "
+    echo "  https://www.isa-afp.org/help/"
+    echo ""
+    echo "  Alternatively, you can continue, on your own risk, to install only"
+    echo "  the AFP entries required to run Isabelle/DOF."
+    echo ""
+    read -p "    Still continue (y/N)? " -n 1 -r
+    echo 
+    if [[ $REPLY =~ ^[Yy]$ ]];
+    then 
+        echo "    Continuing installation on your OWN risk."
+    else
+        exit_error
+    fi
+}
+check_isabelle_version() {
+    echo "* Checking Isabelle version:"
+    if [ "Isabelle" == "$ACTUAL_ISABELLE_VERSION" ]; then
+        echo "  ERROR:"
+        echo "    This script does not support the development version of Isabelle."
+        echo "    The recommended way for installing the AFP for the development"
+        echo "    version of Isabelle is to clone the AFP repository:"
+        echo "    https://foss.heptapod.net/isa-afp/afp-devel/"
+        exit_error
+    fi
+    if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
+        echo "  WARNING:"
+        echo "    The version of Isabelle (i.e., $ACTUAL_ISABELLE_VERSION) you are using"
+        echo "                        IS NOT SUPPORTED"
+        echo "    by the current version of Isabelle/DOF. Please install a supported"
+        echo "    version of Isabelle and rerun the install script, providing the"
+        echo "    the \"isabelle\" command as argument."
+        echo "    Isabelle ($ISABELLE_VERSION) can be obtained from:"
+        echo "    https://isabelle.in.tum.de/website-$ISABELLE_VERSION/"
+        echo ""
+        read -p "    Still continue (y/N)? " -n 1 -r
+        echo 
+        if [[ $REPLY =~ ^[Yy]$ ]];
+        then 
+            echo "    Continuing installation on your OWN risk."
+        else
+            exit_error
+        fi
+     else
+        echo "  Success: found supported Isabelle version ($ISABELLE_VERSION)"
+    fi
+}
+
+check_afp_entries() {
+    echo "* Checking availability of AFP entries:"
+    missing=""
+    required="Regular-Sets Functional-Automata Physical_Quantities Metalogic_ProofChecker"
+    for afp in $required; do 
+        res=`$ISABELLE_TOOL build -n $afp 2>/dev/null || true`
+        if [ "$res" != "" ]; then 
+            echo "  Success: found APF entry $afp."
+        else
+            echo "  Warning: could not find AFP entry $afp."
+            missing="$missing $afp"
+       fi
+    done
+    if [ "$missing" != "" ]; then 
+        echo "           Trying to install AFP (this might take a few *minutes*) ...."
+	extract=""
+	for e in $missing; do
+	    extract="$extract $AFP_DATE/thys/$e"
+	done
+	mkdir -p .afp
+        if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then 
+            for e in $missing; do 
+                echo "           Registering $e"
+                $ISABELLE_TOOL components -u "$PWD/.afp/$AFP_DATE/thys/$e"
+            done
+            echo "           AFP installation successful."
+        else
+            echo "  FAILURE: could not find AFP entries: $missing."
+            echo "    Please obtain the AFP from"
+            echo "    $AFP_URL"
+            echo "    and follow the following instructions:"
+            echo "    https://www.isa-afp.org/using.html"
+            exit_error
+        fi
+    fi
+}
+
+while [ $# -gt 0 ]
+do
+    case "$1" in
+        --help|-h)
+            print_help
+            exit 0;;
+        *)  print_help
+            exit 1;;
+    esac
+    shift
+done
+
+if [ -z ${ISABELLE_TOOL+x} ];
+then
+    print_help
+    exit 1
+fi
+
+ACTUAL_ISABELLE_VERSION=`$ISABELLE_TOOL version`
+
+ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL dof_param -b isabelle_version)"
+
+if [ ${ISABELLE_VERSION} = "Isabelle" ];
+then
+   echo "Error: cannot find Isabelle/DOF configuration, please check that you"
+   echo "       registered Isabelle/DOF as an Isabelle component, e.g., using" 
+   echo "       isabelle components -u ."
+   exit 1
+fi
+
+
+
+AFP_DATE="$($ISABELLE_TOOL dof_param -b afp_version)"
+AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
+
+echo ""
+echo "Isabelle/DOF AFP Installation Utility"
+echo "====================================="
+confirm_usage
+check_isabelle_version
+check_afp_entries
+echo "* AFP Installation successful."
+echo "  You should now be able to enjoy Isabelle/DOF by building its session"
+echo "  and all example documents by executing:"
+echo "  $ISABELLE_TOOL build -D ."
+exit 0

upstream_afp/Isabelle_DOF/scala/dof.scala

@@ -39,7 +39,7 @@ import isabelle._
 object DOF {
   /** parameters **/
 
-  val isabelle_version = ""
+  val isabelle_version = "2025"
   val isabelle_url = "https://isabelle.sketis.net/devel/release_snapshot/"
 
   val afp_version = "afp-devel"