Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Use CWarnings in coqdep #17946

Merged
merged 1 commit into from Sep 7, 2023
Merged

Use CWarnings in coqdep #17946

merged 1 commit into from Sep 7, 2023

Conversation

rlepigre
Copy link
Contributor

@rlepigre rlepigre commented Aug 9, 2023 •
edited

This is a revival of #17483, since it got closed.

Fixes #10156.

  • Added changelog.
  • Added / updated documentation.

@rlepigre rlepigre requested a review from a team as a code owner August 9, 2023 07:40
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 9, 2023
@rlepigre
Copy link
Contributor Author

rlepigre commented Aug 9, 2023 •
edited

CC @ejgallego and @Alizter: this should be useful for dune builds, for which, I believe, all coqdep warnings should be fatal (at least by default).

In our repositories we actually wrap coqdep with code to detect warnings and fail if they come up, which we'd be happy to get rid of eventually.

@rlepigre rlepigre requested a review from a team as a code owner August 9, 2023 08:02
SkySkimmer
SkySkimmer reviewed Sep 5, 2023
View reviewed changes
tools/coqdep/lib/args.ml Outdated Show resolved Hide resolved
SkySkimmer
SkySkimmer reviewed Sep 5, 2023
View reviewed changes
tools/coqdep/coqdep.ml Outdated Show resolved Hide resolved
@SkySkimmer SkySkimmer requested a review from a team September 5, 2023 12:08
@rlepigre rlepigre force-pushed the br/fix-coqdep-warn branch 2 times, most recently from d5ed16d to 5ff73f6 Compare September 6, 2023 07:31
SkySkimmer
SkySkimmer requested changes Sep 6, 2023
View reviewed changes
tools/coqdep/coqdep.ml Outdated Show resolved Hide resolved
tools/coqdep/lib/common.ml Outdated Show resolved Hide resolved
@SkySkimmer
Copy link
Contributor

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 6, 2023
@SkySkimmer SkySkimmer self-assigned this Sep 6, 2023
@SkySkimmer SkySkimmer added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Sep 6, 2023
@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Sep 6, 2023
@SkySkimmer
Copy link
Contributor

Maybe add a changelog?

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 6, 2023
@rlepigre
Copy link
Contributor Author

rlepigre commented Sep 6, 2023

I added the changelog. I don't think user messages change after this MR (only potentially the way they are shown), so probably no update needed.

@rlepigre
[coqdep] Option -w to adjust warnings.
473bd2e 
Co-Authored-By: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
@rlepigre rlepigre requested a review from a team as a code owner September 6, 2023 16:51
@rlepigre
Copy link
Contributor Author

rlepigre commented Sep 6, 2023

I also added an entry for the new argument in the coqdep manpage (also fixed a minor layout problem in it).

@SkySkimmer SkySkimmer removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 7, 2023
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit d52a29a into coq:master Sep 7, 2023
6 checks passed
@ejgallego ejgallego added kind: user messages Improvement of error messages, new warnings, etc. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files. labels Sep 11, 2023
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
221d1c1 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
4788bec 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
f597040 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
1a494a0 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 25, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
16812f5 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 30, 2023
@coqbot-app @SkySkimmer @rlepigre
Merge PR coq#17946: Use CWarnings in coqdep
fe6da2c 
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. kind: user messages Improvement of error messages, new warnings, etc. part: coqdep The coqdep binary for resolving dependencies amongst coq .v files.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

coqdep should fail when it cannot find a .v file
3 participants
@rlepigre @SkySkimmer @ejgallego