scratch files in mathlib

Stream: mathlib4

[Kevin Buzzard]

I have a very minor dilemma about where to put my scratch files and I'm wondering if someone can give me a trick to solve it.

If I'm working on a fast machine and someone posts something on the Zulip or if I want to test something, I might fire up a scratch file within Mathlib. The question is where to put those scratch files. If I put them in a new directory scratch on the same level as Mathlib then they do not get set_option autoImplicit false by default and this has burned me so many times that I cannot consider hacking with this option not set to false (I am crap at coding and I need this guardrail; moreover it is sometimes the answer to the Zulip question). But if I put them in a new directory scratch within Mathlib then I can't run lake mk_all (or lake exe mk_all or whatever it is) when making a PR because it adds all the scratch files to Mathlib.lean and I have to manually remove them.

This is just such a dumb little minor niggle but I'm wondering if someone has a suggestion for a way to me achieve nirvana here.

[Rémy Degenne]

My approach to this is to create the file in whatever folder of Mathlib I am currently working, test things, then delete the file. Creating and deleting is fast enough. Do you want to keep the things you write in those files?

[Damiano Testa]

Not many people know this, but lake exe mk_all --git will work, if you do not stage/commit weird files.

[Damiano Testa]

I have gitignored globally files that start with mwe and have littered them across all dirs inside mathlib.

[Damiano Testa]

I wanted --git to be the default, but that did not go down well with review.

[Kevin Buzzard]

aah this --git option looks like exactly what I'm looking for!

@Rémy Degenne sometimes the things in these files end up being "todo"s and hang around for weeks!

[Damiano Testa]

Kevin, let me know how it works for you: I have been using it for as long as mk_all was merged, have all sorts of non-git-tracked stuff in my Mathlib dir, and never had an issue with it.