## Stream: maths

### Topic: Why isn't mathlib in src?

#### Kevin Buzzard (Nov 04 2018 at 16:21):

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 (Nov 04 2018 at 16:41):

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

#### Kevin Buzzard (Nov 04 2018 at 16:42):

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

#### Kevin Buzzard (Nov 04 2018 at 16:42):

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

#### Kevin Buzzard (Nov 04 2018 at 16:43):

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

#### Kenny Lau (Nov 04 2018 at 18:45):

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

#### Kenny Lau (Nov 04 2018 at 18:45):

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

#### Scott Morrison (Nov 04 2018 at 21:37):

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

Last updated: May 06 2021 at 17:38 UTC