Ali Caglayan (Feb 12 2023 at 21:39): 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
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?
Ali Caglayan (Feb 12 2023 at 21:51):That's a good point...
Ali Caglayan (Feb 12 2023 at 21:52):I believe it would rebuild.
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?
Ali Caglayan (Feb 12 2023 at 21:52):Btw, this would not affect the core coq as we generate our own rules there.
Ali Caglayan (Feb 12 2023 at 21:56):I see we have COQ_COLOR, but that is probably not what we are after right?
Gaëtan Gilbert (Feb 12 2023 at 22:03):also does auto colors not work when called through dune?
Ali Caglayan (Feb 12 2023 at 22:06):I originally tried that, but it didn't work in my terminal.
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.
Ali Caglayan (Feb 12 2023 at 22:07):If we had an enviornment var like OCAML_COLOR that would be the ideal solution.
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
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?
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.
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.
Ali Caglayan (Feb 12 2023 at 22:28):I'll see what the other devs think about the situation.
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
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
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
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.
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.
Ali Caglayan (Feb 13 2023 at 01:07):For now, passing the argument is unlikely to affect many users.
Paolo Giarrusso (Feb 13 2023 at 01:12):I agree environment variables are reasonable, especially if dune can commit to not tracking them.
Paolo Giarrusso (Feb 13 2023 at 01:13):Re "many users": wouldn't this affect IDEs when they switch to dune coq top?
Ali Caglayan (Feb 13 2023 at 01:16):Yes, this is true. Perhaps some more thinking is needed on this feature.
Ali Caglayan (Feb 13 2023 at 01:17):Currently there are good workarounds too like setting -color from env.
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
Paolo Giarrusso (Feb 13 2023 at 01:18):I've have to do this quite a bit, indeed
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
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)))).
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: Jun 04 2023 at 23:30 UTC