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

Don't error on deprecated warnings in ocaml code #841

Merged
merged 2 commits into from
Jul 24, 2024

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@ppedrot
Copy link
Member

ppedrot commented Jul 23, 2024

CI green, is this reasonable a change?

@gares
Copy link
Member

gares commented Jul 23, 2024

I thought the dev provide has -warn-error -all (assuming this is the right syntax to tell dune that warnings are warnings).
So this PR is fine, but it could go one step furhter.

language-server/dune Outdated Show resolved Hide resolved
@gares
Copy link
Member

gares commented Jul 23, 2024

still, if you are about to add a warning in master, then the job coq-master, fatalwarnings is going to fail anyway.
I can help fixing the usages of the deprecated symbol

@SkySkimmer
Copy link
Contributor Author

dev profile is warn-error +all not -all

@gares
Copy link
Member

gares commented Jul 23, 2024

I'm not sure I get it. In the file edited by this PR we redefine the dev profile and we add the fatalwarnings one.
In the dev profile we want warnings to be warnings.
In the fatalwarnings profile we want warnings to be errors.

Did we screw up @SkySkimmer ?

@SkySkimmer
Copy link
Contributor Author

In the dev profile we want warnings to be warnings.

That is the opposite of the dune default but you can do that if you want.

Note that coq CI currently uses the dev profile.

@gares
Copy link
Member

gares commented Jul 23, 2024

That is the opposite of the dune default but you can do that if you want.

I know, they are wrong.

Note that coq CI currently uses the dev profile.

Looks reasonable to me. Maybe the coq CI should use a build system independent way to force warning as errors, and we should honor that in our makefile. Basing on the dune profile cannot cut it (some projects don't even use dune).

@SkySkimmer
Copy link
Contributor Author

I don't think deprecation warnings should be errors in coq CI, the point of deprecating something is to let the 3rd party developers write the adaptation in their own time instead of blocking the coq PR.

@SkySkimmer
Copy link
Contributor Author

Maybe the coq CI should use a build system independent way to force warning as errors

that sounds impossible to me

@SkySkimmer
Copy link
Contributor Author

Shall we merge?

@gares gares merged commit ed38de0 into coq:main Jul 24, 2024
23 checks passed
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.

3 participants