Add support for coqdep flags.

[rlepigre]

This includes the following:

• A coqdep_flags field in the env stanza (under coq).
• A coqdep_flags field in the coq.theory stanza.

CC @ejgallego @Alizter.

[rlepigre]

We could discuss whether :standard should be -w +all for coqdep_flags, which I think would make sense.

[Alizter]

Does coqdep from 8.16 support warnings? If not, you might need to guard these features by the Coq version too.

[rlepigre]

Does coqdep from 8.16 support warnings? If not, you might need to guard these features by the Coq version too.

This feature is not about warnings specifically, so it should still be relevant for any Coq version. However, my test relies on warnings, which are not supported in 8.16 though (they are supported since 8.19.

The easiest solution for me would probably to bump the version of Coq used in CI to 8.19.0. How hard would it be?

[rlepigre]

The easiest solution for me would probably to bump the version of Coq used in CI to 8.19.0. How hard would it be?

@Alizter do you know what would need to happen for that?

[Alizter]

I think rather than relying on a particular behaviour of coqdep, we should just observe the flags passed to coqdep instead. Have a look at how I did this for coqdoc in coqdoc-flags.t. You can pass nonsense flags if you like since we are just inspecting _build/log and seeing what arguments are there.

Bumping 8.16 will be a whole other issue for now, since many tests will need to be updated. It's also good to keep this lower bound in the dune CI. Dune + Coq is tested upstream in nixpkgs and coq-nix-toolbox FTR.

[rlepigre]

OK, I went with a slightly different approach for the test, so now everything seems to be fine. Funnily enough, this revealed a bug: I was duplicating the flags coming from the coq.theory stanza. This is now fixed, and as far as I am concerned this MR is ready.

[Alizter]

Looks good. Only two things missing. Firstly, there is a small coq lang changelog in coq.rst that needs updating; secondly, this needs a regular changelog entry in doc/changes/.

[rlepigre]

Looks good. Only two things missing. Firstly, there is a small coq lang changelog in coq.rst that needs updating; secondly, this needs a regular changelog entry in doc/changes/.

OK, done.

[ejgallego]

Thanks @rlepigre , I will have a look tho I'm sure the code is good.

I'm wondering tho if we want to add this new field, is there a valid use case beyond workarounding Coq bugs?

IMHO coqdep is something internal to Coq and shouldn't be exposed to the Dune user.

[Alizter]

@ejgallego Now that coqdep can have warnings enabled/disabled it makes sense for the user to be able to pass flags to it.

[rlepigre]

@ejgallego: warnings are the main reasons for me to want to be able to configure coqdep.

[ejgallego]

I assumed warnings where the culprit indeed. I am OK to add this, but in principle, we should not need this option.

As of today, coqdep master has 5 warnings:

• "cannot-locate-home-dir": this is not relevant to dune, should be always disabled (and in fact, this feature likely removed from coqdep)
• "unknown-option": this should be an error, added to support sloppy makefiles
• "module-not-found": this should be an error, Coq PR already submitted
• "legacy-loading-removed-coqdep": this is indeed a legitimate use case, but Coq could warn about it too. In a couple of versions this could be made an error
• "project-file": related to _CoqProject, should be removed from coqdep

So indeed, I'd still prefer if somehow we document this flag as "internal", as I don't see a real use case for adding warnings to coqdep.

What do you think folks?

[Alizter]

I think put a "We discourage tweaking the flags of coqdep" in the doc and be done with it. If we don't add this, users complain that they cannot hack around Coq issues. If we add it, then we risk encouraging users to do hacky things. I think we keep it and document it as discouraged unless you know what you are doing.

[rlepigre]

I see your point @ejgallego, I don't know what's best at this point. On the other hand, we can indeed do what @Alizter proposes and add a warning in the documentation. We can always remove the feature for version 1.0 if that makes more sense at that point. In the meantime, we need to address more important issues like proper package metadata (as proposed in coq/rfcs#101).

[ejgallego]

Documenting this as "internal" sounds good to me.

[ejgallego]

I think put a "We discourage tweaking the flags of coqdep" in the doc and be done with it.

I have no problem with the above, but what do you folks think about:

• adding a sub-section, at the end of the stanza documentation "internal fields"
• adding the new field to this section, and writing something like "this flag exists for transient use cases, in particular for disabling coqdep warnings, but it should not be used in normal operation"

Meanwhile I will try to remove two of these warnings from coqdep already from upstream.

I'm unfortunately very very busy with unplanned stuff, please feel free to merge if I don't do it myself before Sat.

[ejgallego]

Thanks a lot!

@rlepigre let me know if you would like to update the docs as suggested, otherwise this is ready to go IMHO.

[rlepigre]

Cool, thanks @ejgallego and @Alizter! I tweaked the documentation, let me know if that's enough.

[ejgallego]

Looks good to me, thanks @rlepigre !