lean-mode docs/confusion

Stream: lean4

[Andrew Kent]

It seems like the README for Lean 3's lean-mode has been updated to specify Lean 3, but the MELPA lean-mode package doesn't reflect that yet. Is that just something that will update automatically given some time? Or does it need a nudge?

(I was just helping someone get Lean 4 working on their machine and they had stumbled on this without realizing it was just for Lean 3.)

[Sebastian Ullrich]

I just updated some commentary in lean-mode.el, which might or might not be reflected in melpa after the next refresh :)

[Joe Kiniry]

:wave: That was me. I figured it all out of course, but it took a bit of digging. I'm good to go now though, despite bravely using it all outside of my nix environment. :laughing:

[Sebastian Ullrich]

Joe Kiniry said:

despite bravely using it all outside of my nix environment. :laughing:

I'm working on that :laughing:

[Sebastian Ullrich]

The melpa page seems to have properly updated now