search

leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
57 stars 26 forks source link

json-readtable-error 47 #39

Open Pi-Cla opened 1 year ago

Pi-Cla commented 1 year ago

I have installed Lean4 via elan and have set lean-rootdir to home/cla/.elan and then home/cla/.elan/ and both times when I try to use lean-toggle-show-goal with the default Main.lean file generated by lake init foo, it gives me the error: lean get info: (json-readtable-error 47)

urkud commented 1 year ago

Do you have Lean 3 mode installed?

kisonecat commented 11 months ago

I also saw this error when I had lean-mode installed; replacing it with lean4-mode fixed this for me.

collares commented 10 months ago

You can have both packages, but the command to see goals in lean4-mode is lean4-toggle-info (bound to C-c TAB). The command you cited is from the lean-mode package (i.e., Lean 3).

quinn-dougherty commented 4 months ago

Notice: you also need to not have lean-company installed to avoid this error.

mekeor commented 2 days ago

You can have both packages, but the command to see goals in lean4-mode is lean4-toggle-info (bound to C-c TAB). The command you cited is from the lean-mode package (i.e., Lean 3).

I agree. lean4-mode does not define a command named lean-toggle-show-goal. The issue-report is just invalid and can be closed, in my opinion.

mekeor commented 2 days ago

Notice: you also need to not have lean-company installed to avoid this error.

That'd be because lean-company depends on lean-mode. Only then, the command lean-toggle-show-goal becomes available.

quinn-dougherty commented 1 day ago

I fixed this by thoroughly purging (with doom purge), since I had previously installed lean-mode and naively removing it didn't purge it thoroughly enough. So I'd expect people to keep running into it if they mistakenly install lean-mode before they realize they need lean4-mode.