Enrico Tassi (Mar 17 2023 at 13:54): Enrico Tassi (Mar 17 2023 at 13:54):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.
Ali Caglayan (Mar 17 2023 at 16:42):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.
Karl Palmskog (Mar 17 2023 at 16:45):is this an option to some tool? If so, having something like (experimental) next to option name in help is nice
Enrico Tassi (Mar 17 2023 at 16:48):it is internal, it should not even exist
Enrico Tassi (Mar 17 2023 at 16:48):this is why I was proposing a long name
Ali Caglayan (Mar 17 2023 at 17:30):I also have a PR reverting these changes https://github.com/coq/coq/pull/17380
Paolo Giarrusso (Mar 17 2023 at 19:46):@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
Paolo Giarrusso (Mar 17 2023 at 19:46):And sorry to butt in, but I've written one dune MR which was part of the motivation
Paolo Giarrusso (Mar 17 2023 at 19:47):The problem is when "foo/bar.v" exists multiple times in the workspace.
Paolo Giarrusso (Mar 17 2023 at 19:49):Your reaction suggests the code needs at least better motivation (and possibly improvements).
Paolo Giarrusso (Mar 17 2023 at 19:50):... @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...
Ali Caglayan (Mar 17 2023 at 19:51):I did not expose it, I just merged the PR.
Ali Caglayan (Mar 17 2023 at 19:52):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.
Ali Caglayan (Mar 17 2023 at 19:53):This isn't great for error messages and the fix is to just call coqc at the level of theories/
Paolo Giarrusso (Mar 17 2023 at 19:53):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
Paolo Giarrusso (Mar 17 2023 at 19:54):Sorry then
Ali Caglayan (Mar 17 2023 at 19:54):That's a different problem and I don't know whether it is even possible.
Ali Caglayan (Mar 17 2023 at 19:55):There is no analogous feature for OCaml AFAIK
Ali Caglayan (Mar 17 2023 at 19:57):But I did have a good look at it a few weeks ago, currently my focus for Dune is installed theories composition.
Enrico Tassi (Mar 17 2023 at 19:57):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
Ali Caglayan (Mar 17 2023 at 20:23):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.
Gaëtan Gilbert (Mar 17 2023 at 20:29):It's not that hacky, it's just undocumented
Paolo Giarrusso (Mar 17 2023 at 22:16):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.
Emilio Jesús Gallego Arias (Mar 19 2023 at 23:48):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.
Emilio Jesús Gallego Arias (Mar 19 2023 at 23:49):Gaëtan Gilbert said:
It's not that hacky, it's just undocumented
I think it is very hacky and should go away :)
Emilio Jesús Gallego Arias (Mar 19 2023 at 23:50):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" ?
Emilio Jesús Gallego Arias (Mar 19 2023 at 23:50):I mean, how many?
Last updated: Dec 07 2023 at 09:01 UTC