forked from Isabelle_DOF/Isabelle_DOF
Declared installation script as deprecated.
This commit is contained in:
parent
873151b4f3
commit
4e47c38860
17
README.md
17
README.md
|
@ -14,22 +14,9 @@ Isabelle/DOF has three major prerequisites:
|
||||||
system from the [Isabelle
|
system from the [Isabelle
|
||||||
website](http://isabelle.in.tum.de/website-Isabelle2022/).
|
website](http://isabelle.in.tum.de/website-Isabelle2022/).
|
||||||
* **AFP:** Isabelle/DOF requires two entries from the [Archive of
|
* **AFP:** Isabelle/DOF requires two entries from the [Archive of
|
||||||
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
|
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
|
||||||
AFP following the instructions given at
|
AFP following the instructions given at
|
||||||
<https://www.isa-afp.org/using.html>. For your convenience, we also
|
<https://www.isa-afp.org/using.html>.
|
||||||
provide a script that only installs the two entries required by
|
|
||||||
Isabelle/DOF into the local Isabelle/DOF directory. First, Isabelle/DOF
|
|
||||||
needs to be registered as an Isabelle component:
|
|
||||||
|
|
||||||
```console
|
|
||||||
foo@bar:~$ isabelle components -u `pwd`
|
|
||||||
```
|
|
||||||
|
|
||||||
Thereafter, the AFP entries can be installed as follows:
|
|
||||||
|
|
||||||
```console
|
|
||||||
foo@bar:~$ isabelle env ./install-afp
|
|
||||||
```
|
|
||||||
|
|
||||||
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
|
* **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.
|
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
|
||||||
|
|
23
install-afp
23
install-afp
|
@ -35,6 +35,8 @@ print_help()
|
||||||
{
|
{
|
||||||
echo "Usage: isabelle env ./install-afp [OPTION] "
|
echo "Usage: isabelle env ./install-afp [OPTION] "
|
||||||
echo ""
|
echo ""
|
||||||
|
echo "Warning: This tools is deprecated."
|
||||||
|
echo ""
|
||||||
echo "Run ..."
|
echo "Run ..."
|
||||||
echo ""
|
echo ""
|
||||||
echo " --help, -h display this help message"
|
echo " --help, -h display this help message"
|
||||||
|
@ -44,11 +46,29 @@ print_help()
|
||||||
|
|
||||||
exit_error() {
|
exit_error() {
|
||||||
echo ""
|
echo ""
|
||||||
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
|
echo " *** Local AFP installation FAILED, please check the README.md for help ***"
|
||||||
echo ""
|
echo ""
|
||||||
exit 1
|
exit 1
|
||||||
}
|
}
|
||||||
|
|
||||||
|
confirm_usage() {
|
||||||
|
echo "* From Isabelle2021-1 on, the recommended method for making the whole AFP "
|
||||||
|
echo " available to Isabelle is the isabelle components -u command."
|
||||||
|
echo " For doing so, please follow the instructions at: "
|
||||||
|
echo " https://www.isa-afp.org/help/"
|
||||||
|
echo ""
|
||||||
|
echo " Alternatively, you can continue, on your own risk, to install only"
|
||||||
|
echo " the AFP entries required to run Isabelle/DOF."
|
||||||
|
echo ""
|
||||||
|
read -p " Still continue (y/N)? " -n 1 -r
|
||||||
|
echo
|
||||||
|
if [[ $REPLY =~ ^[Yy]$ ]];
|
||||||
|
then
|
||||||
|
echo " Continuing installation on your OWN risk."
|
||||||
|
else
|
||||||
|
exit_error
|
||||||
|
fi
|
||||||
|
}
|
||||||
check_isabelle_version() {
|
check_isabelle_version() {
|
||||||
echo "* Checking Isabelle version:"
|
echo "* Checking Isabelle version:"
|
||||||
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
|
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
|
||||||
|
@ -149,6 +169,7 @@ AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
||||||
echo ""
|
echo ""
|
||||||
echo "Isabelle/DOF AFP Installation Utility"
|
echo "Isabelle/DOF AFP Installation Utility"
|
||||||
echo "====================================="
|
echo "====================================="
|
||||||
|
confirm_usage
|
||||||
check_isabelle_version
|
check_isabelle_version
|
||||||
check_afp_entries
|
check_afp_entries
|
||||||
echo "* AFP Installation successful."
|
echo "* AFP Installation successful."
|
||||||
|
|
Loading…
Reference in New Issue