Skip to content

Unify make and cmake behaviours #5993

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.

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

Closed
wants to merge 3 commits into from

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented Apr 1, 2021

This fixes the inconsistencies between cmake and make
behaviours.

Fixes #5986

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

Comment on lines 16 to 17
@$(MAKE) -f $(THIS_FILE) test-paths-lifo
@$(MAKE) -f $(THIS_FILE) test-cprover-smt2
Copy link
Collaborator

Choose a reason for hiding this comment

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

How about making the test target depend on test-paths-lifo and test-cprover-smt2?

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes, either that, or make default target depend on test-paths-lifo and test-cprover-smt2?

Copy link
Contributor

Choose a reason for hiding this comment

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

One issue to consider here is: if we add these additional targets as dependencies for test, we wouldn't be able to run "just test" ...

Copy link
Collaborator

Choose a reason for hiding this comment

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

Good call. The right approach probably is to rename the existing test target and introduce a new (PHONY) test target.

@codecov
Copy link

codecov bot commented Apr 1, 2021

Codecov Report

Merging #5993 (bc54138) into develop (a188777) will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5993   +/-   ##
========================================
  Coverage    77.79%   77.79%           
========================================
  Files         1567     1567           
  Lines       179707   179707           
========================================
  Hits        139797   139797           
  Misses       39910    39910           

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 58d64d8...bc54138. Read the comment docs.

@tautschnig
Copy link
Collaborator

I'm wondering whether tests would pass if this were rebased onto current develop, which includes #5985.

@TGWDB TGWDB force-pushed the regression-test-cleanup branch from ce343c9 to b787c13 Compare April 6, 2021 12:32
done;

# Pattern to execute a single test suite directory
.PHONY: $(DIRS)
$(DIRS):
@echo "Running $@..." ;
$(MAKE) -C "$@" || exit 1;
$(MAKE) -C "$@" test || exit 1;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Wouldn't test-parallel (below) also need this change?

TGWDB added 3 commits May 12, 2022 16:17
This fixes the inconsistencies between cmake and make
behaviours.
Change from calling the separate make targets inside a default
to instead using make dependency style.
@TGWDB TGWDB force-pushed the regression-test-cleanup branch from 7340252 to bc54138 Compare May 12, 2022 15:20
@TGWDB TGWDB closed this Aug 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Several inconsistenties in regression test build scripts
3 participants