diff --git a/.config b/.config deleted file mode 100755 index a1fe6ea..0000000 --- a/.config +++ /dev/null @@ -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" -# diff --git a/.woodpecker/build.yml b/.woodpecker/build.yml index d42f588..d5cb258 100644 --- 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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 82c683f..81aaea9 100644 --- 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 diff --git a/README.md b/README.md index 4a4524c..82e9fc3 100755 --- 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 + . 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 . diff --git a/etc/settings b/etc/settings index 1db5e3c..1c5f8f8 100644 --- 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" +# diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index a70109b..febd0ec 100755 --- 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]\Installing \<^isadof>\ text\ 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>\install\ script. + installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\install-afp\ script. We start by extracting the \<^isadof> archive: @{boxed_bash [display]\ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\} This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution. -Next, we need to invoke the \<^boxed_bash>\install\ script. If necessary, the installation -automatically downloads additional dependencies from the AFP (\<^url>\https://www.isa-afp.org\), -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>\write permissions for the Isabelle system directory\ and registers \<^isadof> as -Isabelle component. -If the \<^boxed_bash>\isabelle\ tool is not in your \<^boxed_bash>\PATH\, you need to call the - \<^boxed_bash>\install\ script with the \<^boxed_bash>\--isabelle\ option, passing the full-qualified -path of the \<^boxed_bash>\isabelle\ tool ( \<^boxed_bash>\install --help\ gives -you an overview of all available configuration options): +\<^isadof> depends on the the AFP (\<^url>\https://www.isa-afp.org\), 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>\https://www.isa-afp.org/using.html\), +or use the provided \<^boxed_bash>\install\ script to install a minimal AFP +setup into the local \<^isadof> directory. The script needs to be prefixed with the +\<^boxed_bash>\isabelle env\ command: @{boxed_bash [display]\ë\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:\} @{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 . \} diff --git a/install b/install-afp similarity index 59% rename from install rename to install-afp index cab4054..fe7038e 100755 --- a/install +++ b/install-afp @@ -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||$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/* - LTX_VERSION="$DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION" - sed -i -e "s||$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 diff --git a/src/scripts/build b/src/scripts/build index 8571a6d..248d36f 100755 --- 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||$DOF_URL|" *.sty + sed -i -e "s||$DOF_URL|" *.tex + LTX_VERSION="$DOF_DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION" + sed -i -e "s||$LTX_VERSION|" *.tex + sed -i -e "s||$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