Never name a file Con.lean

Stream: mathlib4

[Yaël Dillies]

Recently, a funny story happened to me:
I was on the train bumping @Edison Xie's repo in a gitpod workspace. Then suddenly I arrived in Paris and needed to change to the Eurostar. Knowing that there would be no internet connection there, I tried switching to my local vscode on my Windows machine.

[Yaël Dillies]

I cloned the repo locally, but I got an error I had never seen before, saying that somehow the cloning had failed. Thinking it was a network error, I tried tried and retried, to no avail. Eventually I thought of looking into the part-cloned folder to see what's wrong. What I found was that everything was in order, except for a single missing file BrauerGroup/Con.lean.

[Yaël Dillies]

Easy enough, I said to myself, I can just create the file manually and copy-paste its content from github. Hence I clicked on "New file", typed Con.lean and pressed Enter. But then I got this really obscure error which again I had never seen before.

[Yaël Dillies]

Turns out that con/Con/CON/etc are forbidden filenames on Windows, with or without a file extension, as explained on this Windows help page. This is really important to know for mathlib since we have objects like docs#Con, which could naturally live in a file named Con.lean.

[Kenny Lau]

https://www.youtube.com/watch?v=bC6tngl0PTI

Why You Can't Name A File CON In Windows | Tom Scott

[Michael Rothgang]

:scream:

[Michael Rothgang]

We need a linter for this. Would anybody like to volunteer?

[Yaël Dillies]

If nothing is done, eventually a PR will add a file Mathlib.Something.Con, and suddenly all Windows users will be out of the game. Maybe this is something we can prevent using a linter?

[Michael Rothgang]

You can probably imitate the implementation of #24654; I'll be happy to review.

[Yaël Dillies]

CON isn't the only forbidden filename. The whole list provided by the above help page is CON, PRN, AUX, NUL, COM1, COM2, COM3, COM4, COM5, COM6, COM7, COM8, COM9, COM¹, COM², COM³, LPT1, LPT2, LPT3, LPT4, LPT5, LPT6, LPT7, LPT8, LPT9, LPT¹, LPT², and LPT³.

[Kyle Miller]

I'm surprised we haven't heard anyone run into "aux". That's a classic one projects would run into.

[Yaël Dillies]

Kenny Lau said:

https://www.youtube.com/watch?v=bC6tngl0PTI

Why You Can't Name A File CON In Windows | Tom Scott

For the record, I have watched that video years ago, but it never occured to me that Con.lean would be an issue. I thought(/remembered) that only applied to files without an extension.

[Yaël Dillies]

Michael Rothgang said:

You can probably imitate the implementation of #24654; I'll be happy to review.

I'll try adapting said linter in a bit. PR hopefully incoming

[Michael Rothgang]

(This also applies for any part of the module name, by the way --- as directory names are also covered by the above.)

[Michael Rothgang]

If you want, you can also check for bad characters (such as ! or quotes) in module names. Let's get this right!

[Yaël Dillies]

#27588

[Junyan Xu]

Fwiw Windows 11 supports Con.lean: https://youtu.be/Jl2Gc0eMD2s?si=hjUCPa8EYfHhW8uT&t=194

[Aaron Liu]

I will not go to windows 11

[Kenny Lau]

We should just name it Сon.lean (trust me, copy this name and it will work)

[Edison Xie]

Yaël Dillies said:

Recently, a funny story happened to me:
I was on the train bumping Edison Xie's repo in a gitpod workspace. Then suddenly I arrived in Paris and needed to change to the Eurostar. Knowing that there would be no internet connection there, I tried switching to my local vscode on my Windows machine.

We should name every file “Con” to prevent people from using Windows :)

[Edison Xie]

(And force them to use a MacBook)

[Michael Rothgang]

Let's not start an OS debate --- lest I'll have to convince you to use Linux :-)
(edit: oops, missed a negation...)

[Michael Rothgang]

I'd rather just formalise mathematics together with all of you.

[suhr]

Michael Rothgang said:

Let's start an OS debate --- lest I'll have to convince you to use Linux :-)

Your post made me realize something... I should port Lean to Haiku.

[David Ang]

You could call the file Cong.lean instead! :onion:

[Christian Merten]

Maybe lake should ship a Linux VM that replaces the host OS whenever it is not Linux.

[Henrik Böving]

Aaron Liu said:

I will not go to windows 11

You better should (or of course, to something that is not windows), microsoft will be dropping security updates for win 10 by mid October. Using win10 after that is more or less begging to eventually get into trouble.

[Ruben Van de Velde]

(deleted)

[Jon Eugster]

Kyle Miller said:

I'm surprised we haven't heard anyone run into "aux". That's a classic one projects would run into.

Side remark: I mean, I (we) did run into the AUX/ folder issue in a Lean project for a course a while ago, but we just debugged and fixed it and moved on. Since it's a Windoof-problem and not Lean related, it didn't occure to us to mention it on Zulip. I'd imagine others have been at the same place before.

[Niels Voss]

Relevant thread: #general > Build Fails Only on Ubuntu