Zulip Chat Archive

Stream: new members

Topic: Lean not compiling


view this post on Zulip Ashvni Narayanan (Jan 12 2021 at 12:52):

image.png

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

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

view this post on Zulip Ashvni Narayanan (Jan 12 2021 at 13:54):

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

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

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