Skip to content
Merged
Changes from 1 commit
Commits
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
72 changes: 71 additions & 1 deletion COMPILING.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# What architecture?
# WHAT ARCHITECTURE?

CPROVER now needs a C++11 compliant compiler and works in the following
environments:
Expand Down Expand Up @@ -236,3 +236,73 @@ This will:
2) Run all the regression tests
3) Collate the coverage metrics
4) Provide an HTML report of the current coverage

# USING CLANG-FORMAT

CBMC uses clang-format to ensure that the formatting of new patches is readable
and consistent. There are two main ways of running clang-format: remotely, and
locally.

## RUNNING CLANG-FORMAT REMOTELY

When patches are submitted to CBMC, they are automatically run through
continuous integration (CI). One of the CI checks will run clang-format over
the diff that your pull request introduces. If clang-format finds formatting
issues at this point, the build will be failed, and a patch will be produced
in the CI output that you can apply to your code so that it conforms to the
style guidelines.

To apply the patch, copy and paste it into a local file (`patch.txt`) and then
run:
```
patch -p1 -i patch.txt
```
Now, you can commit and push the formatting fixes.

## RUNNING CLANG-FORMAT LOCALLY

### INSTALLATION

To avoid waiting until you've made a PR to find formatting issues, you can
install clang-format locally and run it against your code as you are working.

Different versions of clang-format have slightly different behaviors. CBMC uses
clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
Copy link
Collaborator

Choose a reason for hiding this comment

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

Do we need version 3.8 or could it be "any newer version"?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Subsequent versions have slightly different behaviour, so we need to standardise on a particular version.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Is it just me that I find this lock-in scary?

Maybe I'm misunderstanding your comment: From my point of view this means that the premises 1) "Absolutely consistent (don't have to rely on reviewers catching all errors)" only holds when sticking with this one version forever and 2) "No need for vague style guidelines written in English" is actually untrue, because we'd still need some ground truth when forced to move to a newer version (clang-format 3.8 may become unavailable in pre-compiled form at some point).

Would you be able to provide more detail on "slightly different behaviour?"

Copy link
Contributor Author

Choose a reason for hiding this comment

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

As far as I can tell, newer versions add more formatting parameters, which may affect how clang-format chooses where to place line-breaks, but the config files are backward-compatible. That is, a newer version will produce a style that still obeys all the rules from the config file, but which may find better line-break positions (for some value of 'better').

I don't think that being locked to a specific version is too worrying, as we're already incrementally updating the style. If we want to update to a new version in the future, we can carry on incrementally updating, but using a newer clang-format binary.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I do feel better given the information you have just given me, but this isn't the message that the documentation is sending out right now. So why are you proposing specifically version 3.8 then? Is it because that's the version that is available in current distributions? If so, I'd suggest that package-manager install instructions refer to such a version (much like is done for GCC), but I would refrain from doing so in plain text.

What I want to avoid is a cliff edge when moving to a newer version. I'd rather move with whichever version is available in the distribution used by Travis. Your comments assure me that our incremental application of clang-format should not cause any breakage.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, version 3.8 is available in packages for most platforms, so it seemed like a good choice. However, Ubuntu and Homebrew both supply newer versions of clang-format too, and typing apt install clang-format will default to the newer version. For this reason, I think it's important to provide install instructions specifically for version 3.8.

Copy link
Collaborator

Choose a reason for hiding this comment

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

:-\ I find it a little concerning that they aren't offering settings that are backwards compatible.

Homebrew.
To install, run:
```
sudo apt install clang-format-3.8 # Run this on Ubuntu, Debian etc.
Copy link
Collaborator

Choose a reason for hiding this comment

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

apt-get install (missing "-get", remove "sudo" as that's not done elsewhere in this file)

brew install clang-format-3.8 # Run this on a Mac with Homebrew installed
Copy link
Collaborator

Choose a reason for hiding this comment

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

In my brew set up I've got "clang-format" (seems to be version 4.0) or "[email protected]". Is my set up wrong or is the above guideline wrong?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I got the guideline wrong, fixed now

```
Copy link
Collaborator

Choose a reason for hiding this comment

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

We give build instructions for more platforms than just Ubuntu and Mac OS. Any chance of commands / pointers for those?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I've updated with instructions for more platforms


### FORMATTING A RANGE OF COMMITS

Clang-format is distributed with a driver script called git-clang-format-3.8.
This script can be used to format git diffs (rather than entire files).

After committing some code, it is recommended to run:
```
git-clang-format-3.8 upstream/develop
```
*Important:* If your branch is based on a branch other than `upstream/develop`,
use the name or checksum of that branch instead. It is strongly recommended to
rebase your work onto the tip of the branch it's based on before running
`git-clang-format` in this way.

### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS

If your works spans several commits and you'd like to keep the formatting
correct in each individual commit, you can automatically rewrite the commits
with correct formatting.

The following command will stop at each commit in the range and run
clang-format on the diff at that point. This rewrites git history, so it's
*unsafe*, and you should back up your branch before running this command:
```
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
-- upstream/develop..HEAD
```
*Important*: `upstream/develop` should be changed in *both* places in the
command above if your work is based on a different branch. It is strongly
recommended to rebase your work onto the tip of the branch it's based on before
running `git-clang-format` in this way.