## Stream: new members

### Topic: Lean not compiling

#### Ashvni Narayanan (Jan 12 2021 at 12:52):

Neither of the files are compiling, what can I do?
Any help is appreciated, thank you!

#### Reid Barton (Jan 12 2021 at 12:58):

There's no module ring_theory.algebra in mathlib (I think there used to be), so maybe just delete that import.

#### Ashvni Narayanan (Jan 12 2021 at 13:54):

Thank you, I did that. It isn't compiling though..

#### Anne Baanen (Jan 12 2021 at 14:05):

Could you be a bit more specific? Is the orange bar on the left of the code not going away, or does lean --make number_field.lean give an error?

#### Ashvni Narayanan (Jan 12 2021 at 14:11):

I restarted VS Code, and it seems to be working alright now. Thank you!

Last updated: May 14 2021 at 00:42 UTC