Emilio Jesús Gallego Arias (Jun 22 2022 at 18:58): Emilio Jesús Gallego Arias (Jun 22 2022 at 18:58):Hi all, there was a bit of discussion w.r.t. warnings and Dune at the hacking event. @Ali Caglayan is experimenting with adding a separate (warnings ...) field, however that would require either some coupling to Coq's command line, or allowing duplication of warning settings with (flags ...)`.
@Rudi Grinberg mentioned that it'd be nice if Coq could communicate the warnings, there was a PR for that https://github.com/coq/coq/pull/11901, but it is tricky for a few reasons. Moreover, Coq will already warn if you are using a bad warning.
For me, the warnings field doens't provide a lot of advantages, but I may be wrong. I see more advanced warning machinery going to LSP servers, with fixes, etc...
Thoughts around here?
Ali Caglayan (Jun 22 2022 at 19:31):Coq will already warn if you are using a bad warning.
$ touch a.v
$ coqc -w +foo a.v
$ coqc -w -foo a.v
No warning about this
Emilio Jesús Gallego Arias (Jun 22 2022 at 19:39):Ali Caglayan said:
Coq will already warn if you are using a bad warning.
$ touch a.v $ coqc -w +foo a.v $ coqc -w -foo a.vNo warning about this
that's due to plugins declaring new warnings, used to be a mode to enable coqc to emit that warning, or maybe it only does when you use the warnings vernacular. That's a big problem, due to plugins and command line.
Gaëtan Gilbert (Jun 22 2022 at 20:33):see https://github.com/coq/coq/commit/965960bcd13eb3a6e531b03fb85be516dcdca551
Ali Caglayan (Jun 22 2022 at 20:39):We should add this back in under some sort of option/flag. That way Dune can be stricter with used warnings. Together with a way to declare warnings from coqc, it should allow dune to explicitly pass around which warnings are allowed behind the scenes. Plugin authors could then have a plugin stanza or something where they declare the warnings their plugin uses.
Ali Caglayan (Jun 22 2022 at 20:39):Just an idea tho.
Emilio Jesús Gallego Arias (Jun 23 2022 at 13:15):What problem does that solve?
Emilio Jesús Gallego Arias (Jun 23 2022 at 13:16):Having a list of warnings is useful for documentation, but for Dune?
Emilio Jesús Gallego Arias (Jun 23 2022 at 13:16):If coqc already can do it, why does dune need to get involved?
Rodolphe Lepigre (Jun 23 2022 at 15:40):This seems to me like a pretty minor issue, compared to what is still missing in dune to fully support complex Coq projects. Moreover, having to declare warnings that are registered in plugins in a plugin stanzas seems quite annoying as well: how would you verify that the declaration matches the warning registration done in the plugin? For now I think I would just keep ignoring the problem: how often does it really come up anyway?
I think the main use-cases around warnings are the following:
In both cases, it is pretty easy to realise your error, I think.
Emilio Jesús Gallego Arias (Jun 23 2022 at 15:50):Yes, it doesn't worry too much, what you are missing most @Rodolphe Lepigre ?
Emilio Jesús Gallego Arias (Jun 23 2022 at 15:50):we did some crucial work yesterday, that should allow us to properly scan user-contrib
Rodolphe Lepigre (Jun 23 2022 at 15:56):That's good to hear!
Here is what I'm mainly still missing:
dune coq top in PG and other editors (including stuff like "jump to definition" which needs a file path hack).coqc is interpreting a file (or redirect it to a file, with the possiblity to test that the result is as expected perhaps, or as a separate thing).There are probably other things, but that's all I can think of right now. Maybe @Paolo Giarrusso remember more things we'd like to have.
Rodolphe Lepigre (Jun 23 2022 at 15:58):Also, a proper support for plugins that have deps. :)
Rodolphe Lepigre (Jun 23 2022 at 16:05):I also noticed a more minor issue: If you have two plugins being built in a directory, and a theory that depends on both but (by mistake) only declares one as dependency, then dune will not complain if the .cmxs files happen to have been build prior to compiling the Coq code. Basically Coq is just able to grab a .cmxs file that happens to be in its path, but that it should really not be allowed to use. I should probably write an issue for that, but I don't have time right now.
Emilio Jesús Gallego Arias (Jun 23 2022 at 17:26):Rodolphe Lepigre said:
- Being able to have several (inter-dependent) opam packages that contain Coq code in a single repo.
You should be able to do that as long indeed as you don't install the packages. So at least you can start testing the setup and composed build.
- Proper support for `dune coq top` in PG and other editors (including stuff like "jump to definition" which needs a file path hack).
Can't you just do coq-prog-name=dune coq top in Emacs? For PG and _build the hack is minimal.
- Proper support for vos/vok builds.
That needs a bit of work but it is doable if someone has the cycles, the rules are very close, we just need to have a different object file directory to avoid races with regular .vo compilation.
A way to silence the ouput printed while `coqc` is interpreting a file (or redirect it to a file, with the possiblity to test that the result is as expected perhaps, or as a separate thing).
Yes, there is an open issue about this, see https://github.com/coq/coq/issues/12923
Paolo Giarrusso (Jun 24 2022 at 01:02):@Rodolphe Lepigre for plugins with deps don't you just need Coq 8.16? That's why they moved to loading via findlib
Rodolphe Lepigre (Jun 24 2022 at 06:26):Emilio Jesús Gallego Arias said:
Can't you just do
coq-prog-name=dune coq topin Emacs? For PG and _build the hack is minimal.
I think that does not work, but I don't remember the details. I'm really hopeless with emacs and its configuration, so I would really appreciate guidelines on how to set things up properly if you know how to do this cleanly. And we should also find someone willing to create a PR that adds support to PG. (I really can't take care of this, I just have no clue how emacs works: I only use it for PG.)
When we were looking into this with @MackieLoeffel and others, we found some hacks to make things work, but they were not really acceptable on their own. We at least need a way to easily enable/disable them on a per-project basis. Or ideally, detect that the project is built with dune and enable the tweaks automatically.
Emilio Jesús Gallego Arias (Jun 24 2022 at 07:44):I am also not a great emacs expert. Tuareg has a very simple hack tho, which is to test for _build/default and then locate the source file stripping that prefix.
Emilio Jesús Gallego Arias (Jun 24 2022 at 07:45):Yes, note that in 8.15 it is also possible, you just need to load the deps manually.
Ali Caglayan (Jun 26 2022 at 10:43):Anyway to conclude my thoughts on this since the discussion got a bit sidetracked. I only added a feature that added a warnings field to the coq.theory stanza. Its not complicated and doesn't do something fancy, but it could be the beginning of more high level reasoning about warnings. I reject your reasoning that this can be done from the command line, since that is true for almost every field in the coq stanza.
Many projects keep an explicit list of enabled or disabled warnings. Having a dedicated field is simply to encourage this use case. We could imagine a future Coq warning infrastructure which handles warnings in a different way, or worry about coupling to the command line, but today we are already coupled and I am talking about here and now.
Having a higher level field for warnings would let users be uncoupled from their coq version when writing their dune file and let us do more smart things in dune if needed. We can detect the version of Coq in Dune soon anyway. You seemed to be worrying about Coq versions changing the command line syntax for warnings. I think this is really not that big of an issue.
Here is the PR for others reading https://github.com/ocaml/dune/pull/5908.
Anyway, I don't want to spend any more time talking about it since it is such a simple feature. I'm just baffled by the resistance so I thought I may as well explain myself a bit more.
Paolo Giarrusso (Jun 26 2022 at 13:08):theories is higher-level than the command-line options it translates to. Ali Caglayan (Jun 26 2022 at 13:10):I'm thinking more along the lines of Dune could interface with Coq and find out more information about which warnings are set, having default warning sets, developer warning sets. More information about deprecation, better user suggestions etc.
Ali Caglayan (Jun 26 2022 at 13:10):The reason to introduce it now is so that people get used to using it.
Ali Caglayan (Jun 26 2022 at 13:11):I've been looking at many _CoqProject files, and a typical feature is a list of warnings. There may be other flags, but that is not as common.
Ali Caglayan (Jun 26 2022 at 13:11):I'm not suggesting that this is a great feature and is really important to include, it's not at the moment.
Ali Caglayan (Jun 26 2022 at 13:12):I'm just trying to understand why there is any resistance to the idea.
Gaëtan Gilbert (Jun 26 2022 at 13:14):for ocaml we have warnings in (flags), why do different for coq?
Paolo Giarrusso (Jun 26 2022 at 13:20):@Ali Caglayan I’d encourage you to rephrase your argument in terms of concrete advantages in falsifiable terms. That helps debate the advantages (still unclear) against the costs (more code, maintenance, needed documentation, transition, etc)
Paolo Giarrusso (Jun 26 2022 at 13:22):I take for granted that any costs are likely small, but IMHO this shouldn’t necessarily mean the motivation need not be clear.
Paolo Giarrusso (Jun 26 2022 at 13:26):and I also agree with Rodolphe above on priorities
Ali Caglayan (Jun 26 2022 at 13:28):Compare
(flags
-color on
-w -projection-no-head-constant
-w -redundant-canonical-projection
-indices-matter
-w -notation-overridden
-w +duplicate-clear
-w +non-primitive-record
-w +undeclared-scope
-w -deprecated-hint-without-locality
-w -deprecated-hint-rewrite-without-locality)
with
(flags
-color on
-indices-matter)
(warnings
:my_standard_warnings
+duplicate-clear
-redundant-canonical-projection)
That's all I have to offer with this.
Ali Caglayan (Jun 26 2022 at 13:29):I am not spending all my time thinking about warnings btw, I am most spending time on important features for coq.theory. This was just something that I didn't expect to cause so much debate. 0:-)
Gaëtan Gilbert (Jun 26 2022 at 14:01):what's my_standard_warnings
Ali Caglayan (Jun 26 2022 at 14:05):Its a set of warnings the user can define
Ali Caglayan (Jun 26 2022 at 14:05):The warnings field uses the set language of dune, so we can define sets, combine them, minus them etc.
Ali Caglayan (Jun 26 2022 at 14:06):If you have a project with multiple theories you won't have to copy and past the warnings all the time, you could define a set that you want and use that instead.
Gaëtan Gilbert (Jun 26 2022 at 14:12):why not just put the warnings at toplevel? in coq we have multiple (library) but we don't repeat the warnings for them
Paolo Giarrusso (Jun 26 2022 at 14:13):ah, thanks for spelling out what is higher-level: the set language lets you remove warnings, while subtraction would be less-well defined if you used :my_standard_warnings or :your_custom_warnings. OTOH, Coq already has subtraction and lets you toggle warnings anyway, even if you use strings…
Paolo Giarrusso (Jun 26 2022 at 14:17):indeed (re Gaëtan’s point), Rodolphe showed me I could set warnings in a root dune via
(env
(dev
(coq
(flags
(:standard
;see https://gitlab.mpi-sws.org/iris/iris/-/blob/master/_CoqProject
-w -notation-overridden
-w -redundant-canonical-projection
-w -convert_concl_no_check
-w -ambiguous-paths
; Similar to notation warnings.
-w -custom-entry-overridden
-w -ssr-search-moved
; Turn warning on hints into error:
-w +deprecated-hint-without-locality
-w +deprecated-instance-without-locality
-w +unknown-option
)))))
Gaëtan Gilbert said:
why not just put the warnings at toplevel? in coq we have multiple (library) but we don't repeat the warnings for them
This is also an option, but I am trying to support a use case many users are doing which is to declare all their warnings in _CoqProject.
Gaëtan Gilbert (Jun 26 2022 at 15:46):how's _CoqProject relevant to dune?
Théo Zimmermann (Jun 27 2022 at 07:09):Users use _CoqProject to define warnings because that's the best they have to do this right now. However, I fail to see how this is different from setting warnings in the root dune file.
Emilio Jesús Gallego Arias (Jun 27 2022 at 11:55):The downsides to the current proposal are:
The advantages are:
Emilio Jesús Gallego Arias (Jun 27 2022 at 11:55):So the advantages are purely aesthetical, but the downsides are now, moreover this is not really a blocker for anyone as it all saves is a bit of typing
Emilio Jesús Gallego Arias (Jun 27 2022 at 11:56):so overall that's for now a not very interesting proposal in the current form. How to handle warnings overall it is very intersting, for IMHO goes well beyond Dune as of today
Last updated: Jun 04 2023 at 23:30 UTC