Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC