Dear Coq Discourse,
I have a question regarding how warnings are handled in .mlg files / coq.pp stanzas whilst building plugins with dune, and how one should go about setting up projects accordingly.
Context
I am a reasonably competent coq end-user who has being trying to get into plugin development. If you have been following my last couple of posts you would know that I have been struggling to move my workflow from using a make-file approach onto dune. I’m happy to report that over the last few days I managed to piece together a dune project structure that allows me to have a workflow comparable to that of the make-file approach, i.e. I can now work efficiently building coq-theories with dune.
All that remains for me is to establish a good workflow for developing plugins with dune. I have recently followed this tutorial on building plugins with coq & dune and have managed to get a simple hello world plugin to work. Which is great, it means from this point I can start in earnest with diving into learning plugin development.
There was however one unexpected hiccup I encountered when following the tutorial when compiling/building the mlg file for the plugin, which through a little bit of google-fu I managed to navigate through, but it does present a potential issue when building coq-plugins that I would appreciate the received wisdom from the coq community on:
I have assembled together my test-repo into a small git repo that is essentially just the dune project developed in the tutorial I linked above but with some files and variables renamed.
Question
In the syntax.mlg file for my test plugin, When compiling the project (which i do using dune build --cache=disabled) the file is compiled down into a internal ml file used by coq and in that file a warning for an unused variable is generated. This causes my dune to error-out of the build process with the error:
File "plugin/syntax.mlg", line 5, characters 68-71:
Error (warning 27 [unused-var-strict]): unused variable loc.
Looking into the error and generated syntax.ml file there is indeed a variable loc that is created that is unused. After doing some googling for a quick solution to get dune to ignore warnings as errors I found a solution of adding (env (dev (flags (:standard -warn-error -A)))) to get dune to blanket ignore warnings as errors.
Unless I have made a mistake in my project, it is clear from this that whatever process dune/coq/ocaml uses to compile .mlg to ml files does not ensure that there aren’t any unused variables. Thus it strikes me that any dune project that builds plugins aught to have some protections in its dune files to prevent this eventuality from breaking a build.
So my question is as follows:
To those that build coq plugins, has anyone else stumbled upon this issue? If so how do you solve it in your project?
Whilst personally I’m not a fan of treating warnings as errors across the board in general, as it can (like in this case) cause an undue brittleness in ones code. I have a feeling that my quick solution is probably overkill / naive in some way and may cause problems in instances where one actually does want to treat some parts of a build process to be having warnings. Part of me is thinking that it would be nice to just turn of warnings-as-errors for thus the coq.pp stanzas, so I ask as a secondary question: is that possible?
Note that instead of using opam for my coq, dune, and ocaml installations on my system I am using my package manger (portage) to install this stack of software. I don’t know if this makes a difference to anything happening in this question, but I thought it prudent to note as it could be setting settings in the background that differ from people running straight from opam.
!