I just realized that dune calls coqc
without -q
, hence loading ~/.coqrc
[2]; that differs from coq_makefile
[2] and generally makes build results less reproducible. I can add -q
to coq flags, but it seems dune should do it?
coq_makefile
seems right here: we can't share libraries if they depend on local coqrc
state.coqrc
for protyping settings, like #[global] Set Nested Proofs Allowed.
and #[global] Unset SsrIdents.
, that I don't want in my compiled code. (The latter requires loading ssreflect, which I'm going to debate with myself).[1] https://coq.inria.fr/refman/practical-tools/coq-commands.html#by-resource-file
[2] From coq_makefile's output:
# these flags do NOT contain the libraries, to make them easier to overwrite
COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
@Paolo Giarrusso is this still the case in Dune 2.9 ?
We added -q
to the default set of flags some time ago, maybe you are overriding them in your own (flags ...)
declaration
Remember that you need to pass :standard
if you want default flags to be preserved
I wasn't aware of :standard
.
I'll try adding it, thanks.
I'm also looking at the occurrences in https://dune.readthedocs.io/en/stable/dune-files.html#dune, and after reviewing the occurrences of :standard
and flags
, I'm not sure how one would figure this out :-|.
okay, :standard
seems exactly -q
, thanks! (all on dune 2.9.0).
Indeed the docs need a lot of improvement, [even the deployed version is not 2.9]
Added to document that :standard is -q to my TODO
Yeah this confusion with missing :standard
is a bit common both in OCaml and Coq
But I don't see a way to expose the current set of flags while at the same time allowing users to fully override it
There was some discussion on flags recently, that's a very interesting subject [flags that alter rules for example] , but I feel we are short on manpower to do a lot more
so the bottom line is that best practice is to always add :standard
, like so?
(flags :standard
-w -notation-overridden
-w -notation-incompatible-format
-w -ambiguous-paths)
Emilio Jesús Gallego Arias said:
But I don't see a way to expose the current set of flags while at the same time allowing users to fully override it
have flags
which auto prepends :standard
and override_flags
which behaves like current flags
?
Maybe, but that's a bit ugly, and makes things such as :standard \ foo
a bit more difficult
but indeed it has been a problem in some cases
I guess dune devs are leaning to emitting a warning when you override flags and don't include :standard
such a warning exists now for the stubs
I forgot about \
yeah, the thing is that it is a "set of flags"
many things can be improved about flags IMVHO
and Dune devs know about it, but it is hard to get manpower
as people do care more about speed, caching, IDEs, and features
tbh I'd prefer to have -foo and -no-foo flags with whichever is provided last winning, but that requires a change to the tools
so @Emilio Jesús Gallego Arias can you confirm that we should use :standard
like in my example until something better comes along? Or what do you recommend?
@Karl Palmskog sorry I missed your message
indeed, I think that's the right setup
:standard includes things both inherited and set in the profile
see the tests here https://github.com/ocaml/dune/blob/main/test/blackbox-tests/test-cases/coq/env.t
But yeah it is so easy to forget :standard
that this is an usability issue :S
and :standard
should go before any custom flags in dune
file? I think the order matters, right?
:standard is just expanded to the set of flags that are computed from the workspace and env flags settings
the language dune supports is an "ordered set language"
indeed the order will be one sent to coqc
https://dune.readthedocs.io/en/latest/concepts.html#ordered-set-language
So you can place :standard where you would like it to be
well, I think we are trying to determine where "most people would like it to be, most of the time"
for example, if I have a Coq library, does :standard <custom flags>
give my clients the most flexibility?
I guess o
I guess so
Don't know any further use cases other than warnings and typing flags
you could also imagine setting some workspace falgs, but willing to remove one in a particular lib
can't the native stuff be controlled by flags as well?
Karl Palmskog said:
can't the native stuff be controlled by flags as well?
Not at the moment, we didn't implement the required flag parsing so rules are updated depending on the flags
So now, it is (mode ...)
that tweaks the flags, not the other direction, and would the user mess with the native flags, we would get an ugly error [something such as "coqc failed to generate the native files"] This is similar to ocaml, and what I meant it could be improved, but that's tricky in general. Hopefully for the 1.0 version of the language we could "forbid" certain flags in the flag file.
Actually native is controlled a bit more subtly, as the profile interacts too, and in 3.0, coqc -config
will automatically set it
How to best control it is tricky, once you consider packaking etc... there are quite a few too many needs which are not fully compatible
needs = I mean use cases
some people may prefer lazy generation + cache
some others may prefer always
other "never"
I guess the best is to gather all use cases and do what we can, see the issue for coq_native at https://github.com/ocaml/dune/pull/4750
Last updated: Oct 13 2024 at 01:02 UTC