nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added checks for AFP entries and Isabelle/DOF patch.

This commit is contained in:
Achim D. Brucker 2019-01-05 21:44:51 +00:00
parent 530727cccd
commit dfa2581f06
1 changed files with 109 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

158
install
View File

@ -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