Update compilation and development docs #2789

owen-mc-diffblue · 2018-08-21T15:38:29Z

No description provided.

peterschrammel · 2018-08-21T17:52:19Z

doc/architectural/compilation-and-development.md

+Instructions for compiling CBMC using makefiles are
+available in
+[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#what-architecture)
+in the root of the CBMC repository. They cover linux, Solaris 11,


peterschrammel · 2018-08-21T17:52:35Z

doc/architectural/compilation-and-development.md


-### Regression tests ###
+There is experimental support for compiling using CMake. Instructions are


Still experimental??

I'm just copying what it says in COMPILING.md. I'll update both places.

peterschrammel · 2018-08-21T17:53:28Z

doc/architectural/compilation-and-development.md

+There is experimental support for compiling using CMake. Instructions are
+available in
+[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake-experimental)
+in the root of the CBMC repository.


One note here is that cmake currently always compiles CBMC and JBMC, whereas with Makefiles you can compile CBMC without JBMC.

Surely with CMake targets you can just compile CBMC?

I asked @smowton and he agreed that you can compile just CBMC using CMake targets, so unless I hear otherwise I won't add anything about this.

peterschrammel · 2018-08-21T17:55:39Z

doc/architectural/compilation-and-development.md

+`regression/` there is a directory for each of the tools/modules. Each of
+these contains multiple test directories, with names describing
+what they test. When there are multiple tests in a test directory then
+they should all be testing the same thing. Each test directory contains


What is "thing" here?

I have the same comment. Maybe be more specific about what a "thing" is.

I've updated it to "When there are multiple tests in a test directory then they should be testing very similar aspects of the program's behaviour."

peterschrammel · 2018-08-21T17:56:39Z

doc/architectural/compilation-and-development.md

+to run, what output is expected and so on. The test framework is an in-house
+Perl script,
+[test.pl](https://github.com/diffblue/cbmc/blob/develop/regression/test.pl).
+To run all the tests in a directory corresponding to a tool or module:

    ../test.pl -c PATH_TO_CBMC


Nobody does that by hand. You usually run it through make.

Be careful when using the term "nobody" :-) - legitimate uses include running selected tests. But arguably the text could recommend the use of make test.

Everyone I know runs test.pl directly, though as @tautschnig says it's normally for running a single test. I will add instructions for make test.

peterschrammel · 2018-08-21T17:57:57Z

doc/architectural/compilation-and-development.md

+
+If you have compiled CBMC using CMake then another way to run the same tests
+is through `CTest`. From the build directory, the command `ctest -V -L CORE`
+will run all of the tests that are run in CI. `-V` makes it print out more


Not sure that is a good definition: "all of the tests that are run in CI"

Alternative suggestion: Runs all tests labelled CORE in the desc files and unit tests. I think the current isn't correct as aren't THOROUGH tests also run on CI?

THOROUGH tests aren't run in CI

peterschrammel · 2018-08-21T17:58:38Z

doc/architectural/compilation-and-development.md

-The `–help` option gives instructions for use and the
-format of the description files.
+The `--help` option to `test.pl` gives instructions for use and outlines the
+format of the test description files.


The test categories CORE, KNOWNBUG, etc should be explained.

Also the labels for excluding specific tests need some explanation.

thk123 · 2018-08-22T09:59:26Z

doc/architectural/compilation-and-development.md

+
+If you have compiled CBMC using CMake then another way to run the same tests
+is through `CTest`. From the build directory, the command `ctest -V -L CORE`
+will run all of the tests that are run in CI. `-V` makes it print out more


Alternative suggestion: Runs all tests labelled CORE in the desc files and unit tests. I think the current isn't correct as aren't THOROUGH tests also run on CI?

thk123 · 2018-08-22T10:00:17Z

doc/architectural/compilation-and-development.md

+is through `CTest`. From the build directory, the command `ctest -V -L CORE`
+will run all of the tests that are run in CI. `-V` makes it print out more
+useful output and `-L CORE` makes it only run tests that have been tagged
+`CORE`. `-R regular_expression` can be used to limit which tests are run, and


Might be worth mentioning this can't be used to for example run a specific .desc file, only one of the top level folders.

Is there actually a way to run individual tests in CMake? Not knowing how to work with the tests is one of the reasons I've largely refrained from adopting CMake.

I believe that what we add to CTest is one command per module/tool folder, so CTest doesn't know how to run just one folder within one of those.

thk123 · 2018-08-22T10:01:12Z

doc/architectural/compilation-and-development.md

+base branch:
+
+    scripts/run_lint.sh <base-branch>


I'd give an example base-branch just because I don't think its meaning is necessarily well understood.

allredj

This document should keep evolving, but it's a good start. Only minor comments.

allredj · 2018-08-22T14:35:41Z

doc/architectural/compilation-and-development.md

@@ -3,43 +3,106 @@

 \author Martin Brain, Peter Schrammel


@owen-jones-diffblue add your name to the author's list or remove it. In general I don't think file author lists make any sense.

allredj · 2018-08-22T14:42:41Z

doc/architectural/compilation-and-development.md

+they should all be testing the same thing. Each test directory contains
+input files and one or more test description files,
+which have the ending `.desc`. The test description files describe what command
+to run, what output is expected and so on. The test framework is an in-house


⛏️ Remove in-house. Most of the code is "in-house" (and that part is not one we're particularly proud of).

Would you accept "hand-rolled"?

allredj · 2018-08-22T14:43:09Z

doc/architectural/compilation-and-development.md

+`regression/` there is a directory for each of the tools/modules. Each of
+these contains multiple test directories, with names describing
+what they test. When there are multiple tests in a test directory then
+they should all be testing the same thing. Each test directory contains


I have the same comment. Maybe be more specific about what a "thing" is.

owen-mc-diffblue · 2018-08-23T16:33:46Z

I've pushed a PR addressing many of the comments. Work left:

how to run tests (make, directly, ctest)
test.pl arguments for excluding specific tests

thk123

A huge improvement - thanks. The suggested outstanding stuff would of course be good, but I think this is already a useful step forward.

thk123 · 2018-08-24T11:17:37Z

doc/architectural/compilation-and-development.md

+will run all of the tests that are  labelled CORE in the desc files and unit
+tests. `-V` makes it print out more
+useful output and `-L CORE` makes it only run tests that have been tagged
+`CORE`. `-R regular_expression` can be used to limit which tests are run, and


💡 provide an example

ctest -L CORE -V -R goto-analyzer will run all the CORE tests in regression/goto-analyzer

peterschrammel · 2018-08-30T07:40:50Z

@owen-jones-diffblue, please amend the PR to cover the two remaining items. Then it looks good to go.

owen-mc-diffblue · 2018-08-30T13:34:50Z

I've addressed the final review comments. I'm aware there are still some areas where this could be improved, e.g. running the tests using make or directly. I am not familiar with those areas, so either people should suggest specific things that should be mentioned in review comments, or these areas should be improved by others who are more familiar with them in follow-up PRs.

tautschnig · 2018-08-30T14:00:00Z

doc/architectural/compilation-and-development.md

@@ -1,45 +1,149 @@
 \ingroup module_hidden 
 \page compilation-and-development Compilation and Development

-\author Martin Brain, Peter Schrammel
+\author Martin Brain, Peter Schrammel, Owen Jones


I've seen @peterschrammel comment on this elsewhere: are authors being recorded or removed?

I think the conclusion was to record the authors - there were a few arguments for it (more difficult to git praise these pages, recognition of doc contributors).

Update compilation and development docs

2e9bcb4

owen-mc-diffblue requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners August 21, 2018 15:38

peterschrammel added the documentation label Aug 21, 2018

peterschrammel reviewed Aug 21, 2018

View reviewed changes

peterschrammel assigned thk123 and allredj Aug 21, 2018

thk123 reviewed Aug 22, 2018

View reviewed changes

allredj approved these changes Aug 22, 2018

View reviewed changes

peterschrammel assigned owen-mc-diffblue and unassigned thk123 and allredj Aug 22, 2018

Owen Jones added 2 commits August 23, 2018 17:29

CMake support is no longer experimental

95eae59

Address most review comments

f88a065

owen-mc-diffblue force-pushed the doc/compilation-and-development branch from c87d30f to f88a065 Compare August 23, 2018 16:32

thk123 approved these changes Aug 24, 2018

View reviewed changes

Address more review comments

3f9d01f

owen-mc-diffblue assigned peterschrammel and unassigned owen-mc-diffblue Aug 30, 2018

tautschnig approved these changes Aug 30, 2018

View reviewed changes

peterschrammel approved these changes Aug 30, 2018

View reviewed changes

peterschrammel assigned owen-mc-diffblue and unassigned peterschrammel Aug 30, 2018

peterschrammel merged commit 1dfc476 into diffblue:develop Aug 31, 2018

owen-mc-diffblue deleted the doc/compilation-and-development branch September 3, 2018 05:33


		### Regression tests ###
		There is experimental support for compiling using CMake. Instructions are

Update compilation and development docs #2789

Update compilation and development docs #2789

Uh oh!

Conversation

owen-mc-diffblue commented Aug 21, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

owen-mc-diffblue commented Aug 23, 2018

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel commented Aug 30, 2018

Uh oh!

owen-mc-diffblue commented Aug 30, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!