Stream: Dune devs & users

Topic: Dune builds affected by coqrc


view this post on Zulip Paolo Giarrusso (Oct 24 2021 at 07:54):

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?

[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)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 13:26):

@Paolo Giarrusso is this still the case in Dune 2.9 ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 13:27):

We added -q to the default set of flags some time ago, maybe you are overriding them in your own (flags ...) declaration

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 13:27):

Remember that you need to pass :standard if you want default flags to be preserved

view this post on Zulip Paolo Giarrusso (Oct 24 2021 at 13:56):

I wasn't aware of :standard.

view this post on Zulip Paolo Giarrusso (Oct 24 2021 at 14:47):

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 :-|.

view this post on Zulip Paolo Giarrusso (Oct 24 2021 at 14:54):

okay, :standard seems exactly -q, thanks! (all on dune 2.9.0).

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:34):

Indeed the docs need a lot of improvement, [even the deployed version is not 2.9]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:35):

Added to document that :standard is -q to my TODO

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:35):

Yeah this confusion with missing :standard is a bit common both in OCaml and Coq

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:36):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:36):

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

view this post on Zulip Karl Palmskog (Oct 24 2021 at 18:44):

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)

view this post on Zulip Gaëtan Gilbert (Oct 24 2021 at 18:49):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:52):

Maybe, but that's a bit ugly, and makes things such as :standard \ foo a bit more difficult

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:53):

but indeed it has been a problem in some cases

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:53):

I guess dune devs are leaning to emitting a warning when you override flags and don't include :standard

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:53):

such a warning exists now for the stubs

view this post on Zulip Gaëtan Gilbert (Oct 24 2021 at 18:53):

I forgot about \

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:54):

yeah, the thing is that it is a "set of flags"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:54):

many things can be improved about flags IMVHO

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:54):

and Dune devs know about it, but it is hard to get manpower

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:54):

as people do care more about speed, caching, IDEs, and features

view this post on Zulip Gaëtan Gilbert (Oct 24 2021 at 18:55):

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

view this post on Zulip Karl Palmskog (Oct 24 2021 at 18:55):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:55):

@Karl Palmskog sorry I missed your message

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:55):

indeed, I think that's the right setup

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:55):

:standard includes things both inherited and set in the profile

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:56):

see the tests here https://github.com/ocaml/dune/blob/main/test/blackbox-tests/test-cases/coq/env.t

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 18:58):

But yeah it is so easy to forget :standard that this is an usability issue :S

view this post on Zulip Karl Palmskog (Oct 24 2021 at 18:58):

and :standard should go before any custom flags in dune file? I think the order matters, right?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:04):

:standard is just expanded to the set of flags that are computed from the workspace and env flags settings

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:04):

the language dune supports is an "ordered set language"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:04):

indeed the order will be one sent to coqc

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:05):

https://dune.readthedocs.io/en/latest/concepts.html#ordered-set-language

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:05):

So you can place :standard where you would like it to be

view this post on Zulip Karl Palmskog (Oct 24 2021 at 19:05):

well, I think we are trying to determine where "most people would like it to be, most of the time"

view this post on Zulip Karl Palmskog (Oct 24 2021 at 19:06):

for example, if I have a Coq library, does :standard <custom flags> give my clients the most flexibility?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:06):

I guess o

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:06):

I guess so

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:07):

Don't know any further use cases other than warnings and typing flags

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:08):

you could also imagine setting some workspace falgs, but willing to remove one in a particular lib

view this post on Zulip Karl Palmskog (Oct 24 2021 at 19:08):

can't the native stuff be controlled by flags as well?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:15):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:16):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:16):

needs = I mean use cases

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:17):

some people may prefer lazy generation + cache

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:17):

some others may prefer always

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:17):

other "never"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 24 2021 at 19:17):

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: Feb 04 2023 at 02:03 UTC