Stream: Coq users

Topic: Coq projects broken on Windows in the wild


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip 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)

view this post on Zulip Jakob Botsch Nielsen (Oct 22 2020 at 16:05):

Thanks for the heads up @Karl Palmskog, I will get that fixed asap


Last updated: Feb 04 2023 at 22:29 UTC