Stream: Dune devs & users

Topic: Dune now passes -color to coqc


view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:39):

I've made a patch to pass -color on to coqc when Dune detects it can enable color outputs itself. This should lead to prettier error messages for users. I would appreciate if people tried it out: https://github.com/ocaml/dune/pull/7052

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 21:43):

if I run dune build in a color capable terminal, then again in a color incapable terminal, does it detect that the coqc command changed and rebuild?

view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:51):

That's a good point...

view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:52):

I believe it would rebuild.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:52):

The color options are passed to ocamlc using an env var. Do we have something similar for coqc?

view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:52):

Btw, this would not affect the core coq as we generate our own rules there.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 21:56):

I see we have COQ_COLOR, but that is probably not what we are after right?

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 22:03):

also does auto colors not work when called through dune?

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:06):

I originally tried that, but it didn't work in my terminal.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:07):

Color detection in other binaries is also off by default, since I guess Dune is piping outputs.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:07):

If we had an enviornment var like OCAML_COLOR that would be the ideal solution.

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 22:21):

Ali Caglayan said:

I see we have COQ_COLOR, but that is probably not what we are after right?

I see COQ_COLORS (plural) but not COQ_COLOR
we could add COQ_COLOR

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 22:22):

OTOH using env vars to get around dune feels like a hack
maybe dune should have a system to understand flags that don't affect the actual targets?

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:23):

If you set CLI_COLOR you can turn off Dune's auto color detection, which should help people in the situation of switching between a color and non-color terminal.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:24):

For most people, Dune will be called inside a color terminal and there won't be a switch of enviornment.

view this post on Zulip Ali Caglayan (Feb 12 2023 at 22:28):

I'll see what the other devs think about the situation.

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:35):

CI need not be a color terminal... But I'd say we do need smarter caching for other reasons

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:38):

https://github.com/ocaml/dune/issues/6005 / https://github.com/ocaml/dune/pull/6006 is the example I have in mind

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 00:40):

@Gaëtan Gilbert I'd expect auto-colors can't work in dune because dune always buffers the output (like make -O) to avoid mixing outputs from multiple commands in concurrent builds

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:06):

Paolo Giarrusso said:

https://github.com/ocaml/dune/issues/6005 / https://github.com/ocaml/dune/pull/6006 is the example I have in mind

This is on my radar, but I still don't know a good way of fixing those error messages for users other than parsing and fixing.

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:07):

In anycase after discussing with some of the Dune devs, I don't think we will ever have a way of ignoring command line arguments in Dune. I don't think the environment variable solution is too hacky, so I would like for Coq to implement CLI_COLOR eventually.

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:07):

For now, passing the argument is unlikely to affect many users.

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:12):

I agree environment variables are reasonable, especially if dune can commit to not tracking them.

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:13):

Re "many users": wouldn't this affect IDEs when they switch to dune coq top?

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:16):

Yes, this is true. Perhaps some more thinking is needed on this feature.

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:17):

Currently there are good workarounds too like setting -color from env.

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:17):

Ah by wrapping coqc you mean like this?

https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/dune#L4
https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tools/coqc_timing.sh

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:18):

I've have to do this quite a bit, indeed

view this post on Zulip Paolo Giarrusso (Feb 13 2023 at 01:19):

@Ali Caglayan also, I didn't link the !6006 MR because of the error-message problem, but because caching is too strict for it to work

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:21):

I don't mean overriding the coqc binary, but you can do (env (_ (coq (flags -color on)))).

view this post on Zulip Ali Caglayan (Feb 13 2023 at 01:22):

btw Dune uses some path rewriting hackery to get ocamlc builds to be relocatable. However this screws with other tools such as ocamldebug.


Last updated: May 25 2024 at 20:01 UTC