Changed user interface of the installation script: supports now long and short options and allows one to skipt the lengthy patch and afp installation check.
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
HOL-OCL/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
090b5f3e63
commit
00cb307fc5
14
README.md
14
README.md
|
@ -12,17 +12,27 @@ system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle201
|
||||||
|
|
||||||
## Installation
|
## Installation
|
||||||
|
|
||||||
|
### Quick Installation Guide
|
||||||
|
|
||||||
In most case, the DOF-plugin can be installed as follows:
|
In most case, the DOF-plugin can be installed as follows:
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ ./install
|
foo@bar:~$ ./install
|
||||||
```
|
```
|
||||||
If a specific Isabelle version should be used (i.e., not the default
|
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
|
one), the full path to the ``isabelle`` command needs to be passed as
|
||||||
argument to the ``install`` script:
|
using the ``-i`` command line argument of the ``install`` script:
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
|
foo@bar:~$ ./install -i /usr/local/Isabelle2017/bin/isabelle
|
||||||
```
|
```
|
||||||
|
|
||||||
|
For further command line options of the installer, please use the
|
||||||
|
built-in help:
|
||||||
|
```console
|
||||||
|
foo@bar:~$ ./install -h
|
||||||
|
```
|
||||||
|
|
||||||
|
### What The Installer Actually Does
|
||||||
|
|
||||||
The installer will
|
The installer will
|
||||||
* apply a patch to Isabelle that is necessary to use Isabelle/DOF.
|
* apply a patch to Isabelle that is necessary to use Isabelle/DOF.
|
||||||
If this patch installations fails, you need to manually replace
|
If this patch installations fails, you need to manually replace
|
||||||
|
|
56
install
56
install
|
@ -34,14 +34,32 @@ ISABELLE_VERSION="Isabelle2017: October 2017"
|
||||||
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2017/"
|
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2017/"
|
||||||
AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz"
|
AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz"
|
||||||
|
|
||||||
ISABELLE=${1:-`which isabelle`}
|
ISABELLE=`which isabelle`
|
||||||
GEN_DIR=document-generator
|
GEN_DIR=document-generator
|
||||||
|
PROG=`echo $0 | sed 's|.*/||'`;
|
||||||
|
ISABELLE_VERSION=`$ISABELLE version`
|
||||||
|
SKIP="false"
|
||||||
VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME ISABELLE_TOOLS`
|
VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME ISABELLE_TOOLS`
|
||||||
for i in $VARS; do
|
for i in $VARS; do
|
||||||
export "$i"
|
export "$i"
|
||||||
done
|
done
|
||||||
|
|
||||||
|
print_help()
|
||||||
|
{
|
||||||
|
echo "Usage: $PROG [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-patch-and-afp, -s skip installation of Isabelle/DOF patch for"
|
||||||
|
echo " Isabelle and required AFP entries. USE AT"
|
||||||
|
echo " YOUR OWN RISK (default: $SKIP)"
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
exit_error() {
|
exit_error() {
|
||||||
echo ""
|
echo ""
|
||||||
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
|
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
|
||||||
|
@ -51,10 +69,9 @@ exit_error() {
|
||||||
|
|
||||||
check_isabelle_version() {
|
check_isabelle_version() {
|
||||||
echo "* Checking Isabelle version:"
|
echo "* Checking Isabelle version:"
|
||||||
VERSION=`$ISABELLE version`
|
if [ "$ISABELLE_VERSION" != "$ISABELLE_VERSION" ]; then
|
||||||
if [ "$VERSION" != "$ISABELLE_VERSION" ]; then
|
|
||||||
echo " WARNING:"
|
echo " WARNING:"
|
||||||
echo " The version of Isabelle (i.e., $VERSION) you are using"
|
echo " The version of Isabelle (i.e., $ISABELLE_VERSION) you are using"
|
||||||
echo " IS NOT SUPPORTED"
|
echo " IS NOT SUPPORTED"
|
||||||
echo " by the current version of Isabelle/DOF. Please install a 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 " version of Isabelle and rerun the install script, providing the"
|
||||||
|
@ -71,7 +88,7 @@ check_isabelle_version() {
|
||||||
exit_error
|
exit_error
|
||||||
fi
|
fi
|
||||||
else
|
else
|
||||||
echo " Success: found supported Isabelle version ($VERSION)"
|
echo " Success: found supported Isabelle version ($ISABELLE_VERSION)"
|
||||||
fi
|
fi
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -189,11 +206,34 @@ install_and_register(){
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
while [ $# -gt 0 ]
|
||||||
|
do
|
||||||
|
case "$1" in
|
||||||
|
--isabelle|-i)
|
||||||
|
ISABELLE="$2";
|
||||||
|
shift;;
|
||||||
|
--skip-patch-and-afp|-s)
|
||||||
|
SKIP="true";;
|
||||||
|
--help|-h)
|
||||||
|
print_help
|
||||||
|
exit 0;;
|
||||||
|
*) print_help
|
||||||
|
exit 1;;
|
||||||
|
esac
|
||||||
|
shift
|
||||||
|
done
|
||||||
|
|
||||||
|
|
||||||
echo "Isabelle/DOF Installer"
|
echo "Isabelle/DOF Installer"
|
||||||
echo "======================"
|
echo "======================"
|
||||||
check_isabelle_version
|
check_isabelle_version
|
||||||
check_isa_dof_patch
|
if [ "$SKIP" = "true" ]; then
|
||||||
check_afp_entries
|
echo " Warning: skipping installation of Isabelle patch and AFP entries."
|
||||||
|
else
|
||||||
|
check_isa_dof_patch
|
||||||
|
check_afp_entries
|
||||||
|
fi
|
||||||
check_old_installation
|
check_old_installation
|
||||||
install_and_register
|
install_and_register
|
||||||
echo "* Installation successful. Enjoy Isabelle/DOF, you can now build the session"
|
echo "* Installation successful. Enjoy Isabelle/DOF, you can now build the session"
|
||||||
|
|
Loading…
Reference in New Issue