First Mathlib PR

Stream: new members

[Brian Nugent]

Hello, I have recently been working on formalizing regular local rings and some results on dimension theory for local rings and I would like to PR it to Mathlib. This is my first time doing this and I read online that I should ask for write access here. My GitHub username is Brian-Nugent.

[Kevin Buzzard]

@Brian Nugent invitation sent!

[Brian Nugent]

Ok, so I cloned mathlib and added a file (EmbDim.lean) and ran "lake build" which worked fine. Now I've added my second file which uses EmbDim as a dependency and I am getting the error "no such file in directory"

[Andrew Yang]

Perhaps try running lake build again.
This seems to be the same issue as #general > Cache acting weird

[Brian Nugent]

Hmm, lake build seems to run fine with no errors

[Brian Nugent]

But I don't think it is running my added file (it would certainly have warnings)

[Brian Nugent]

Oh, I just forgot to run "lake exe mk_all" first, now it is at least giving me warnings when I run lake build

[Brian Nugent]

Ok, I think I figured it out, thanks for the reference