Make use of install script optional in favor of registration as Isabelle component. Style files, templates, and scripts are no longer installed into ISABELLE_USER_HOME.

2022-03-27 13:21:55 +01:00 · 2022-03-27 13:21:55 +01:00 · 7b8ae0a93d
parent 700855411e
commit 7b8ae0a93d
8 changed files with 90 additions and 152 deletions
--- a/.config
+++ b/.config
@ -1,18 +0,0 @@
-# Isabelle/DOF Version Information
-DOF_VERSION="Unreleased"    # "Unreleased" for development, semantic version for releases 
-DOF_LATEST_VERSION="1.2.0"    
-DOF_LATEST_ISABELLE="Isabelle2021"
-DOF_LATEST_DOI="10.5281/zenodo.6385695"
-DOF_GENERIC_DOI="10.5281/zenodo.3370482"
-#
-# Isabelle and AFP Configuration
-ISABELLE_VERSION="Isabelle2021-1"
-ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021-1/"
-AFP_DATE="afp-2021-12-28"
-AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
-#
-# Isabelle/DOF Repository Configuration
-DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
-DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
-#
--- a/.woodpecker/build.yml
+++ b/.woodpecker/build.yml
@ -7,7 +7,7 @@ pipeline:
      - export `isabelle getenv ISABELLE_HOME_USER`
      - mkdir -p $ISABELLE_HOME_USER/etc
      - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
-      - ./install
+      - isabelle components -u `pwd` 
      - isabelle build -D . -o browser_info
      - isabelle mkroot_DOF DOF_test
      - isabelle build -D DOF_test
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@ -15,6 +15,9 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
  from ROOT files.
 - lipics support is now official, requires document option "document_comment_latex=true"
  in the ROOT file.
+- Isabelle/DOF is now a proper Isabelle component that should be installed using the 
+  "isabelle components" command. The installation script is now only an convenience 
+  means for installing the required AFP entries.

 ## 1.2.0 - 2022-03-26

--- a/README.md
+++ b/README.md
@ -7,38 +7,37 @@ online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF

 ## Pre-requisites

