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.

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

dune: make Coq warnings fatal when building locally #1762

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Sep 18, 2023

When building with the dev profile, we make all Coq warnings fatal.

The dev profile is selected by default when building locally. Only the opam package CI job builds dune with the release profile where the warnings will not be fatal.

We need to think about this some more, since warnings might be introduced outside of our control which would make development annoying. I'll probably end up using another profile like warn-error so that dune build --profile warn-error would be strict about warnings.

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

cc @jdchristensen how do you feel about this?

@jdchristensen
Copy link
Collaborator

@Alizter I'm not sure. I guess it depends how often this would cause an issue. It might be annoying if I want to test a newer version of Coq, and have to deal with warnings. I guess warnings are called warnings because they aren't meant to be fatal errors, so maybe this isn't the best way to go? In general, with so little development on this repo, I'd like to have the procedures as light-weight as possible.

@jdchristensen
Copy link
Collaborator

@Alizter BTW, why does the CI on this PR show double the number of checks compared to usual?

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

@jdchristensen Looks like I accidentally created a branch in this repo rather than my fork.

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 18, 2023

I'll close this anyway as it doesn't really gain us much. It was useful for me when fixing the warnings but that isn't worth any potential difficulty it introduced.

@Alizter Alizter closed this Sep 18, 2023
@Alizter Alizter deleted the ps/branch/dune__make_coq_warnings_fatal_when_building_locally branch September 18, 2023 17:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants