Migration to Isabelle 2019.
Isabelle_DOF/Isabelle_DOF/Isabelle2019 There was a failure building this commit
Details
Isabelle_DOF/Isabelle_DOF/Isabelle2019 There was a failure building this commit
Details
This commit is contained in:
parent
c7d277b9da
commit
39afa24591
|
@ -24,7 +24,7 @@
|
|||
#
|
||||
# SPDX-License-Identifier: BSD-2-Clause
|
||||
|
||||
FROM logicalhacking:isabelle2018
|
||||
FROM logicalhacking:isabelle2019
|
||||
|
||||
WORKDIR /home/isabelle
|
||||
COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
|
||||
|
|
16
README.md
16
README.md
|
@ -6,9 +6,9 @@ well as formal development.
|
|||
|
||||
## Prerequisites
|
||||
|
||||
Isabelle/DOF requires [Isabelle 2018](http://isabelle.in.tum.de/website-Isabelle2018/).
|
||||
Please download the Isabelle 2018 distribution for your operating
|
||||
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2018/).
|
||||
Isabelle/DOF requires [Isabelle 2019](http://isabelle.in.tum.de/website-Isabelle2019/).
|
||||
Please download the Isabelle 2019 distribution for your operating
|
||||
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2019/).
|
||||
|
||||
## Installation
|
||||
|
||||
|
@ -22,7 +22,7 @@ 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
|
||||
using the ``-i`` command line argument of the ``install`` script:
|
||||
```console
|
||||
foo@bar:~$ ./install -i /usr/local/Isabelle2018/bin/isabelle
|
||||
foo@bar:~$ ./install -i /usr/local/Isabelle2019/bin/isabelle
|
||||
```
|
||||
|
||||
For further command line options of the installer, please use the
|
||||
|
@ -36,22 +36,22 @@ foo@bar:~$ ./install -h
|
|||
The installer will
|
||||
* apply a patch to Isabelle that is necessary to use Isabelle/DOF.
|
||||
If this patch installations fails, you need to manually replace
|
||||
the file ``Isabelle2018/src/Pure/Thy/thy_output.ML`` in the Isabelle
|
||||
the file ``Isabelle2019/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 required entries from the [AFP](https://www.isa-afp.org). If this
|
||||
installations fails, you need to manually install the AFP for Isabelle 2018 as follows:
|
||||
Download the [AFP for Isabelle 2018](https://sourceforge.net/projects/afp/files/afp-Isabelle2018/afp-2019-06-04.tar.gz)
|
||||
installations fails, you need to manually install the AFP for Isabelle 2019 as follows:
|
||||
Download the [AFP for Isabelle 2019](https://www.isa-afp.org/release/afp-2019-06-17.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/Isabelle2018/ROOTS
|
||||
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2019/ROOTS
|
||||
```
|
||||
* install the Isabelle/DOF-plugin into the Isabelle user directory
|
||||
(the exact location depends on the Isabelle version).
|
||||
|
|
8
install
8
install
|
@ -31,11 +31,11 @@
|
|||
shopt -s nocasematch
|
||||
|
||||
# Global configuration
|
||||
ISABELLE_VERSION="Isabelle2018: August 2018"
|
||||
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2018/"
|
||||
ISABELLE_VERSION="Isabelle2019: June 2019"
|
||||
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2019/"
|
||||
|
||||
AFP_DATE="afp-2019-06-04"
|
||||
AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2018/"$AFP_DATE".tar.gz"
|
||||
AFP_DATE="afp-2019-06-17"
|
||||
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
||||
|
||||
print_help()
|
||||
{
|
||||
|
|
Loading…
Reference in New Issue