Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Include AFP download and registration in installer.

This commit is contained in:
Achim D. Brucker 2019-01-06 13:23:42 +00:00
parent f2d3ff9918
commit c8a69afc4c
2 changed files with 34 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
README.md
View File

@ -6,28 +6,10 @@ well as formal development.
## Prerequisites
### Isabelle 2017
Isabelle/DOF requires [Isabelle 2017](http://isabelle.in.tum.de/website-Isabelle2017/).
Please download the Isabelle 2017 distribution for your operating
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2017/).
### AFP Entries
Moreover, Isabelle/DOF requires the two entries from the Archive of
Formal Proofs. Please download the [AFP for Isabelle
2017](https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz")
and follow the [instructions for installing the AFP as Isabelle
component](https://www.isa-afp.org/using.html). If you have extracted
the AFP archive into the directory to `/home/myself/afp`, you should
run the following command to make the AFP session `ROOTS` available to
Isabelle:
```console
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
```
## Installation
In most case, the DOF-plugin can be installed as follows:
@ -50,6 +32,18 @@ The installer will
```console
cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/
```
* install required entries from the [AFP](https://www.isa-afp.org). If this
installations fails, you need to manually install the AFP for Isabelle 2017 as follows:
Download the [AFP for Isabelle 2017](https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz")
and follow the [instructions for installing the AFP as Isabelle
component](https://www.isa-afp.org/using.html). If you have extracted
the AFP archive into the directory to `/home/myself/afp`, you should
run the following command to make the AFP session `ROOTS` available to
Isabelle:
```console
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
```
* install the Isabelle/DOF-plugin into the Isabelle user directory
(the exact location depends on the Isabelle version).

25
install
View File

@ -77,19 +77,38 @@ check_isabelle_version() {
check_afp_entries() {
echo "* Checking availability of AFP entries:"
for afp in Regular-Sets Functional-Automata; do
missing=""
required="Regular-Sets Functional-Automata"
for afp in $required; 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 " Warning: could not find AFP entry $afp."
missing="$missing $afp"
fi
done
if [ "$missing" != "" ]; then
echo " Trying to install AFP (this might take a few *minutes*) ...."
extract=""
for e in $missing; do
extract="$extract afp-2018-08-14/thys/$e"
done
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
for e in $missing; do
echo " Registering $e in $ISABELLE_HOME_USER/ROOTS"
echo "$PWD/.afp/afp-2018-08-14/thys/$e" >> $ISABELLE_HOME_USER/ROOTS
done
echo " AFP installation successful."
else
echo " FAILURE: could not find AFP entries: $missing."
echo " Please obtain the AFP from"
echo " $AFP_URL"
echo " and follow the following instructions:"
echo " https://www.isa-afp.org/using.html"
exit_error
fi
done
fi
}
check_isa_dof_patch() {