Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Restructure compilation documentation #6109

Merged
merged 14 commits into from
May 13, 2021
Merged

Restructure compilation documentation #6109

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
e26ece4
Update compiling document to indicate current platform status
thomasspriggs May 12, 2021
892e59b
Move CMake build instructions above make build instructions
thomasspriggs May 12, 2021
62a5248
Update compiling documentation to refer to Visual Studio 2019
thomasspriggs May 12, 2021
df55570
Fix misspelling of "should" in compiling documentation
thomasspriggs May 12, 2021
8e78992
Document location of built binaries for the cmake build
thomasspriggs May 12, 2021
ed7c6b7
Link to CI script in compiling documentation
thomasspriggs May 12, 2021
a295f90
Move SOLARIS and FREEBSD sections downwards
thomasspriggs May 12, 2021
a4bfb6d
Retitle Windows section to indicate cygwin usage
thomasspriggs May 12, 2021
1eca47c
Quote `strawberryperl` in compiling documentation
thomasspriggs May 13, 2021
d79edf5
Consistently capitalise CMake when naming the build system
thomasspriggs May 13, 2021
070dfec
Quote `cmake` when referring to the command
thomasspriggs May 13, 2021
1aa9b60
Document where to get Strawberry Perl in `COMPILING.md`
thomasspriggs May 13, 2021
d34fc86
Rephrase explaination of non-universal macOS binaries
thomasspriggs May 13, 2021
c112db2
Remove references to cygwin in favour of Windows instead
thomasspriggs May 13, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
201 changes: 103 additions & 98 deletions COMPILING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,106 @@ past, but are not actively tested:
- FreeBSD 11
- Cygwin

The rest of this document is split up into three parts: compilation on Linux,
MacOS, Windows. Please read the section appropriate for your machine.
# Building using CMAKE
NlightNFotis marked this conversation as resolved.
Show resolved Hide resolved

# COMPILATION ON LINUX
Building with CMake is supported across Linux, MacOS X and Windows with Visual
Studio. There are also hand-written make files which can be used to build
separate binaries independently. Usage of the hand-written make files is
explained in a separate section. The CMake build can build the complete
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could that "separate section" be named/referenced here?

repository in fewer steps and supports better integration with various IDEs and
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How did you find out that it was "fewer steps?"

static-analysis tools. On Windows, the CMake build has the advantage of not
depending on Cygwin or MinGW, and doesn't require manual modification of build
files.

1. Ensure you have all the build dependencies installed. Build dependencies are
the same as for the makefile build, but with the addition of CMake version
3.2 or higher. The installed CMake version can be queried with `cmake
--version`. To install cmake:
- On Debian-like distributions, do
```
apt-get install g++ gcc flex bison make git curl patch cmake
```
- On Red Hat/Fedora or derivates, do
```
dnf install gcc gcc-c++ flex bison curl patch cmake
```
- On macOS, do
```
xcode-select --install
```
You shoud also install [Homebrew](https://brew.sh), after which you can
run `brew install cmake` to install CMake.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also similar to tautshnig's comment below, why is MacOS different in style and arguments to the others. I think it would be better to have single (displayed) comment for each system and let that do it all. If users want to play around, this can (probably) be covered elsewhere. (Note, I'm reviewing by commit, so they may be a little haphazard depending on the commits.)

- On platforms where installing the Java Development Kit and Maven is
difficult, you can avoid needing these dependencies by not building
JBMC. Just pass `-DWITH_JBMC=OFF` to cmake in step (4) below.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The above commands didn't install maven or a JDK! Also, having this item right here is a bit strange for both the ones before and after are about installing operating-system specific dependencies.

