Topic: scratch files
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.
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.
Scott Morrison (Sep 16 2018 at 00:27):
I'd support adding /scratch/ to the official .gitignore. I've wanted the same thing previously.
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
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!
Kevin Buzzard (Sep 16 2018 at 08:53):
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
Scott Morrison (Sep 16 2018 at 10:48):
Last updated: May 11 2021 at 14:11 UTC