Why isn't mathlib in `src`?

Stream: maths

[Kevin Buzzard]

I thought I'd try proving Hilbert Basis theorem again with the new module stuff (although it's been impossible because my nephews have been here all weekend) and I realised that building my version of community mathlib is really annoying because my scratch files don't compile (as they were all doing things with old versions of module). This could all be fixed if mathlib lived in src like everything else does. Can we make this change at some point?

[Mario Carneiro]

what is the connection between mathlib in src and your files not compiling?

[Kevin Buzzard]

I could cd src;lean --make if mathlib weren't in root

[Kevin Buzzard]

my non-compiling scratch files have no place to hide this way

[Kevin Buzzard]

All of my other project have everything in src and a directory called scratch in root and in .gitignore

[Kenny Lau]

@Kevin Buzzard in fact that is what i had been doing on the train

[Kenny Lau]

and you can make it compile by making it the first workspace of vscode

[Scott Morrison]

I've had the same problem; I like having a scratch directory sometimes.