Restructure compilation documentation #6109

thomasspriggs · 2021-05-12T09:49:47Z

This PR restructures the compilation documentation. We have received some feedback that the compilation instructions are difficult to follow for new users. This PR makes things more straight forward for new users to follow.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Becuase some platforms are not tested in CI, a new user would be well adviced to try a platform which is tested if they have choice.

The complete repository can be built using fewer build step using CMake than using the hand-written makefiles. Therefore people who are new to building CBMC should be able to get started more quickly using the CMake build than the make build. Therefore it makes sense for them to read about that build system first.

In order to match the version of visual studio and tool chain currently tested in CI.

Because "shoud" is not the correct spelling.

Because this was previously missing and it might not have been obvious for anyone unfamiliar with the build system.

Because this helps document the way CBMC is currently built in CI. This is usefull both for reference compared to local builds and for working out why CI builds are failing on PRs.

To match the ordering in the outline at the top.

To distance this section from the comparitively well-maintained Visual Studio 2019 with cmake build.

NlightNFotis

LGTM, with some minor comments.

COMPILING.md

NlightNFotis · 2021-05-12T10:32:48Z

COMPILING.md

+     [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


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?

COMPILING.md

codecov · 2021-05-12T11:32:19Z

Codecov Report

Merging #6109 (c112db2) into develop (4c14789) will increase coverage by 0.75%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6109      +/-   ##
===========================================
+ Coverage    74.52%   75.27%   +0.75%     
===========================================
  Files         1447     1447              
  Lines       157808   157988     +180     
===========================================
+ Hits        117610   118930    +1320     
+ Misses       40198    39058    -1140

Impacted Files	Coverage Δ
src/util/type.cpp	`44.44% <0.00%> (-33.34%)`	⬇️
src/ansi-c/c_typecheck_base.cpp	`50.68% <0.00%> (-27.55%)`	⬇️
src/goto-programs/remove_returns.cpp	`74.84% <0.00%> (-24.53%)`	⬇️
src/util/parse_options.cpp	`59.61% <0.00%> (-21.16%)`	⬇️
src/ansi-c/literals/convert_character_literal.cpp	`53.84% <0.00%> (-17.95%)`	⬇️
src/goto-programs/goto_program.cpp	`53.04% <0.00%> (-13.57%)`	⬇️
src/ansi-c/anonymous_member.cpp	`84.61% <0.00%> (-10.26%)`	⬇️
src/util/xml.cpp	`62.83% <0.00%> (-10.14%)`	⬇️
src/util/simplify_expr_floatbv.cpp	`86.82% <0.00%> (-9.31%)`	⬇️
src/ansi-c/ansi_c_convert_type.cpp	`70.17% <0.00%> (-8.56%)`	⬇️
... and 71 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 25a7b36...c112db2. Read the comment docs.

tautschnig

Thank you for improving the documentation!

COMPILING.md

tautschnig · 2021-05-13T06:51:17Z

COMPILING.md

+Building with CMake is supported across Linux, MacOS X and Windows with Visual
+Studio 2019. 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


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

tautschnig · 2021-05-13T06:53:56Z

COMPILING.md

+Studio 2019. 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
+repository in fewer steps and supports better integration with various IDEs and


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

tautschnig · 2021-05-13T06:57:41Z

COMPILING.md

+   - 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.


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.

COMPILING.md

TGWDB · 2021-05-13T08:42:25Z

COMPILING.md

+     You shoud also install [Homebrew](https://brew.sh), after which you can
+     run `brew install cmake` to install CMake.


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.)

TGWDB · 2021-05-13T08:44:38Z

COMPILING.md

+# 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.


"machine" -> "platform"

TGWDB · 2021-05-13T08:48:58Z

COMPILING.md


 - Linux
 - MacOS X
+- Microsoft Visual Studio


This should be >=2019, also below should probably indicate MSVS 2015+-?

COMPILING.md

In order to indicate that this is the name of the package.

Because "CMake" should be capitalised that way; not "cmake" or "CMAKE".

To distinguish it from the name of the build system as the command should not be capitalised.

To help users who decide to install Strawberry Perl to do so.

In order to more clearly explain the issue.

Because cygwin is not tested in CI and because this means that we can list operating systems rather than a mix of operating systems and tool chains.

Implement some suggestions presented as comments in diffblue#6109 (we had to merge the PR before we could get a chance to incorporate them, so we are compensating now) and do some other minor cleanup of the COMPILING.md file.

thomasspriggs added 8 commits May 12, 2021 10:44

Update compiling document to indicate current platform status

e26ece4

Becuase some platforms are not tested in CI, a new user would be well adviced to try a platform which is tested if they have choice.

Update compiling documentation to refer to Visual Studio 2019

62a5248

In order to match the version of visual studio and tool chain currently tested in CI.

Fix misspelling of "should" in compiling documentation

df55570

Because "shoud" is not the correct spelling.

Document location of built binaries for the cmake build

8e78992

Because this was previously missing and it might not have been obvious for anyone unfamiliar with the build system.

Link to CI script in compiling documentation

ed7c6b7

Because this helps document the way CBMC is currently built in CI. This is usefull both for reference compared to local builds and for working out why CI builds are failing on PRs.

Move SOLARIS and FREEBSD sections downwards

a295f90

To match the ordering in the outline at the top.

Retitle Windows section to indicate cygwin usage

a4bfb6d

To distance this section from the comparitively well-maintained Visual Studio 2019 with cmake build.

thomasspriggs requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners May 12, 2021 09:49

NlightNFotis approved these changes May 12, 2021

View reviewed changes

NlightNFotis mentioned this pull request May 12, 2021

Visual Studio compilation documentation #6111

Merged

7 tasks

tautschnig approved these changes May 13, 2021

View reviewed changes

tautschnig assigned thomasspriggs May 13, 2021

TGWDB reviewed May 13, 2021

View reviewed changes

thomasspriggs added 6 commits May 13, 2021 10:34

Quote strawberryperl in compiling documentation

1eca47c

In order to indicate that this is the name of the package.

Consistently capitalise CMake when naming the build system

d79edf5

Because "CMake" should be capitalised that way; not "cmake" or "CMAKE".

Quote cmake when referring to the command

070dfec

To distinguish it from the name of the build system as the command should not be capitalised.

Document where to get Strawberry Perl in COMPILING.md

1aa9b60

To help users who decide to install Strawberry Perl to do so.

Rephrase explaination of non-universal macOS binaries

d34fc86

In order to more clearly explain the issue.

Remove references to cygwin in favour of Windows instead

c112db2

Because cygwin is not tested in CI and because this means that we can list operating systems rather than a mix of operating systems and tool chains.

NlightNFotis merged commit 4aa3c0d into diffblue:develop May 13, 2021

thomasspriggs deleted the tas/compiling_docs_refactor branch May 13, 2021 13:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Restructure compilation documentation #6109

Restructure compilation documentation #6109

thomasspriggs commented May 12, 2021 •

edited

Loading

NlightNFotis left a comment

NlightNFotis May 12, 2021

codecov bot commented May 12, 2021 •

edited

Loading

tautschnig left a comment

tautschnig May 13, 2021

tautschnig May 13, 2021

tautschnig May 13, 2021

TGWDB May 13, 2021

TGWDB May 13, 2021

TGWDB May 13, 2021

		You shoud also install [Homebrew](https://brew.sh), after which you can
		run `brew install cmake` to install CMake.

Restructure compilation documentation #6109

Restructure compilation documentation #6109

Conversation

thomasspriggs commented May 12, 2021 • edited Loading

NlightNFotis left a comment

Choose a reason for hiding this comment

NlightNFotis May 12, 2021

Choose a reason for hiding this comment

codecov bot commented May 12, 2021 • edited Loading

Codecov Report

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig May 13, 2021

Choose a reason for hiding this comment

tautschnig May 13, 2021

Choose a reason for hiding this comment

tautschnig May 13, 2021

Choose a reason for hiding this comment

TGWDB May 13, 2021

Choose a reason for hiding this comment

TGWDB May 13, 2021

Choose a reason for hiding this comment

TGWDB May 13, 2021

Choose a reason for hiding this comment

thomasspriggs commented May 12, 2021 •

edited

Loading

codecov bot commented May 12, 2021 •

edited

Loading