Skip to content

Commit 42a88bc

Browse files
sanjit-bhattedinskiadpaco-aws
authored
docs: separate install instructions for pre-compiled binaries vs. building from source (rust-lang#1275)
Co-authored-by: Ted Kaminski <[email protected]> Co-authored-by: Adrian Palacios <[email protected]>
1 parent 3be9ed4 commit 42a88bc

File tree

4 files changed

+112
-90
lines changed

4 files changed

+112
-90
lines changed

‎docs/README.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
11
## Kani documentation development
22

3+
VS Code recognizes localhost URLs in the terminal and automatically offers to port-forward them for you.
4+
All you need to do is run `mdbook serve` and then click "Open in browser".
5+
6+
### Outside VS Code
7+
38
A good trick when developing Kani on a remote machine is to SSH forward to test documentation changes.
49

510
```

‎docs/src/SUMMARY.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
- [Getting started](./getting-started.md)
44
- [Installation](./install-guide.md)
5+
- [Building from source](./build-from-source.md)
56
- [Usage](./usage.md)
67
- [On a single file](./kani-single-file.md)
78
- [On a package](./cargo-kani.md)

‎docs/src/build-from-source.md

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
# Installing from source code
2+
3+
> If you were able to [install Kani](install-guide.md) normally, you do not need to build Kani from source.
4+
> You probably want to proceed to the [Kani tutorial](kani-tutorial.md).
5+
6+
## Dependencies
7+
8+
In general, the following dependencies are required to build Kani from source.
9+
10+
> **NOTE**: These dependencies may be installed by running the scripts shown
11+
> below and don't need to be manually installed.
12+
13+
1. Cargo installed via [rustup](https://rustup.rs/)
14+
2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.59.0)
15+
3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (>= 3.2)
16+
17+
Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
18+
19+
### Install dependencies on Ubuntu
20+
21+
Support is available for Ubuntu 18.04 and 20.04.
22+
The simplest way to install dependencies (especially if you're using a fresh VM)
23+
is following our CI scripts:
24+
25+
```
26+
# git clone [email protected]:model-checking/kani.git
27+
git clone https://github.com/model-checking/kani.git
28+
cd kani
29+
git submodule update --init
30+
./scripts/setup/ubuntu/install_deps.sh
31+
./scripts/setup/ubuntu/install_cbmc.sh
32+
./scripts/setup/install_viewer.sh 3.5
33+
./scripts/setup/install_rustup.sh
34+
# If you haven't already:
35+
source $HOME/.cargo/env
36+
```
37+
38+
### Install dependencies on macOS
39+
40+
Support is available for macOS 10.15. You need to have [Homebrew](https://brew.sh/) installed already.
41+
42+
```
43+
# git clone [email protected]:model-checking/kani.git
44+
git clone https://github.com/model-checking/kani.git
45+
cd kani
46+
git submodule update --init
47+
./scripts/setup/macos-10.15/install_deps.sh
48+
./scripts/setup/macos-10.15/install_cbmc.sh
49+
./scripts/setup/install_viewer.sh 3.5
50+
./scripts/setup/install_rustup.sh
51+
# If you haven't already:
52+
source $HOME/.cargo/env
53+
```
54+
55+
## Build and test Kani
56+
57+
Build the Kani package:
58+
59+
```
60+
cargo build --workspace
61+
```
62+
63+
Then, optionally, run the regression tests:
64+
65+
```
66+
./scripts/kani-regression.sh
67+
```
68+
69+
This script has a lot of noisy output, but on a successful run you'll see:
70+
71+
```
72+
All Kani regression tests completed successfully.
73+
```
74+
75+
## Adding Kani to your path
76+
77+
To use Kani from anywhere, add the Kani scripts to your path:
78+
79+
```bash
80+
export PATH=$(pwd)/scripts:$PATH
81+
```
82+
83+
## Next steps
84+
85+
If you're learning Kani for the first time, you may be interested in our [tutorial](kani-tutorial.md).

‎docs/src/install-guide.md

Lines changed: 21 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -1,112 +1,43 @@
11
# Installation
22

3-
To install the latest version of Kani, run:
4-
5-
```bash
6-
cargo install --locked kani-verifier
7-
cargo-kani setup
8-
```
3+
Kani offers an easy installation option on two platforms:
94

10-
This will build and place in `~/.cargo/bin` (in a typical environment) the `kani` and `cargo-kani` binaries.
11-
The second step (`cargo-kani setup`) will download the Kani compiler and other necessary dependencies (and place them under `~/.kani/`).
5+
* `x86_64-unknown-linux-gnu` (Most Linux distributions)
6+
* `x86_64-apple-darwin` (Intel Mac OS)
127

13-
Currently, only two platforms are supported:
8+
Other platforms are either not yet supported or require instead that you [build from source](build-from-source.md).
149

15-
* `x86_64-unknown-linux-gnu`
16-
* `x86_64-apple-darwin`
10+
## Dependencies
1711

1812
The following must already be installed:
1913

20-
* **Python version 3.8 or greater** and the package installer pip.
21-
* Rust installed via `rustup`
22-
* `ctags` is required for Kani's `--visualize` option to work correctly.
14+
* **Python version 3.6 or greater** and the package installer `pip`.
15+
* Rust installed via `rustup`.
16+
* `ctags` is required for Kani's `--visualize` option to work correctly. [Universal ctags](https://ctags.io/) is recommended.
17+
18+
## Installing the latest version
2319

24-
# Installing an older version of Kani
20+
To install the latest version of Kani, run:
2521

2622
```bash
27-
cargo install --lock kani-verifier --version <VERSION>
23+
cargo install --locked kani-verifier
2824
cargo-kani setup
2925
```
3026

31-
# Building from source
32-
33-
In general, the following dependencies are required.
34-
35-
> **NOTE**: These dependencies may be installed by running the CI scripts shown
36-
> below and there's no need to install them separately, for their respective
37-
> OS.
38-
39-
1. Cargo installed via [rustup](https://rustup.rs/)
40-
2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.59.0)
41-
3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (>= 3.5)
42-
43-
Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
44-
45-
## Install dependencies on Ubuntu
46-
47-
Support is available for Ubuntu 18.04 and 20.04.
48-
The simplest way to install dependencies (especially if you're using a fresh VM)
49-
is following our CI scripts:
50-
51-
```
52-
# git clone [email protected]:model-checking/kani.git
53-
git clone https://github.com/model-checking/kani.git
54-
cd kani
55-
git submodule update --init
56-
./scripts/setup/ubuntu/install_deps.sh
57-
./scripts/setup/ubuntu/install_cbmc.sh
58-
./scripts/setup/install_viewer.sh 3.5
59-
./scripts/setup/install_rustup.sh
60-
# If you haven't already:
61-
source $HOME/.cargo/env
62-
```
63-
64-
## Install dependencies on macOS
65-
66-
Support is available for macOS 10.15. You need to have [Homebrew](https://brew.sh/) installed already.
67-
68-
```
69-
# git clone [email protected]:model-checking/kani.git
70-
git clone https://github.com/model-checking/kani.git
71-
cd kani
72-
git submodule update --init
73-
./scripts/setup/macos-10.15/install_deps.sh
74-
./scripts/setup/macos-10.15/install_cbmc.sh
75-
./scripts/setup/install_viewer.sh 3.5
76-
./scripts/setup/install_rustup.sh
77-
# If you haven't already:
78-
source $HOME/.cargo/env
79-
```
80-
81-
## Build and test Kani
82-
83-
Build the Kani package:
84-
85-
```
86-
cargo build --workspace
87-
```
88-
89-
Then, optionally, run the regression tests:
90-
91-
```
92-
./scripts/kani-regression.sh
93-
```
94-
95-
This script has a lot of noisy output, but on a successful run you'll see:
96-
97-
```
98-
All Kani regression tests completed successfully.
99-
```
100-
101-
## Try running Kani
27+
This will build and place in `~/.cargo/bin` (in a typical environment) the `kani` and `cargo-kani` binaries.
28+
The second step (`cargo-kani setup`) will download the Kani compiler and other necessary dependencies (and place them under `~/.kani/`).
10229

103-
Add the Kani scripts to your path:
30+
## Installing an older version
10431

10532
```bash
106-
export PATH=$(pwd)/scripts:$PATH
33+
cargo install --lock kani-verifier --version <VERSION>
34+
cargo-kani setup
10735
```
10836

109-
Create a test file:
37+
## Checking your installation
38+
39+
After you've installed Kani,
40+
you can try running it by creating a test file:
11041

11142
```rust
11243
// File: test.rs

0 commit comments

Comments
 (0)