I've just discovered this beauty. Can we at least clearly mark the code which is a hack? I mean something like -override-source-file-name-in-messages would have been clearer to me (assuming I understood what it is for, that is work around a hack in the implementation of dune).
It is an internal flag no one needs to type.
That was @Gaëtan Gilbert's work around for compiler messages looking nice when running our Dune rules. @Emilio Jesús Gallego Arias wanted to just fix the rules, but he didn't have the time to get around to it yet and I merged the PR in the mean time which I am slightly regretting.
is this an option to some tool? If so, having something like (experimental)
next to option name in help is nice
it is internal, it should not even exist
this is why I was proposing a long name
I also have a PR reverting these changes https://github.com/coq/coq/pull/17380
@Enrico Tassi I think the alternative fix today is to rewrite the file name in dune, which isn't exciting either. "The path relative to the folder where coqc was invoked" isn't a robust concept
And sorry to butt in, but I've written one dune MR which was part of the motivation
The problem is when "foo/bar.v" exists multiple times in the workspace.
Your reaction suggests the code needs at least better motivation (and possibly improvements).
... @Ali Caglayan wait, were you exposing this just to tools/dune_rule_gen/coq_rules.ml
? I'm thinking of exposing it to dune instead...
I did not expose it, I just merged the PR.
Our dune rules in the Coq repo are different to the coq.theory ones. The cqoc in coq.theory is called at the directory of the theory and coqc in Coq's custom dune rules are called at the level of the file.
This isn't great for error messages and the fix is to just call coqc at the level of theories/
I was thinking about https://github.com/ocaml/dune/pull/6006, but I've now closed it because calling coqc in the project isn't a complete fix
Sorry then
That's a different problem and I don't know whether it is even possible.
There is no analogous feature for OCaml AFAIK
But I did have a good look at it a few weeks ago, currently my focus for Dune is installed theories composition.
The number of quirks to make dune "work" is suggesting we went the wrong path, or the right path but way too early.
Said that I'm fine having hacks, but I prefer them to be very explicit/documented. Ideally all coming with an issue to track their removal, eventually
This isn't a quirk to make Dune work. Dune was working fine before this patch was merged. What is at issue are the custom Dune rules that were written for the Coq repo, they are calling coqc in the wrong place. This bug was documented for a while but there was no progress on it. It caused error messages when developing the stadard library to just show the file name. Gaetan had a PR that added this hack and I accepted and merged it against Emilio's advice because I was tired of hearing complaints about the dune setup tbh. I did this knowing that the fix would not come today, but a temporary hack would be good enough until it does come.
Honestly I really regret doing this now. Emilio isn't happy that I merged this hack against his advice and further more people are asking about it which wasn't supposed to happen.
It's not that hacky, it's just undocumented
as an outside observer, Enrico's compromise seems reasonable: dropping this would hinder Coq devs (a net negative), the "technical debt" seems to have limited costs, and the "proper fix" isn't urgent. And arguably, the hack is having to run coqc in the right folder just to get useful errors.
Ali Caglayan said:
Honestly I really regret doing this now. Emilio isn't happy that I merged this hack against his advice and further more people are asking about it which wasn't supposed to happen.
I think it is not a big deal that the PR was indeed merged, it is just that I didn't see the pain of the wrong location so bad as to be so urgent, and indeed I was fearing there would be some discussion like this taking more time than the fix.
The fix is pretty simple (and I will eventually get to it , but please feel free to get ahead of me). Instead of calling coqc
in the current dir, just cd
to the right dir. The code already supports that as can relocate arguments.
We decided to merge the rules with this bug because indeed at some point there is just so much you can take at once.
Gaëtan Gilbert said:
It's not that hacky, it's just undocumented
I think it is very hacky and should go away :)
Enrico Tassi said:
The number of quirks to make dune "work" is suggesting we went the wrong path, or the right path but way too early.
Said that I'm fine having hacks, but I prefer them to be very explicit/documented. Ideally all coming with an issue to track their removal, eventually
What is the number quirks we have to make dune "work" ?
I mean, how many?
Last updated: Jun 04 2023 at 19:30 UTC