Lean not compiling

Stream: new members

[Ashvni Narayanan]

image.png

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

[Reid Barton]

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

[Ashvni Narayanan]

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

[Anne Baanen]

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]

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