Skip to content

Commit 4aa3c0d

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6109 from thomasspriggs/tas/compiling_docs_refactor
Restructure compilation documentation
2 parents d61a8f4 + c112db2 commit 4aa3c0d

File tree

1 file changed

+148
-189
lines changed

1 file changed

+148
-189
lines changed

‎COMPILING.md‎

Lines changed: 148 additions & 189 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,129 @@
11
# WHAT ARCHITECTURE?
22

3-
CPROVER now needs a C++11 compliant compiler and works in the following
4-
environments:
3+
CPROVER now needs a C++11 compliant compiler and is known to work in the
4+
following environments:
55

66
- Linux
77
- MacOS X
8+
- Windows
9+
10+
The above environments are currently tested as part of our continuous
11+
integration system. It separately tests both the CMake build system and the
12+
hand-written make files. The latest build steps being used in CI can be
13+
[referenced here](https://github.com/diffblue/cbmc/blob/develop/.github/workflows/pull-request-checks.yaml).
14+
15+
The environments below have been used successfully in the
16+
past, but are not actively tested:
17+
818
- Solaris 11
919
- FreeBSD 11
10-
- Cygwin
11-
- Microsoft Visual Studio
1220

13-
The rest of this document is split up into three parts: compilation on Linux,
14-
MacOS, Windows. Please read the section appropriate for your machine.
21+
# Building using CMake
22+
23+
Building with CMake is supported across Linux, MacOS X and Windows with Visual
24+
Studio 2019. There are also hand-written make files which can be used to build
25+
separate binaries independently. Usage of the hand-written make files is
26+
explained in a separate section. The CMake build can build the complete
27+
repository in fewer steps and supports better integration with various IDEs and
28+
static-analysis tools. On Windows, the CMake build has the advantage of not
29+
depending on Cygwin or MinGW, and doesn't require manual modification of build
30+
files.
31+
32+
1. Ensure you have all the build dependencies installed. Build dependencies are
33+
the same as for the makefile build, but with the addition of CMake version
34+
3.2 or higher. The installed CMake version can be queried with `cmake
35+
--version`. To install CMake:
36+
- On Debian-like distributions, do
37+
```
38+
apt-get install g++ gcc flex bison make git curl patch cmake
39+
```
40+
- On Red Hat/Fedora or derivates, do
41+
```
42+
dnf install gcc gcc-c++ flex bison curl patch cmake
43+
```
44+
- On macOS, do
45+
```
46+
xcode-select --install
47+
```
48+
You should also install [Homebrew](https://brew.sh), after which you can
49+
run `brew install cmake` to install CMake.
50+
- On platforms where installing the Java Development Kit and Maven is
51+
difficult, you can avoid needing these dependencies by not building
52+
JBMC. Just pass `-DWITH_JBMC=OFF` to `cmake` in step (4) below.
53+
- On Windows, ensure you have Visual Studio 2019 or later installed. The
54+
developer command line that comes with Visual Studio 2019 has CMake
55+
already available. You will also need to ensure that you have winflexbison
56+
installed and available in the path. winflexbison is available from
57+
[the github release page](https://github.com/lexxmark/winflexbison/releases/)
58+
or through
59+
[the chocolatey package manager.](https://community.chocolatey.org/packages/winflexbison3)
60+
Installing `strawberryperl` is advised if you want to run tests on Windows.
61+
This is available from
62+
[the Strawberry Perl website](https://strawberryperl.com/) or through the
63+
[the chocolatey package manager.](https://community.chocolatey.org/packages/StrawberryPerl)
64+
- Use of CMake has not been tested on Solaris or FreeBSD. However, it should
65+
be possible to install CMake from the system package manager or the
66+
[official download page](https://cmake.org/download) on those systems.
67+
The dependencies (as listed in the relevant sections above) will also be
68+
required, and should be installed using the suggested methods.
69+
2. Navigate to the *top level* folder of the project. This is different from
70+
the Makefile build, which requires you to navigate to the `src` directory
71+
first.
72+
3. Update git submodules:
73+
```
74+
git submodule update --init
75+
```
76+
4. Generate build files with CMake:
77+
```
78+
cmake -S . -Bbuild
79+
```
80+
This command tells CMake to use the configuration in the current directory,
81+
and to generate build files into the `build` directory. This is the point
82+
to specify custom build settings, such as compilers and build back-ends. You
83+
can use clang (for example) by adding the argument
84+
`-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake
85+
to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a
86+
comprehensive list of supported back-ends.
87+
88+
On macOS >10.14, the build will fail unless you explicitly specify
89+
the full path to the compiler. This issue is being tracked
90+
[here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
91+
looks like this:
92+
```
93+
cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
94+
```
95+
96+
Generally it is not necessary to manually specify individual compiler or
97+
linker flags, as CMake defines a number of "build modes" including Debug and
98+
Release modes. To build in a particular mode, add the flag
99+
`-DCMAKE_BUILD_TYPE=Debug` (or `RelWithDebInfo`) to the initial invocation.
100+
The default is to perform an optimized build via the `Release` configuration.
101+
102+
If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
103+
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
104+
sanitizers.
15105
16-
# COMPILATION ON LINUX
106+
Finally, to enable building universal binaries on macOS, you can pass the
107+
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
108+
the built binaries will only work on the architecture of the machine being
109+
used to do the build.
110+
111+
5. Run the build:
112+
```
113+
cmake --build build
114+
```
115+
This command tells CMake to invoke the correct tool to run the build in the
116+
`build` directory. You can also use the build back-end directly by invoking
117+
`make`, `ninja`, or opening the generated IDE project as appropriate. The
118+
complete set of built binaries can be found in `./build/bin` once the build
119+
is complete.
120+
121+
# Building using hand-written make files.
122+
123+
The rest of this section is split up based on the platform being built on.
124+
Please read the section appropriate for your machine.
125+
126+
## COMPILATION ON LINUX
17127
18128
We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
19129
@@ -65,7 +175,34 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
65175
make -C jbmc/src
66176
```
67177
68-
# COMPILATION ON SOLARIS 11
178+
## COMPILATION ON MACOS X
179+
180+
Follow these instructions:
181+
182+
1. You need a C/C++ compiler, Flex and Bison, and GNU make. To this end, first
183+
install the XCode from the App-store and then type
184+
```
185+
xcode-select --install
186+
```
187+
in a terminal window.
188+
2. Then get the CBMC source via
189+
```
190+
git clone https://github.com/diffblue/cbmc cbmc-git
191+
cd cbmc-git
192+
```
193+
3. To compile CBMC, do
194+
```
195+
make -C src minisat2-download
196+
make -C src
197+
```
198+
4. To compile JBMC, you additionally need Maven 3, which has to be installed
199+
manually. Then do
200+
```
201+
make -C jbmc/src setup-submodules
202+
make -C jbmc/src
203+
```
204+
205+
## COMPILATION ON SOLARIS 11
69206
70207
We assume Solaris 11.4 or newer. To build JBMC, you'll need to install
71208
Maven 3 manually.
@@ -90,7 +227,7 @@ Maven 3 manually.
90227
gmake -C jbmc/src
91228
```
92229
93-
# COMPILATION ON FREEBSD 11
230+
## COMPILATION ON FREEBSD 11
94231
95232
1. As root, get the necessary tools:
96233
```
@@ -116,184 +253,6 @@ Maven 3 manually.
116253
gmake -C jbmc/src
117254
```
118255
119-
# COMPILATION ON MACOS X
120-
121-
Follow these instructions:
122-
123-
1. You need a C/C++ compiler, Flex and Bison, and GNU make. To this end, first
124-
install the XCode from the App-store and then type
125-
```
126-
xcode-select --install
127-
```
128-
in a terminal window.
129-
2. Then get the CBMC source via
130-
```
131-
git clone https://github.com/diffblue/cbmc cbmc-git
132-
cd cbmc-git
133-
```
134-
3. To compile CBMC, do
135-
```
136-
make -C src minisat2-download
137-
make -C src
138-
```
139-
4. To compile JBMC, you additionally need Maven 3, which has to be installed
140-
manually. Then do
141-
```
142-
make -C jbmc/src setup-submodules
143-
make -C jbmc/src
144-
```
145-
146-
# COMPILATION ON WINDOWS
147-
148-
There are two options: the Visual Studio compiler with version 14 (2015) or
149-
later, or the MinGW cross compiler with version 5.4 or later.
150-
We recommend Visual Studio.
151-
152-
Follow these instructions:
153-
154-
1. First install Cygwin, then from the Cygwin setup facility install the
155-
following packages: `flex, bison, tar, gzip, git, make, wget, patch,
156-
curl`.
157-
2. Get the CBMC source via
158-
```
159-
git clone https://github.com/diffblue/cbmc cbmc-git
160-
cd cbmc-git
161-
```
162-
3. Depending on your choice of compiler:
163-
1. To compile with Visual Studio, change the second line of `src/config.inc`
164-
to
165-
```
166-
BUILD_ENV = MSVC
167-
```
168-
Open the Developer Command Prompt for Visual Studio, then start the
169-
Cygwin shell with
170-
```
171-
bash.exe -login
172-
```
173-
Please note that this might open a different shell instead, especially if
174-
you have installed other Linux subsystems previously. To verify that you
175-
are in the correct shell, make sure that the Windows file system can be
176-
accessed via the folder`/cygdrive`. If the command above does not open
177-
the Cygwin shell, you can also access it by using its absolute path,
178-
`C:\cygwin64\bin\bash.exe` by default. In the Developer Command Prompt,
179-
simply type
180-
```
181-
C:\cygwin64\bin\bash.exe -login
182-
```
183-
2. To compile with MinGW, use Cygwin setup to install a mingw g++ compiler
184-
package, i.e. one of `mingw{32,64}-{x86_64,i686}-gcc-g++`. You may also
185-
have to adjust the section in `src/common` that defines `CC` and `CXX`
186-
for BUILD_ENV = Cygwin.
187-
Then start the Cygwin shell.
188-
4. To compile CMBC, open the Cygwin shell and type
189-
```
190-
make -C src DOWNLOADER=wget minisat2-download
191-
make -C src
192-
```
193-
5. To compile JBMC, you additionally need the JDK and Maven 3, which have
194-
to be installed manually. Then open the Cygwin shell and type
195-
```
196-
make -C jbmc/src setup-submodules
197-
make -C jbmc/src
198-
```
199-
200-
(Optional) A Visual Studio project file can be generated with the script
201-
"generate_vcxproj" that is in the subdirectory "scripts". The project file is
202-
helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can
203-
be used for building with MSBuild. Note that you still need to run flex/bison
204-
using "make generated_files" before opening the project.
205-
206-
# WORKING WITH CMAKE
207-
208-
There is also a build based on CMake instead of hand-written
209-
makefiles. It should work on a wider variety of systems than the standard
210-
makefile build, and can integrate better with IDEs and static-analysis tools.
211-
On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't
212-
require manual modification of build files.
213-
214-
1. Ensure you have all the build dependencies installed. Build dependencies are
215-
the same as for the makefile build, but with the addition of CMake version
216-
3.2 or higher. The installed CMake version can be queried with `cmake
217-
--version`. To install cmake:
218-
- On Debian-like distributions, do
219-
```
220-
apt-get install cmake
221-
```
222-
- On Red Hat/Fedora or derivates, do
223-
```
224-
dnf install cmake
225-
```
226-
- On macOS, do
227-
```
228-
xcode-select --install
229-
```
230-
You shoud also install [Homebrew](https://brew.sh), after which you can
231-
run `brew install cmake` to install CMake.
232-
- On platforms where installing the Java Development Kit and Maven is
233-
difficult, you can avoid needing these dependencies by not building
234-
JBMC. Just pass `-DWITH_JBMC=OFF` to cmake in step (4) below.
235-
- On Windows, ensure you have Visual Studio 2015 or later installed.
236-
Then, download CMake from the [official download
237-
page](https://cmake.org/download).
238-
You'll also need `git` and `patch`, which are both provided by the
239-
[git for Windows](git-scm.com/download/win) package.
240-
Finally, Windows builds of flex and bison should be installed from
241-
[the sourceforge page](sourceforge.net/projects/winflexbison).
242-
The easiest way to 'install' these executables is to unzip them and to
243-
drop the entire unzipped package into the CBMC source directory.
244-
- Use of CMake has not been tested on Solaris or FreeBSD. However, it should
245-
be possible to install CMake from the system package manager or the
246-
[official download page](https://cmake.org/download) on those systems.
247-
The dependencies (as listed in the relevant sections above) will also be
248-
required, and should be installed using the suggested methods.
249-
2. Navigate to the *top level* folder of the project. This is different from
250-
the Makefile build, which requires you to navigate to the `src` directory
251-
first.
252-
3. Update git submodules:
253-
```
254-
git submodule update --init
255-
```
256-
4. Generate build files with CMake:
257-
```
258-
cmake -S . -Bbuild
259-
```
260-
This command tells CMake to use the configuration in the current directory,
261-
and to generate build files into the `build` directory. This is the point
262-
to specify custom build settings, such as compilers and build back-ends. You
263-
can use clang (for example) by adding the argument
264-
`-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake
265-
to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a
266-
comprehensive list of supported back-ends.
267-
268-
On macOS >10.14, the build will fail unless you explicitly specify
269-
the full path to the compiler. This issue is being tracked
270-
[here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
271-
looks like this:
272-
```
273-
cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
274-
```
275-
276-
Generally it is not necessary to manually specify individual compiler or
277-
linker flags, as CMake defines a number of "build modes" including Debug and
278-
Release modes. To build in a particular mode, add the flag
279-
`-DCMAKE_BUILD_TYPE=Debug` (or `RelWithDebInfo`) to the initial invocation.
280-
The default is to perform an optimized build via the `Release` configuration.
281-
282-
If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
283-
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
284-
sanitizers.
285-
286-
Finally, to enable building universal binaries on macOS, you can pass the
287-
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
288-
the build will just be for the architecture of your machine.
289-
5. Run the build:
290-
```
291-
cmake --build build
292-
```
293-
This command tells CMake to invoke the correct tool to run the build in the
294-
`build` directory. You can also use the build back-end directly by invoking
295-
`make`, `ninja`, or opening the generated IDE project as appropriate.
296-
297256
# WORKING WITH ECLIPSE
298257
299258
To work with Eclipse, do the following:
@@ -343,7 +302,7 @@ If compiling with make:
343302
2. Uncomment the definition of `CUDD` in the file `src/config.inc`.
344303
3. Compile with `make -C src`
345304
346-
If compiling with cmake:
305+
If compiling with CMake:
347306
348307
1. Add the `-DCMAKE_USE_CUDD=true` flag to the `cmake` configuration phase.
349308
For instance:
@@ -397,7 +356,7 @@ make -C src glucose-download
397356
make -C src GLUCOSE=../../glucose-syrup
398357
```
399358
400-
For `cmake` the alternatives can be built with the following arguments to `cmake`
359+
For CMake the alternatives can be built with the following arguments to `cmake`
401360
for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`.
402361
403362

0 commit comments

Comments
 (0)