- On Windows, ensure you have Visual Studio 2015 or later installed.
Then, download CMake from the [official download
page](https://cmake.org/download).
You'll also need `git` and `patch`, which are both provided by the
[git for Windows](git-scm.com/download/win) package.
Finally, Windows builds of flex and bison should be installed from
[the sourceforge page](sourceforge.net/projects/winflexbison).
The easiest way to 'install' these executables is to unzip them and to
drop the entire unzipped package into the CBMC source directory.
- Use of CMake has not been tested on Solaris or FreeBSD. However, it should
be possible to install CMake from the system package manager or the
[official download page](https://cmake.org/download) on those systems.
The dependencies (as listed in the relevant sections above) will also be
required, and should be installed using the suggested methods.
2. Navigate to the *top level* folder of the project. This is different from
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe add the second sentence as a bullet point, or add the paths in parentheses (cbmc vs cbmc/src/) to make it a bit less confusing?

the Makefile build, which requires you to navigate to the `src` directory
first.
3. Update git submodules:
```
git submodule update --init
```
4. Generate build files with CMake:
```
cmake -S . -Bbuild
```
This command tells CMake to use the configuration in the current directory,
and to generate build files into the `build` directory. This is the point
to specify custom build settings, such as compilers and build back-ends. You
can use clang (for example) by adding the argument
`-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake
to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a
comprehensive list of supported back-ends.

On macOS >10.14, the build will fail unless you explicitly specify
the full path to the compiler. This issue is being tracked
[here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
looks like this:
```
cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
```

Generally it is not necessary to manually specify individual compiler or
linker flags, as CMake defines a number of "build modes" including Debug and
Release modes. To build in a particular mode, add the flag
`-DCMAKE_BUILD_TYPE=Debug` (or `RelWithDebInfo`) to the initial invocation.
The default is to perform an optimized build via the `Release` configuration.

If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
sanitizers.

Finally, to enable building universal binaries on macOS, you can pass the
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
the build will just be for the architecture of your machine.
NlightNFotis marked this conversation as resolved.
Show resolved Hide resolved
5. Run the build:
```
cmake --build build
```
This command tells CMake to invoke the correct tool to run the build in the
`build` directory. You can also use the build back-end directly by invoking
`make`, `ninja`, or opening the generated IDE project as appropriate.

# Building using hand-written make files.

The rest of this section is split up based on the platform being built on.
Please read the section appropriate for your machine.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"machine" -> "platform"


## COMPILATION ON LINUX

We assume that you have a Debian/Ubuntu or Red Hat-like distribution.

Expand Down Expand Up @@ -70,7 +166,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
make -C jbmc/src
```

# COMPILATION ON SOLARIS 11
## COMPILATION ON SOLARIS 11

We assume Solaris 11.4 or newer. To build JBMC, you'll need to install
Maven 3 manually.
Expand All @@ -95,7 +191,7 @@ Maven 3 manually.
gmake -C jbmc/src
```

# COMPILATION ON FREEBSD 11
## COMPILATION ON FREEBSD 11

1. As root, get the necessary tools:
```
Expand All @@ -121,7 +217,7 @@ Maven 3 manually.
gmake -C jbmc/src
```

# COMPILATION ON MACOS X
## COMPILATION ON MACOS X

Follow these instructions:

Expand All @@ -148,7 +244,7 @@ Follow these instructions:
make -C jbmc/src
```

# COMPILATION ON WINDOWS
## COMPILATION ON WINDOWS

There are two options: the Visual Studio compiler with version 14 (2015) or
later, or the MinGW cross compiler with version 5.4 or later.
Expand Down Expand Up @@ -208,97 +304,6 @@ helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can
be used for building with MSBuild. Note that you still need to run flex/bison
using "make generated_files" before opening the project.

# WORKING WITH CMAKE

There is also a build based on CMake instead of hand-written
makefiles. It should work on a wider variety of systems than the standard
makefile build, and can integrate better with IDEs and static-analysis tools.
On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't
require manual modification of build files.

1. Ensure you have all the build dependencies installed. Build dependencies are
the same as for the makefile build, but with the addition of CMake version
3.2 or higher. The installed CMake version can be queried with `cmake
--version`. To install cmake:
- On Debian-like distributions, do
```
apt-get install cmake
```
- On Red Hat/Fedora or derivates, do
```
dnf install cmake
```
- On macOS, do
```
xcode-select --install
```
You shoud also install [Homebrew](https://brew.sh), after which you can
run `brew install cmake` to install CMake.
- On platforms where installing the Java Development Kit and Maven is
difficult, you can avoid needing these dependencies by not building
JBMC. Just pass `-DWITH_JBMC=OFF` to cmake in step (4) below.
- On Windows, ensure you have Visual Studio 2015 or later installed.
Then, download CMake from the [official download
page](https://cmake.org/download).
You'll also need `git` and `patch`, which are both provided by the
[git for Windows](git-scm.com/download/win) package.
Finally, Windows builds of flex and bison should be installed from
[the sourceforge page](sourceforge.net/projects/winflexbison).
The easiest way to 'install' these executables is to unzip them and to
drop the entire unzipped package into the CBMC source directory.
- Use of CMake has not been tested on Solaris or FreeBSD. However, it should
be possible to install CMake from the system package manager or the
[official download page](https://cmake.org/download) on those systems.
The dependencies (as listed in the relevant sections above) will also be
required, and should be installed using the suggested methods.
2. Navigate to the *top level* folder of the project. This is different from
the Makefile build, which requires you to navigate to the `src` directory
first.
3. Update git submodules:
```
git submodule update --init
```
4. Generate build files with CMake:
```
cmake -S . -Bbuild
```
This command tells CMake to use the configuration in the current directory,
and to generate build files into the `build` directory. This is the point
to specify custom build settings, such as compilers and build back-ends. You
can use clang (for example) by adding the argument
`-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake
to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a
comprehensive list of supported back-ends.

On macOS >10.14, the build will fail unless you explicitly specify
the full path to the compiler. This issue is being tracked
[here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
looks like this:
```
cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
```

Generally it is not necessary to manually specify individual compiler or
linker flags, as CMake defines a number of "build modes" including Debug and
Release modes. To build in a particular mode, add the flag
`-DCMAKE_BUILD_TYPE=Debug` (or `RelWithDebInfo`) to the initial invocation.
The default is to perform an optimized build via the `Release` configuration.

If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
sanitizers.

Finally, to enable building universal binaries on macOS, you can pass the
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
the build will just be for the architecture of your machine.
5. Run the build:
```
cmake --build build
```
This command tells CMake to invoke the correct tool to run the build in the
`build` directory. You can also use the build back-end directly by invoking
`make`, `ninja`, or opening the generated IDE project as appropriate.

# WORKING WITH ECLIPSE

To work with Eclipse, do the following:
Expand Down