emacs json-readtable-error

Stream: general

[Quinn]

the emacs-mode repo says its for lean 3, idk if that means its deprecated on lean4. I can't use it at all because:

lean scroll hook: (json-readtable-error 47) [2 times]
lean get info: (json-readtable-error 47)

[Quinn]

I use doom, but i'm not using the doom :lang lean module right now i'm using package! lean-mode from melpa. neither of them work.

[Richard Copley]

Use lean4-mode instead.

[Tomas Skrivan]

Nice, I see some activity on the official repo. Is the official lean4-mode usable again? I'm on Paul's fork right now, should I switch back to the official?

[Richard Copley]

Tomas Skrivan said:

Nice, I see some activity on the official repo. Is the official lean4-mode usable again? I'm on Paul's fork right now, should I switch back to the official?

Each has its advantages and disadvantages. Nothing major has changed yet on the main line, so if you had a particular reason to switch, it is likely that it still holds.

[Yury G. Kudryashov]

The main issue with the main repo is that I'm the maintainer and (a) my emacs programming skills aren't great; (b) I recently started working for a startup and I don't have much time. What are the nice features of the fork? We can try to merge them back.