-Isabelle/DOF has two major pre-requisites:
+Isabelle/DOF has three major pre-requisites:

 * **Isabelle:** Isabelle/DOF requires [Isabelle 2021-1](http://isabelle.in.tum.de/website-Isabelle2021-1/).
  Please download the Isabelle 2021-1 distribution for your operating
-  system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
+  system from the [Isabelle
+  website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
+* **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
+  <https://www.isa-afp.org/using.html>. For your convenience, we also
+  provide a script that only installs the two entries required by
+  Isabelle/DOF into the local Isabelle/DOF directory. You can use this 
+  script as follows:
+  ```console
+  foo@bar:~$ isabelle env ./install-afp
+  ```  
 * **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.
  
 ## Installation

-In most case, the DOF-plugin can be installed as follows:
+Isabelle/DOF is provided as a Isabelle component. After installing the
+pre-requisites the Isabelle/Archive needs to be unpacked and
+registered.  Change into the directory you unpacked Isabelle/DOF (this
+should be the directory containing this ``README.md'' file) and execute

 ```console
-foo@bar:~$ ./install
+foo@bar:~$ isabelle components -u `pwd`
 ```

-If a specific Isabelle version should be used (i.e., not the default
-one), the full path to the ``isabelle`` command needs to be passed as
-using the ``--isabelle`` command line argument of the ``install`` script:
-
-```console
-foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021-1/bin/isabelle
-```
-
-For further command line options of the installer, please use the
-built-in help:
-
-```console
-foo@bar:~$ ./install --help
-```
-
-A final step for the installation is:
+The final step for the installation is:

 ```console
 foo@bar:~$ isabelle build -D .
--- a/etc/settings
+++ b/etc/settings
@ -4,3 +4,22 @@ ISABELLE_DOF_HOME="$COMPONENT"
 ISABELLE_TOOLS="$ISABELLE_TOOLS":"$ISABELLE_DOF_HOME/src/Tools"
 ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc":"$ISABELLE_DOCS"

+# Isabelle/DOF Version Information
+DOF_VERSION="Unreleased"    # "Unreleased" for development, semantic version for releases 
+DOF_DATE="00/00/00"
+DOF_LATEST_VERSION="1.2.0"    
+DOF_LATEST_ISABELLE="Isabelle2021"
+DOF_LATEST_DOI="10.5281/zenodo.6385695"
+DOF_GENERIC_DOI="10.5281/zenodo.3370482"
+#
+# Isabelle and AFP Configuration
+ISABELLE_VERSION="Isabelle2021-1"
+ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021-1/"
+AFP_DATE="afp-2021-12-28"
+AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
+#
+# Isabelle/DOF Repository Configuration
+DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
+DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
+#
--- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
@ -70,35 +70,26 @@ subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
 text\<open>
  In the following, we assume that you already downloaded the \<^isadof> distribution 
  (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for 
-  installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install\<close> script. 
+  installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install-afp\<close> script. 
  We start by extracting the \<^isadof> archive:
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
 This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
-Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installation 
-automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), 
-namely the AFP  entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} 
-and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a 
-few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system, 
-which requires  \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as 
-Isabelle component. 

-If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your  \<^boxed_bash>\<open>PATH\<close>, you need to call the 
- \<^boxed_bash>\<open>install\<close> script with the  \<^boxed_bash>\<open>--isabelle\<close> option, passing the full-qualified
-path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives 
-you an overview of all available configuration options):
+\<^isadof> depends on the the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), namely the AFP  
+entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and 
+``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. You can either
+install the complete AFP, following the instructions given at \<^url>\<open>https://www.isa-afp.org/using.html\<close>), 
+or use the provided \<^boxed_bash>\<open>install\<close> script to install a minimal AFP 
+setup into the local \<^isadof> directory. The script needs to be prefixed with the 
+\<^boxed_bash>\<open>isabelle env\<close> command:

@{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
-ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
+ë\prompt{\isadofdirn}ë isabelle env ./install-afp

 Isabelle/DOF Installer
 ======================
 * Checking Isabelle version:
  Success: found supported Isabelle version ë(\isabellefullversion)ë
-* Check availability of Isabelle/DOF patch:
-  Warning: Isabelle/DOF patch is not available or outdated.
-           Trying to patch system ....
-       Applied patch successfully, Isabelle/HOL will be rebuilt during
-       the next start of Isabelle.
 * Checking availability of AFP entries:\<close>}

@{boxed_bash [display]
@ -110,18 +101,6 @@ Isabelle/DOF Installer
           Registering Functional-Automata iëën 
                 /home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
           AFP installation successful.
-* Searching fëëor existing installation:
-  No old installation found.
-* Installing Isabelle/DOF
-  - Installing Tools iëën 
-        /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/Toolsë
-  - Installing document templates iëën 
-        /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/document-templateë
-  - Installing LaTeX styles iëën 
-       /home/achim/.isabelle/Isabelleë\isabelleversion/DOF/latexë
-  - Registering Isabelle/DOF
-    * Registering tools iëën 
-       /home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë
 * Installation successful. Enjoy Isabelle/DOF, you can build the session
  Isabelle/DOF and all example documents by executing:
  /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
--- a/89
+++ b/89
@ -30,23 +30,13 @@
 #set -e
 shopt -s nocasematch

-# get global configuration  
-if [ -d .git ]; then
-    export `git show -s --format="COMMIT=%H DATE=%cd" --date=short | sed -e 's|-|/|g'`
-fi    
-source .config
-
 print_help()
 {
-    echo "Usage: install [OPTION] "
+    echo "Usage: isabelle env ./install-afp [OPTION] "
    echo ""
    echo "Run ..."
    echo ""
    echo "  --help, -h                display this help message"
-    echo "  --isabelle, -i isabelle   isabelle command used for installation"
-    echo "                            (default: $ISABELLE)"
-    echo "  --skip-afp, -s            skip installation of AFP entries. "
-    echo "                            USE AT YOUR OWN RISK (default: $SKIP)"
 }


@ -88,7 +78,7 @@ check_afp_entries() {
    missing=""
    required="Regular-Sets Functional-Automata"
    for afp in $required; do 
-        res=`$ISABELLE build -n $afp 2>/dev/null || true`
+        res=`$ISABELLE_TOOL build -n $afp 2>/dev/null || true`
        if [ "$res" != "" ]; then 
            echo "  Success: found APF entry $afp."
        else
@ -106,7 +96,7 @@ check_afp_entries() {
        if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then 
            for e in $missing; do 
                echo "           Registering $e"
-                $ISABELLE components -u "$PWD/.afp/$AFP_DATE/thys/$e"
+                $ISABELLE_TOOL components -u "$PWD/.afp/$AFP_DATE/thys/$e"
            done
            echo "           AFP installation successful."
        else
@ -120,64 +110,15 @@ check_afp_entries() {
    fi
 }

-check_old_installation(){
-    echo "* Searching for existing installation:"
-    if [[ -d "$ISABELLE_HOME_USER/DOF" ]]; then
-        echo "  Found old installation, moving it to $ISABELLE_HOME_USER/DOF.bak."
-        rm -rf "$ISABELLE_HOME_USER/DOF.bak"
-        mv "$ISABELLE_HOME_USER/DOF" "$ISABELLE_HOME_USER/DOF.bak"
-    else
-        echo "  No old installation found."
-    fi
-
-}
-
-install_and_register(){
-    echo "* Installing Isabelle/DOF"
-
-    DIR="$ISABELLE_HOME_USER/DOF/document-template"
-    echo "  - Installing document templates in $DIR"
-    mkdir -p "$DIR"
-    cp $GEN_DIR/document-templates/* "$DIR"
-    cp $GEN_DIR/DOF/*/*.sty "$DIR"
-    
-    ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
-    sed -i -e "s|%%% CONFIG %%%| \
-      \\\\renewcommand{\\\\dof@isabelleversion}{$ISABELLE_SHORT_VERSION} \
-      \\\\renewcommand{\\\\isabellelatestversion}{$DOF_LATEST_ISABELLE} \
-      \\\\renewcommand{\\\\isabellefullversion}{$ISABELLE_VERSION\\\\xspace} \
-      \\\\renewcommand{\\\\dof@version}{$DOF_VERSION} \
-      \\\\renewcommand{\\\\doflatestversion}{$DOF_LATEST_VERSION} \
-      \\\\renewcommand{\\\\isadoflatestdoi}{$DOF_LATEST_DOI} \
-      \\\\renewcommand{\\\\isadofgenericdoi}{$DOF_GENERIC_DOI} \
-      \\\\renewcommand{\\\\isabelleurl}{$ISABELLE_URL} \
-      \\\\renewcommand{\\\\dofurl}{$DOF_URL} \
-      \\\\renewcommand{\\\\dof@artifacturl}{https://$DOF_ARTIFACT_HOST/$DOF_ARTIFACT_DIR}|" \
-      "$DIR/DOF-core.sty"
-
-    DIR="$ISABELLE_HOME_USER/DOF/latex"
-    echo "  - Installing LaTeX styles in $DIR"
-    mkdir -p "$DIR"
-    cp $GEN_DIR/ontologies/*/*.sty "$DIR"
-    
+register(){
    echo "  - Registering Isabelle/DOF"
-    sed -i -e "s|<isadofurl>|$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/*
-    LTX_VERSION="$DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
-    sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" $ISABELLE_HOME_USER/DOF/*/*
-    $ISABELLE components -u "$PWD"    
+    $ISABELLE_TOOL components -u "$PWD"    
 }


-ISABELLE=`command -v isabelle`
-SKIP="false"
 while [ $# -gt 0 ]
 do
    case "$1" in
-        --isabelle|-i)
-            ISABELLE="$2";
-            shift;;
-        --skip-afp|-s)
-            SKIP="true";;
        --help|-h)
            print_help
            exit 0;;
@ -187,27 +128,15 @@ do
    shift
 done

-
-ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
-GEN_DIR=src
-PROG=`echo $0 | sed 's|.*/||'`;
-VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME`
-for i in $VARS; do 
-	export "$i"
-done
+ACTUAL_ISABELLE_VERSION=`$ISABELLE_TOOL version`

 echo ""
 echo "Isabelle/DOF Installer"
 echo "======================"
 check_isabelle_version
-if [ "$SKIP" = "true" ]; then
-  echo "* Warning: skipping installation of AFP entries."
-else
-  check_afp_entries
-fi
-check_old_installation
-install_and_register
+check_afp_entries
+register
 echo "* Installation successful. Enjoy Isabelle/DOF, you can build the session"
 echo "  Isabelle/DOF and all example documents by executing:"
-echo "  $ISABELLE build -D ."
+echo "  $ISABELLE_TOOL build -D ."
 exit 0
--- a/src/scripts/build
+++ b/src/scripts/build
@ -33,6 +33,33 @@ NAME=${2:-root}

 ROOT_NAME="root_$NAME"

+install_dof_tex(){
+    cp $ISABELLE_DOF_HOME/src/document-templates/* .
+    cp $ISABELLE_DOF_HOME/src/DOF/*/*.sty .
+    cp $ISABELLE_DOF_HOME/src/ontologies/*/*.sty . 
+    
+    ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
+    sed -i -e "s|%%% CONFIG %%%| \
+      \\\\renewcommand{\\\\dof@isabelleversion}{$ISABELLE_SHORT_VERSION} \
+      \\\\renewcommand{\\\\isabellelatestversion}{$DOF_LATEST_ISABELLE} \
+      \\\\renewcommand{\\\\isabellefullversion}{$ISABELLE_VERSION\\\\xspace} \
+      \\\\renewcommand{\\\\dof@version}{$DOF_VERSION} \
+      \\\\renewcommand{\\\\doflatestversion}{$DOF_LATEST_VERSION} \
+      \\\\renewcommand{\\\\isadoflatestdoi}{$DOF_LATEST_DOI} \
+      \\\\renewcommand{\\\\isadofgenericdoi}{$DOF_GENERIC_DOI} \
+      \\\\renewcommand{\\\\isabelleurl}{$ISABELLE_URL} \
+      \\\\renewcommand{\\\\dofurl}{$DOF_URL} \
+      \\\\renewcommand{\\\\dof@artifacturl}{https://$DOF_ARTIFACT_HOST/$DOF_ARTIFACT_DIR}|" \
+      "DOF-core.sty"
+
+    
+    sed -i -e "s|<isadofurl>|$DOF_URL|" *.sty
+    sed -i -e "s|<isadofurl>|$DOF_URL|" *.tex
+    LTX_VERSION="$DOF_DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
+    sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.tex
+    sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.sty
+}
+
 [ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"

 if [ -f "$DIR/$ROOT_NAME.tex" ]; then 
@ -72,7 +99,9 @@ for o in $ONTOLOGY; do
  >&2 echo "\usepackage{DOF-$o}" >> ontologies.tex;
 done

-ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex"
+install_dof_tex
+
+ROOT="root-$TEMPLATE.tex"
 if [ ! -f $ROOT ]; then 
    >&2 echo ""
    >&2 echo "Error: Isabelle/DOF document setup not correct"
@ -83,8 +112,6 @@ if [ ! -f $ROOT ]; then
 fi

 cp $ROOT root.tex
-cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
-cp $ISABELLE_HOME_USER/DOF/document-template/*.sty .

 # delete outdated aux files from previous runs
 rm -f *.aux