scratch files

Stream: general

[Kevin Buzzard]

I'd like to have a few scratch files in my clone of community-mathlib, in e.g. a scratch/ directory. Should I do this with some local trickery in .gitignore, should I change the github version of .gitignore, should I just use _target, should I load a second project in VS Code? I want VS Code to stop nagging me about files I just use to do tests or calculations.

[Bryan Gin-ge Chen]

Putting stuff in _target/scratch/ seems safe enough, at least it doesn't seem to be overwritten when doing leanpkg upgrade / build.

[Scott Morrison]

I'd support adding /scratch/ to the official .gitignore. I've wanted the same thing previously.

[Mario Carneiro]

I have a test.lean file at the root of my repository, that I have added to my local gitignore (.git/info/exclude). I suggest doing this for whatever your local scratch setup is

[Kevin Buzzard]

Aah this is probably the canonical solution. The idea is that .gitignore is for files and directories which should be ignored by all users of the repo, like .olean files, but .git/info/exclude is a local .gitignore for your clone only and you won't be faced with VS Code nagging you that you've updated .gitignore if you edit this. Thanks for this tip Mario!

[Kevin Buzzard]

Gaargh leanpkg build builds my scratch files that don't build and then reports errors. Could this be fixed by moving all of mathlib into a src/ directory?

[Scott Morrison]

Yes. :-)