Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:41):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:42):

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

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:42):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:45):

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

view this post on Zulip Kenny Lau (Nov 04 2018 at 18:45):

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

view this post on Zulip 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