Add regression test information to COMPILING.md #5781

TGWDB · 2021-01-25T15:10:23Z

This adds information on how to run regression tests using bnoth cmake and make to COMPILING.md.
Also ensures COMPILING.md follows clang-format-7.

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.

REGRESSION_TESTS.md

COMPILING.md

tautschnig · 2021-01-25T15:23:39Z

REGRESSION_TESTS.md

+This document assumes you have already been able to build CPROVER on
+your chosen architecture. For details on building CPROVER see
+COMPILING.md.


Could we please merge this documentation with doc/architectural/compilation-and-development.md rather than adding another file?

Happy to merge this file with another one. I started a draft pull request to make sure I wasn't putting bad information in or adding things in the wrong place. If we all agree on doc/architectural/compilation-and-development.md as the right location I'll move everything there.

Thank you for bringing up all these gaps in our documentation, and coming up with fixes for these! I'd just like to make sure we don't have the documentation in multiple places. I'm no longer able to tell what's actually needed for someone to get started, and where they might be looking for documentation. Is perhaps CONTRIBUTING.md (which we don't currently have) the canonical place for people to get started?

I'm happy to try and sort it all out. I'm using myself as a test subject for this (before I know my way around well), so hopefully do not create too many (draft) proposals to change things that are explained somewhere.

For (a possible) CONTRIBUTING.md, would this also include the various links and information on policies for style and committing?

If we had a CONTRIBUTING.md, perhaps it could serve as a collection of pointers towards documentation, pointing people to COMPILING.md, CODING_STANDARD.md, and the sections of the manual (such as doc/architectural/compilation-and-development.md).

Btw, the documentation is published at http://cprover.diffblue.com (see link on top fo README)

What is our link preference here, should we link to http://cprover.diffblue.com/ or do we reference inside the repository since that page is generated from doc/architectural/front-page.md ?

README.md references http://cprover.diffblue.com/, so I'd go with that in top-level files (README.md, COMPILING.md, CODING_STANDARD.md, and possibly any files to be added at that level).

REGRESSION_TESTS.md

hannes-steffenhagen-diffblue · 2021-01-25T15:41:49Z

@tautschnig This CSmith check just failed: https://github.com/diffblue/cbmc/pull/5781/checks?check_run_id=1762881802

How do we interpret that?

codecov · 2021-01-25T15:48:27Z

Codecov Report

Merging #5781 (1e919e6) into develop (763f6a2) will increase coverage by 0.08%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5781      +/-   ##
===========================================
+ Coverage    74.90%   74.98%   +0.08%     
===========================================
  Files         1447     1447              
  Lines       158198   158214      +16     
===========================================
+ Hits        118491   118637     +146     
+ Misses       39707    39577     -130

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	`93.75% <ø> (ø)`
src/goto-instrument/code_contracts.cpp	`85.45% <100.00%> (+0.10%)`	⬆️
src/util/c_types.h	`100.00% <100.00%> (+1.80%)`	⬆️
src/ansi-c/gcc_types.cpp	`41.86% <0.00%> (-46.52%)`	⬇️
src/ansi-c/scanner.l	`40.71% <0.00%> (-21.02%)`	⬇️
src/ansi-c/literals/convert_float_literal.cpp	`73.80% <0.00%> (-19.05%)`	⬇️
src/ansi-c/literals/parse_float.cpp	`83.65% <0.00%> (-12.50%)`	⬇️
src/ansi-c/c_typecheck_code.cpp	`66.26% <0.00%> (-11.66%)`	⬇️
src/ansi-c/c_storage_spec.cpp	`86.84% <0.00%> (-10.53%)`	⬇️
src/util/std_types.cpp	`83.95% <0.00%> (-4.94%)`	⬇️
... and 31 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 66d9d17...1e919e6. Read the comment docs.

tautschnig · 2021-01-25T16:40:25Z

@tautschnig This CSmith check just failed: https://github.com/diffblue/cbmc/pull/5781/checks?check_run_id=1762881802

How do we interpret that?

See #5780 - hoping for @kroening or @chrisr-diffblue to review this ASAP.

chrisr-diffblue · 2021-05-17T11:33:54Z

COMPILING.md

@@ -482,3 +482,42 @@ successfully on Windows or macOS.
   The argument for the IPASIR parameter gives the build system the location for
   the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
   compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
+This document assumes you have already been able to build CPROVER on
+your chosen architecture. For details on building CPROVER see
+COMPILING.md.


Since this content is in COMPILING.md - maybe its better to say see section BLAH ?

chrisr-diffblue · 2021-05-17T11:37:02Z

COMPILING.md

+simply running make as follows.
+```
+cd regression
+make


I believe there's a slight difference between cmake/make in what tests actually run, which might be worth either clarifying, or adjusting the instructions to elide. That is around unit tests... I believe the ctest commands run both regression and unit tests, whereas I though the make command you show here only runs the regression tests. My recommendation might be to tweak the section title to say "RUNNING REGRESSION AND UNIT TESTS", and then tweak the instructions for make to show how to run unit tests as well?

I think this is clearer now.

This adds information on how to run regression tests using bnoth cmake and make to COMPILING.md. Also ensures COMPILING.md follows clang-format-7.

chrisr-diffblue

Thanks, thats a great addition to the docs!

hannes-steffenhagen-diffblue reviewed Jan 25, 2021

View reviewed changes

REGRESSION_TESTS.md Outdated Show resolved Hide resolved

COMPILING.md Outdated Show resolved Hide resolved

TGWDB force-pushed the compiling-documentation branch from e754c25 to c4f2b7b Compare January 25, 2021 15:17

tautschnig reviewed Jan 25, 2021

View reviewed changes

TGWDB mentioned this pull request Feb 1, 2021

Tools overview #5792

Merged

6 tasks

tautschnig assigned TGWDB May 10, 2021

TGWDB force-pushed the compiling-documentation branch 2 times, most recently from 21de8d4 to c48457f Compare May 17, 2021 09:24

TGWDB changed the title ~~Compiling documentation~~ Add regression test information to COMPILING.md May 17, 2021

TGWDB marked this pull request as ready for review May 17, 2021 10:34

TGWDB requested review from chrisr-diffblue, kroening and smowton as code owners May 17, 2021 10:34

chrisr-diffblue reviewed May 17, 2021

View reviewed changes

TGWDB force-pushed the compiling-documentation branch 2 times, most recently from d83dccb to 1e919e6 Compare May 21, 2021 08:56

Add regression test information to COMPILING.md

1e919e6

This adds information on how to run regression tests using bnoth cmake and make to COMPILING.md. Also ensures COMPILING.md follows clang-format-7.

TGWDB requested a review from chrisr-diffblue May 21, 2021 11:06

chrisr-diffblue approved these changes May 27, 2021

View reviewed changes

TGWDB merged commit 2985aca into diffblue:develop May 27, 2021

Add regression test information to COMPILING.md #5781

Add regression test information to COMPILING.md #5781

Uh oh!

Conversation

TGWDB commented Jan 25, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Uh oh!

hannes-steffenhagen-diffblue commented Jan 25, 2021

Uh oh!

codecov bot commented Jan 25, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig commented Jan 25, 2021

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!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

TGWDB commented Jan 25, 2021 •

edited

Loading

codecov bot commented Jan 25, 2021 •

edited

Loading