1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
Building Sail on Ubuntu and macOS
=========================
This note lists the commands needed to get Sail and all dependencies
working and built from source on a new Ubuntu install or macOS. We
have recently (2018-02-17) tested these on Xubuntu 16.04 LTS in a
virtual machine and on macOS Sierra 10.12.6, so they should
work. Hopefully this will be useful as a reference.
For most users, installing and building the dependencies using OPAM is
likely easier than building everything manually, see [INSTALL.md](INSTALL.md).
Basics
------
First we need some basic packages if they're not already installed.
For Ubuntu:
```
sudo apt-get install build-essential git
```
For macOS: compilers and supporting utilities are called Xcode instead of build-essential. First, download Xcode from the Mac App Store, and then run the following in the terminal:
```
xcode-select --install
```
git can be installed using ```brew install git```
OCaml and sail expect some packages. m4 is for OPAM, libgmp-dev is for
zarith which most of our tools rely on. Sail uses Z3 as a constraint
solver.
```
sudo apt-get install m4 libgmp-dev z3
```
For macOS: ```brew install m4 gmp z3```
OCaml and OPAM
--------------
Install OPAM. Either directly from [https://opam.ocaml.org] or from
the package manager - both should work, but we used the install script
from the website. ```opam init``` must be run after installing OPAM.
Distributions often contain quite outdated OCaml packages, so we need to make sure that we use an up-to-date OCaml compiler with opam:
```
opam switch 4.06.1
```
For opam versions >=2.0 the command syntax for opam switch is slightly different:
```
opam switch create ocaml-base-compiler.4.06.1
```
After doing opam switch it is important to check that the ocaml tools in your $PATH point at the opam installed toolchain, rather than any installed by the distribution package manager.
The `opam` file in the Sail repository specifies the required dependencies:
```
depends: [
"ocamlfind"
"ocamlbuild"
"zarith"
"menhir"
"linenoise" {>= "1.1.0"}
"ott" {>= "0.28"}
"lem" {>= "2018-12-14"}
"linksem" {>= "0.3"}
"omd"
"conf-gmp"
"conf-zlib"
"base64" {< "3.0.0"}
"yojson"
"pprint"
]
```
each of which can be installed using `opam install`. The `opam pin` command can be used to select a specific version of a dependency.
Ott
---
Before cloning the repositories you may need to set up ssh keys with
github or use https. Create a directory to install the various REMS
tools and cd into it.
```
git clone git@github.com:ott-lang/ott.git
cd ott
make
cd ..
```
Sail depends on ott, so add the ott executable (``` path-to-ott/bin```) in the $PATH.
Lem
---
If you are using OCaml 4.06, you'll need to run `opam install num` before building lem.
```
git clone git@github.com:rems-project/lem.git
cd lem
make
cd ocaml-lib
make install
cd ../..
```
Linksem
-------
Before installing linksem, we are required to set the LEMLIB environment variable and to put the lem executable in $PATH. LEMLIB should be the library directory within the checked-out lem directory (i.e. ```path-to-lem/library/```). Next, install linksem as
```
git clone git@github.com:rems-project/linksem.git
cd linksem
make && make install
```
Sail
----
Sail depends on lem and ott, so make sure lem and ott executables
exist in $PATH.
```
git clone git@github.com:rems-project/sail.git
cd sail
make
```
To build Sail with interactive support we need two more commands
```
opam install linenoise
make isail
```
To test if Sail behaves correctly, execute the following from the
root directory of the sail repository. You may also need to set
$LEM_DIR to the root of the lem repository for the lem tests. Some of
the C backend tests will fail if valgrind isn't installed. Some tests will
fail if cvc4 isn’t installed.
```
export SAIL_DIR=$PWD
test/run_tests.sh
```
To install Sail using OPAM from the git repo, use `opam pin` as follows.
```
opam pin add sail /path/to/local/sail/repo
```
This way, you can make the most recent changes to Sail easily available to programs
that use it. To rebuild this installation of Sail, use `opam upgrade` as usual.
If you want to do more complicated things, `opam pin --help` might be of
interest.
|
