Zulip Chat Archive

Stream: general

Topic: scratch files


view this post on Zulip Kevin Buzzard (Sep 15 2018 at 14:59):

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.

view this post on Zulip Bryan Gin-ge Chen (Sep 15 2018 at 15:05):

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

view this post on Zulip Scott Morrison (Sep 16 2018 at 00:27):

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

view this post on Zulip Mario Carneiro (Sep 16 2018 at 04:42):

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

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:21):

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!

view this post on Zulip Kevin Buzzard (Sep 16 2018 at 08:53):

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?

view this post on Zulip Scott Morrison (Sep 16 2018 at 10:48):

Yes. :-)


Last updated: May 11 2021 at 14:11 UTC