Ralf Jung (Sep 03 2020 at 07:32): Ralf Jung (Sep 03 2020 at 07:32):Is there a way to turn warnings into errors, but only those warnings that I have actually enabled? Basically, I want to ensure that compilation completes without showing any warnings. I tried -w +all but that also enables extra warnings that would not be shown at all without this flag. Basically, I want the equivalent of #[deny(warnings)]/-D warnings in Rust. Is that possible?
Ralf Jung (Sep 03 2020 at 07:37):For now I am grepping the build log, but that is not a great solution^^
Christian Doczkal (Sep 03 2020 at 09:49):how about -w +default? According to the manual this should work :shrug:
Ralf Jung (Sep 03 2020 at 09:55):that doesnt sound like it will respect the -w -notation-overridden flags that I added
Ralf Jung (Sep 03 2020 at 09:56):I have one place (_CoqProject) where I configure which things we warn about, and now in another place (CI configuration) I'd like to say "oh and make all those warnings, and only them, errors". C compilers have such a flag (-Werror), Rust has it (-D warnings), but it seems like Coq does not?
Théo Zimmermann (Sep 03 2020 at 10:16):Make a custom _CoqProject file (or patch it during CI) and put -arg -w -arg +default before -arg -w -arg -notation-overridden (order matters). Or use Dune when building in CI.
Ralf Jung (Sep 03 2020 at 10:27):patching _CoqProject on CI sounds about as hacky as grepping the build output^^
Ralf Jung (Sep 03 2020 at 10:28):also, this will stop working once we use _CoqProject to enable further warnings -- it wouldnt turn them into errors.
Théo Zimmermann (Sep 03 2020 at 10:30):Well, the Dune solution is still likely to work and it should even allow you to define several profiles, one of them being warn-as-errors that you could run both on CI and locally when you feel like.
Théo Zimmermann (Sep 03 2020 at 10:31):Note that our experience in the Coq development team is that activating warnings as errors in CI but not locally in developer mode leads to frustration and waste of time.
Théo Zimmermann (Sep 03 2020 at 10:31):Developers want to be confident that what they submit will build if they've built it locally first.
Ralf Jung (Sep 03 2020 at 10:33):Théo Zimmermann said:
Note that our experience in the Coq development team is that activating warnings as errors in CI but not locally in developer mode leads to frustration and waste of time.
I dont have any experience with this on the Coq side, but this is exactly what we do in Rust and it works very well. Developers still see the warnings, after all, you just might want to ignore them during development.
Ralf Jung (Sep 03 2020 at 10:34):However, Coq is worse off here since warnings can hide in parts of the code that are not rebuilt; Rust caches diagnostics so even when just parts of a crate are rebuilt, all warnings are shown.
Théo Zimmermann (Sep 03 2020 at 10:35):At least in Dune, if you change the flags that are used to build (e.g. by switching profiles), every file will be rechecked.
Ralf Jung (Sep 03 2020 at 10:36):Théo Zimmermann said:
Developers want to be confident that what they submit will build if they've built it locally first.
I also want to be confident that things build without warnings, so IMO enabling it on CI is a must. This just means that I finally need to set up something bors-like so CI can tell us about such things before the code ends up on master.
Ralf Jung (Sep 03 2020 at 10:36):Théo Zimmermann said:
Well, the Dune solution is still likely to work and it should even allow you to define several profiles, one of them being warn-as-errors that you could run both on CI and locally when you feel like.
I dont see how dune can do anything here without coq support
Ralf Jung (Sep 03 2020 at 10:37):it sounds like with profiles I can have different flags, but when enabling a new warning I'd still have to enable it both in the strict CI profile and the normal "just warn" profile
Ralf Jung (Sep 03 2020 at 10:37):so there'd still be redundancy and a chance for things to go out of sync
Ralf Jung (Sep 03 2020 at 10:37):if I'd be willing to accept that I could just as well use COQEXTRAFLAGS
Théo Zimmermann (Sep 03 2020 at 11:35):so there'd still be redundancy and a chance for things to go out of sync
Sure, but the two profiles can be defined in the same file on two consecutive lines, so it's easy to avoid going out of sync.
Ralf Jung (Sep 03 2020 at 12:32):okay so it's a slightly better hack then...
Last updated: Oct 13 2024 at 01:02 UTC