2020-12-02 01:32:26 +00:00
|
|
|
<!--
|
|
|
|
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
|
|
|
|
|
|
|
SPDX-License-Identifier: CC-BY-SA-4.0
|
|
|
|
-->
|
|
|
|
|
|
|
|
<!-- This file is also included on https://docs.sel4.systems/projects/buildsystem/host-dependencies.html -->
|
|
|
|
|
|
|
|
# Proof and Isabelle Dependencies
|
|
|
|
|
|
|
|
## Proof Dependencies
|
|
|
|
|
|
|
|
### Linux Packages - Debian
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
On **Buster** or **Bullseye**, to run all proofs against the
|
|
|
|
**ARMv7-A** architecture you will need to install the following packages:
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
```bash
|
|
|
|
sudo apt-get install \
|
|
|
|
python3 python3-pip python3-dev \
|
|
|
|
gcc-arm-none-eabi build-essential libxml2-utils ccache \
|
|
|
|
ncurses-dev librsvg2-bin device-tree-compiler cmake \
|
|
|
|
ninja-build curl zlib1g-dev texlive-fonts-recommended \
|
|
|
|
texlive-latex-extra texlive-metapost texlive-bibtex-extra \
|
|
|
|
rsync
|
|
|
|
```
|
|
|
|
|
|
|
|
There is no package for the MLton compiler on Buster or Bullseye, so you will
|
|
|
|
need to install it from the [MLton website](http://www.mlton.org).
|
|
|
|
|
|
|
|
The Haskell Stack package is unavailable on Bullseye and out-of-date on Buster,
|
|
|
|
so you will need to install it from the [Haskell Stack
|
|
|
|
website](https://docs.haskellstack.org/en/stable/README).
|
|
|
|
|
|
|
|
### Linux Packages - Ubuntu
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
On **Ubuntu 18.04**, to run all proofs against the **ARMv7-A**
|
|
|
|
architecture you will need to install the following packages:
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
```bash
|
|
|
|
sudo apt-get install \
|
|
|
|
python3 python3-pip python3-dev \
|
|
|
|
gcc-arm-none-eabi build-essential libxml2-utils ccache \
|
|
|
|
ncurses-dev librsvg2-bin device-tree-compiler cmake \
|
|
|
|
ninja-build curl zlib1g-dev texlive-fonts-recommended \
|
|
|
|
texlive-latex-extra texlive-metapost texlive-bibtex-extra \
|
|
|
|
mlton-compiler haskell-stack
|
|
|
|
```
|
|
|
|
|
|
|
|
### Python
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
The build system for the seL4 kernel requires several python packages:
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
```bash
|
|
|
|
sudo pip3 install --upgrade pip
|
|
|
|
sudo pip3 install sel4-deps
|
|
|
|
```
|
|
|
|
|
|
|
|
### Haskell Stack
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
After installing
|
|
|
|
[haskell-stack](https://docs.haskellstack.org/en/stable/README), make sure
|
|
|
|
you've adjusted your `PATH` to include `$HOME/.local/bin`, and that you're
|
|
|
|
running an up-to-date version:
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
```bash
|
|
|
|
stack upgrade --binary-only
|
|
|
|
which stack # should be $HOME/.local/bin/stack
|
|
|
|
```
|
|
|
|
|
|
|
|
### MacOS
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
Other than the cross-compiler `gcc` toolchain, setup on MacOS should be similar
|
|
|
|
to that on Ubuntu. To set up a cross-compiler, try the following:
|
2021-05-17 02:39:54 +00:00
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
* Install `XCode` from the AppStore and its command line tools. If you are
|
2021-05-17 02:39:54 +00:00
|
|
|
running MacPorts or homebrew, you have these already. Otherwise, after you have XCode
|
2020-12-02 01:32:26 +00:00
|
|
|
installed, run `gcc --version` in a terminal window. If it reports a version,
|
|
|
|
you're set. Otherwise it should pop up a window and prompt for installation
|
|
|
|
of the command line tools.
|
|
|
|
* Install the seL4 Python dependencies, for instance using `sudo easy_install
|
|
|
|
sel4-deps`. `easy_install` is part of Python's [`setuptools`][setuptools].
|
|
|
|
* Install the [`misc/scripts/cpp`][cpp-script] wrapper for clang, by
|
|
|
|
putting it in `~/bin`, or somewhere else in your `PATH`.
|
|
|
|
|
|
|
|
[setuptools]: https://pypi.python.org/pypi/setuptools "python package installer"
|
|
|
|
[cpp-script]: https://github.com/seL4/l4v/blob/master/misc/scripts/cpp "cpp wrapper script"
|
|
|
|
|
|
|
|
## Isabelle Setup
|
|
|
|
|
|
|
|
After the repository is set up using `repo` with
|
|
|
|
`seL4/verification-manifest`, you should have following directory
|
|
|
|
structure, where `l4v` is the repository you are currently looking at:
|
|
|
|
|
|
|
|
```bash
|
|
|
|
verification/
|
2021-05-17 02:39:54 +00:00
|
|
|
HOL4/
|
|
|
|
graph-refine/
|
2020-12-02 01:32:26 +00:00
|
|
|
isabelle/
|
|
|
|
l4v/
|
|
|
|
seL4/
|
|
|
|
```
|
|
|
|
|
|
|
|
To set up Isabelle for use in `l4v/`, assuming you have no previous
|
|
|
|
installation of Isabelle, run the following commands in the directory
|
|
|
|
`verification/l4v/`:
|
|
|
|
|
|
|
|
```bash
|
|
|
|
mkdir -p ~/.isabelle/etc
|
|
|
|
cp -i misc/etc/settings ~/.isabelle/etc/settings
|
|
|
|
./isabelle/bin/isabelle components -a
|
|
|
|
./isabelle/bin/isabelle jedit -bf
|
|
|
|
./isabelle/bin/isabelle build -bv HOL-Word
|
|
|
|
```
|
|
|
|
|
|
|
|
These commands perform the following steps:
|
|
|
|
|
2021-05-17 02:39:54 +00:00
|
|
|
* create an Isabelle user settings directory.
|
|
|
|
* install L4.verified Isabelle settings.
|
|
|
|
These settings initialise the Isabelle installation to use the standard
|
|
|
|
Isabelle `contrib` tools from the Munich Isabelle repository and set up
|
|
|
|
paths such that multiple Isabelle repository installations can be used
|
|
|
|
side by side without interfering with each other.
|
|
|
|
* download `contrib` components from either the Munich or TS repository. This includes
|
|
|
|
Scala, a Java JDK, PolyML, and multiple external provers. You should
|
|
|
|
download these, even if you have these tools previously installed
|
|
|
|
elsewhere to make sure you have the right versions. Depending on your
|
|
|
|
internet connection, this may take some time.
|
|
|
|
* compile and build the Isabelle PIDE jEdit interface.
|
|
|
|
* build basic Isabelle images, including `HOL-Word` to ensure that
|
|
|
|
the installation works. This may take a few minutes.
|
2020-12-02 01:32:26 +00:00
|
|
|
|
|
|
|
Alternatively, it is possible to use the official Isabelle2020 release
|
|
|
|
bundle for your platform from the [Isabelle website][isabelle]. In this case, the
|
|
|
|
installation steps above can be skipped, and you would replace the directory
|
|
|
|
`verification/isabelle/` with a symbolic link to the Isabelle home directory
|
|
|
|
of the release version. Note that this is not recommended for development,
|
|
|
|
since Google repo will overwrite this link when you synchronise repositories
|
|
|
|
and Isabelle upgrades will have to be performed manually as development
|
|
|
|
progresses.
|
|
|
|
|
2021-08-06 06:33:35 +00:00
|
|
|
## PIDE Tools
|
|
|
|
|
|
|
|
The following tools and tips can make writing proofs easier and more efficient
|
|
|
|
when using the Isabelle PIDE jEdit interface.
|
|
|
|
|
|
|
|
### WhiteSpace plugin
|
|
|
|
|
|
|
|
The WhiteSpace plugin can highlight normally invisible whitespace characters
|
|
|
|
such as tabs and spaces, and can remove trailing whitespace on save. To
|
|
|
|
install and configure the WhiteSpace plug-in for jEdit, follow
|
|
|
|
the instructions below.
|
|
|
|
|
|
|
|
1. Go to Plugins -> Plugin manager -> Install.
|
|
|
|
2. Search for `WhiteSpace` and install the plugin.
|
|
|
|
3. Go to Plugins -> Plugin Options -> WhiteSpace -> On save actions.
|
|
|
|
4. Check "Remove trailing whitespace" and click Apply.
|
|
|
|
|
|
|
|
### Key bindings for Navigator
|
|
|
|
|
|
|
|
The Isabelle PIDE provides "Back" and "Forward" actions that allow you to
|
|
|
|
easily navigate to previous positions in your edit history. Follow the steps
|
|
|
|
below to bind a key to the "Back" function. We recommend ``[ctrl]+[`]``.
|
|
|
|
|
|
|
|
1. Go to Utilities -> Global Options -> jEdit -> Shortcuts.
|
|
|
|
2. Select Action Set -> Plugin: Navigator.
|
|
|
|
3. Set a shortcut for `Back`.
|
|
|
|
|
|
|
|
### Go-to-error macro
|
|
|
|
|
|
|
|
Run the following commands in the directory `verification/l4v/`:
|
|
|
|
|
|
|
|
```
|
|
|
|
mkdir -p ~/.isabelle/jedit/macros
|
|
|
|
cp misc/jedit/macros/goto-error.bsh ~/.isabelle/jedit/macros/.
|
|
|
|
```
|
|
|
|
|
|
|
|
You can add keybindings for this macro in the usual way, by going to
|
|
|
|
Utilities -> Global Options -> jEdit -> Shortcuts.
|
|
|
|
|
2020-12-02 01:32:26 +00:00
|
|
|
[isabelle]: http://isabelle.in.tum.de
|