Do not treat default warnings as errors in _CoqProject #157
Conversation
|
@andres-erbsen the original reason for the warnings-as-errors thing was that we wanted this project to be warnings-free, and after asking several people in the core team I got permission to use this project as a kind of canary in the coalmine for new warnings that just show up. From your perspective, would it be enough if tags/releases do not error-on-warning? Since this is a plugin, it's only meant to work with single Rocq version, so I think it would be a bug if a new warning showed up in a minor release. How would you organize a project so that it is warning-free at all times? |
|
The dune build (used by the opam file) does -w +default independently of the _CoqProject Line 6 in 7a7f4a6 This could be moved to just the "dev" dune env (add a |
My interest is about whatever version we test (and send overlays to) in Roqc and stdlib CI. So I think the answer is no.
I really don't understand why you want at all times. And this is even though I am strongly on board with the goal of addressing warnings proactively. Is this about putting pressure against addition of new warnings (that may turn out to be unwise when attempting to address them in this repo)? I am obviously not opposed to you fixing any warnings. But, answering the original question: If you really want to have the build of aac treat all warnings as erros, my recommendation would be to have it be a monorepo and monobuild with its actively developed dependencies. This is how stdlib works internally, and it is workable exactly because there is no coordination overhead. And even so, it is a chore with the limited tooling available for Rocq, lacking even an inline-everywhere tool -- we still sometimes silence warnings. Nevertheless, myself and others have advocated for the Rocq ecosystem moving in the monorepo+monobuild direction, perhaps most prominently with coq-universe. But, alas, we seem to be headed some other way. In contrast, the current build configuration seems to be functioning as a change-detector test: if stdlib adds a warning, our build of aac breaks. And it's a particularly hard-to-fix one: as aac and stdlib are in different repositories, this automatically means that we cannot land our changes without interacting with aac maintainers. This blocking of development is what I am principally opposed to. In particular, it entirely defeats the purpose of deprecation warnings -- if we were willing to do a synchronized change, backwards-compatible deprecation would be unnecessary. (If the discussions leading up to the status quo are public, I would be interested in reading them.) Another policy that I've seen work is that PRs to the repo itself (here aac) are prevented from introducing new warnings, but dependencies are not similarly constrained. Instead somebody has treated it as a regular gardening task to address new warnings added by dependencies. I guess another way to have a warning-free build at all times would be to pin the dependencies and leave Rocq+stdlib CI, but that seems to be in nobody's interest. |
|
I'm willing to give every Stdlib and Rocq core maintainer merge access to this repo. But I guess the easier solution is just to merge this PR. |
|
That solution would be acceptable to me -- if you prefer it, let's do it. (As an experiment, just for this repo.) |
|
@andres-erbsen I invited you to join Rocq-community and the organization's team that merges PRs related to Rocq core. This gives you write access to this repo (and others in Rocq CI hosted in the organization). |
3 participants
An important idea behind warnings is that a project's dependencies can mark stuff as deprecated or otherwise anti-recommended before removing that functionality, without requiring an atomic change across the two repositories. Another benefit of this design is that then we can use it to see all instances where a warning is triggered, instead of the build breaking on the first one. Treating warnings as errors even when others build the project with dependency versions that it wasn't developed on breaks this.
Now, you may want to do something other than exactly this PR. It is up to you whether you treat warnings as errors when building against release versions of your dependencies. But since there is no version-conditional logic in the Makefile right now, and this project is under coq-community, I am proposing the simplest change I can think of as opposed to the most fine-grained one.
Context: https://github.com/rocq-prover/stdlib/actions/runs/15409303789/job/43358101546?pr=162#step:12:249