From dfa2581f06c89fc546dbb7d2329f00e815386587 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 5 Jan 2019 21:44:51 +0000 Subject: [PATCH] Added checks for AFP entries and Isabelle/DOF patch. --- install | 158 ++++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 109 insertions(+), 49 deletions(-) diff --git a/install b/install index 8a61700..1e66a69 100755 --- a/install +++ b/install @@ -1,5 +1,5 @@ #!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. +# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved. # 2018 The University of Paris-Sud. All rights reserved. # # Redistribution and use in source and binary forms, with or without @@ -28,63 +28,123 @@ set -e +# Global configuration +ISABELLE_VERSION="Isabelle2017: October 2017" +ISABELLE_URL="http://isabelle.in.tum.de/website-Isabelle2017/" +AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz" + ISABELLE=${1:-`which isabelle`} export `$ISABELLE getenv ISABELLE_HOME_USER` export `$ISABELLE getenv ISABELLE_TOOLS` - GEN_DIR=document-generator +check_isabelle_version() { + echo "* Checking Isabelle version:" + VERSION=`$ISABELLE version` + if [ "$VERSION" != "$ISABELLE_VERSION" ]; then + echo " WARNING:" + echo " The version of Isabelle (i.e., $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\" binary as argument." + echo " Isabelle 2017 can be obtained from:" + echo " $ISABELLE_URL" + echo + read -p " Still continue (y/N)? " -n 1 -r + echo + if [[ $REPLY =~ ^[Yy]$ ]]; + then + echo " Continuing installation on your OWN risk." + else + exit 1 + fi + else + echo " Success: found supported Isabelle version ($VERSION)" + fi +} -VERSION=`$ISABELLE version` -if [ "$VERSION" != "Isabelle2017: October 2017" ]; then - echo "Warning, the version of Isabelle (i.e., $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\" binary as argument." - echo - read -p "Still continue (y/N)? " -n 1 -r - echo - if [[ $REPLY =~ ^[Yy]$ ]] - then - echo "Continuing installation on your OWN risk." - else - exit 1 - fi -fi +check_afp_entries() { + echo "* Checking availability of AFP entries:" + for afp in Regular-Sets Functional-Automata; do + res=`$ISABELLE build -n -d . $afp 2>/dev/null || true` + if [ "$res" != "" ]; then + echo " Success: found APF entry $afp." + else + echo " FAILURE: could not find AFP entry $afp." + echo " Please obtain the AFP from" + echo " $AFP_URL" + echo " and follow the following instructions:" + echo " https://www.isa-afp.org/using.html" + exit 1 + fi + done +} -if [[ -d "$ISABELLE_HOME_USER/DOF" ]]; then - echo "Moving old installation to $DIR/settings $ISABELLE_HOME_USER/DOF.bak" - rm -rf "$ISABELLE_HOME_USER/DOF.bak" - mv "$ISABELLE_HOME_USER/DOF" "$ISABELLE_HOME_USER/DOF.bak" -fi +check_isa_dof_patch() { + echo "* Check availabilty of Isabelle/DOF patch:" + if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then + echo " Success: Isabelle is already patched" + else + export `isabelle getenv ISABELLE_HOME_USER` + echo " FAILURE: Isabelle/DOF patch is not available." + echo " Please copy patches/thy_output.ML to $ISABELLE_HOME/src/Pure/Thy/:" + echo " cp patches/thy_output.ML $ISABELLE_HOME/src/Pure/Thy/" + echo " and rebuild Isabelle/HOL." + exit 1 + fi +} -DIR="$ISABELLE_HOME_USER/DOF/Tools" -echo "Installing Tools in $DIR" -mkdir -p "$DIR" -cp $GEN_DIR/Tools/* "$DIR" -chmod 755 "$DIR"/* +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 instllation found." + fi -# Register Tools -DIR="$ISABELLE_HOME_USER/etc" -mkdir -p "$DIR" -if [[ $ISABELLE_TOOLS = *DOF* ]]; then - echo "Tools already registered in $DIR/settings" -else - echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \ - >> "$DIR/settings" - echo "Registering tools in Tools already registered in $DIR/settings" -fi +} -DIR="$ISABELLE_HOME_USER/DOF/document-template" -echo "Installing document templates in $DIR" -mkdir -p "$DIR" -cp $GEN_DIR/document-template/* "$DIR" +install_and_register(){ + echo "* Installing Isabelle/DOF" + + DIR="$ISABELLE_HOME_USER/DOF/Tools" + echo " - Installing Tools in $DIR" + mkdir -p "$DIR" + cp $GEN_DIR/Tools/* "$DIR" + chmod 755 "$DIR"/* + + DIR="$ISABELLE_HOME_USER/DOF/document-template" + echo " - Installing document templates in $DIR" + mkdir -p "$DIR" + cp $GEN_DIR/document-template/* "$DIR" + + DIR="$ISABELLE_HOME_USER/DOF/latex" + echo " - Installing LaTeX styles in $DIR" + mkdir -p "$DIR" + cp $GEN_DIR/latex/*.sty "$DIR" + + DIR="$ISABELLE_HOME_USER/etc" + echo " - Registering Isabelle/DOF" + mkdir -p "$DIR" + if [[ $ISABELLE_TOOLS = *DOF* ]]; then + echo " * Tools already registered in $DIR/settings" + else + echo " * Registering tools in Tools already registered in $DIR/settings" + echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \ + >> "$DIR/settings" + fi +} -DIR="$ISABELLE_HOME_USER/DOF/latex" -echo "Installing LaTeX styles in $DIR" -mkdir -p "$DIR" -cp $GEN_DIR/latex/*.sty "$DIR" - -echo "Installation successful." +echo "Isabelle/DOF Installer" +echo "======================" +check_isabelle_version +check_isa_dof_patch +check_afp_entries +check_old_installation +install_and_register +echo "* Installation successful" +exit 1