Karl Palmskog (Oct 18 2020 at 20:14): Karl Palmskog (Oct 18 2020 at 20:14):as has been discussed earlier, having a file named Aux.v breaks a Coq project on Windows, for annoying historic reasons. However, more interesting is perhaps how common this is in the wild, and it turns out to be somewhat common: https://github.com/search?l=&q=filename%3AAux.v+language%3ACoq&type=code
Karl Palmskog (Oct 18 2020 at 20:15):in particular, I would suggest we change Aux.v to another name here https://github.com/coq-contribs/sum-of-two-square/blob/v8.9/Aux.v
Michael Soegtrop (Oct 22 2020 at 15:26):Interesting finding - 28 pages of results ...
Maybe we should introduce a warning in coqc for non portable file names. On Windows there are quite a few more (NUL, PRN, COM1..COM4). What I find more annoying is that people give file names to example files which are invalid module names, so that one can't open them in CoqIDE.
Karl Palmskog (Oct 22 2020 at 15:58):note though that only the first 2-3 pages in the search have names that actually cause trouble, the rest are variations on Aux like NumAux.v, which is fine on Windows
Karl Palmskog (Oct 22 2020 at 15:59):I completely agree that there should be some warning with file names that are invalid/broken. We are maybe a bit unique in being a PL community that has few Windows users overall, so the Aux thing needs to be flagged up
Karl Palmskog (Oct 22 2020 at 16:02):ah, and I should ping @Danil Annenkov and @Jakob Botsch Nielsen that ConCert has this problem (Aux.v file causes broken Windows builds)
Pierre-Marie Pédrot (Oct 22 2020 at 16:03):Forbidding file names with less than 3 letters seems like an efficient solution, both for Windows compatibility and human readability :scissors:
Karl Palmskog (Oct 22 2020 at 16:04):unfortunately I think this would break a large part of Coq's CI (even though I agree in principle)
Jakob Botsch Nielsen (Oct 22 2020 at 16:05):Thanks for the heads up @Karl Palmskog, I will get that fixed asap
Last updated: Apr 19 2024 at 13:02 UTC