forked from Isabelle_DOF/Isabelle_DOF
Installer now applyes Isabelle/DOF patch during installation.
This commit is contained in:
parent
3ca1c13dea
commit
2c121e573c
25
README.md
25
README.md
|
@ -12,14 +12,6 @@ Isabelle/DOF requires [Isabelle 2017](http://isabelle.in.tum.de/website-Isabelle
|
||||||
Please download the Isabelle 2017 distribution for your operating
|
Please download the Isabelle 2017 distribution for your operating
|
||||||
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2017/).
|
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2017/).
|
||||||
|
|
||||||
After unpacking the Isabelle distribution, replace the file
|
|
||||||
``Isabelle2017/src/Pure/Thy/thy_output.ML`` in the Isabelle
|
|
||||||
distribution with the file ``patches/thy_output.ML`` from the
|
|
||||||
Isabelle/DOF distribution:
|
|
||||||
|
|
||||||
```console
|
|
||||||
cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/
|
|
||||||
```
|
|
||||||
|
|
||||||
### AFP Entries
|
### AFP Entries
|
||||||
|
|
||||||
|
@ -33,7 +25,7 @@ run the following command to make the AFP session `ROOTS` available to
|
||||||
Isabelle:
|
Isabelle:
|
||||||
|
|
||||||
```console
|
```console
|
||||||
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2018/ROOTS
|
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
|
||||||
```
|
```
|
||||||
|
|
||||||
## Installation
|
## Installation
|
||||||
|
@ -49,8 +41,19 @@ argument to the ``install`` script:
|
||||||
foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
|
foo@bar:~$ ./install /usr/local/Isabelle2017/bin/isabelle
|
||||||
```
|
```
|
||||||
|
|
||||||
The DOF-plugin will be installed in the Isabelle user directory
|
The installer will
|
||||||
(the exact location depends on the Isabelle version).
|
* apply a patch to Isabelle that is necessary to use Isabelle/DOF.
|
||||||
|
If this patch installations fails, you need to manually replace
|
||||||
|
the file ``Isabelle2017/src/Pure/Thy/thy_output.ML`` in the Isabelle
|
||||||
|
distribution with the file ``patches/thy_output.ML`` from the
|
||||||
|
Isabelle/DOF distribution:
|
||||||
|
```console
|
||||||
|
cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/
|
||||||
|
```
|
||||||
|
|
||||||
|
* install the Isabelle/DOF-plugin into the Isabelle user directory
|
||||||
|
(the exact location depends on the Isabelle version).
|
||||||
|
* check that the AFP has been installed successfully.
|
||||||
|
|
||||||
## Usage
|
## Usage
|
||||||
|
|
||||||
|
|
29
install
29
install
|
@ -27,6 +27,7 @@
|
||||||
# SPDX-License-Identifier: BSD-2-Clause
|
# SPDX-License-Identifier: BSD-2-Clause
|
||||||
|
|
||||||
set -e
|
set -e
|
||||||
|
shopt -s nocasematch
|
||||||
|
|
||||||
# Global configuration
|
# Global configuration
|
||||||
ISABELLE_VERSION="Isabelle2017: October 2017"
|
ISABELLE_VERSION="Isabelle2017: October 2017"
|
||||||
|
@ -86,14 +87,28 @@ check_afp_entries() {
|
||||||
|
|
||||||
check_isa_dof_patch() {
|
check_isa_dof_patch() {
|
||||||
echo "* Check availabilty of Isabelle/DOF patch:"
|
echo "* Check availabilty of Isabelle/DOF patch:"
|
||||||
if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then
|
src="patches/thy_output.ML"
|
||||||
echo " Success: Isabelle is already patched"
|
dst="$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"
|
||||||
|
if [[ $(md5sum "$src") = $(md5sum "$dst") ]]; then
|
||||||
|
echo " Success: latest Isabelle/DOF patch already applied"
|
||||||
|
if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then
|
||||||
|
true
|
||||||
|
else
|
||||||
|
echo " Success: Warning: Isabelle/HOL needs to be rebuild to activate patch."
|
||||||
|
fi
|
||||||
else
|
else
|
||||||
echo " FAILURE: Isabelle/DOF patch is not available."
|
echo " Warning: Isabelle/DOF patch is not available or outdated."
|
||||||
echo " Please copy patches/thy_output.ML to $ISABELLE_HOME/src/Pure/Thy/:"
|
echo " Trying to patch system ...."
|
||||||
echo " cp patches/thy_output.ML $ISABELLE_HOME/src/Pure/Thy/"
|
if (cp $dst $dst.backup-by-isadof-installer && cp -f $src $dst) &> /dev/null; then
|
||||||
echo " and rebuild Isabelle/HOL."
|
echo " Applied patch successfully, Isabelle/HOL will be rebuilt during"
|
||||||
exit 1
|
echo " the next start of Isabelle."
|
||||||
|
else
|
||||||
|
echo " FAILURE: Could not apply Isabelle/DOF patch."
|
||||||
|
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
|
||||||
fi
|
fi
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Reference in New Issue