Zulip Chat Archive

Stream: lean4

Topic: Doom Emacs setup


view this post on Zulip Miguel Raz Guzmán Macedo (Feb 01 2021 at 01:23):

Has anyone setup their Lean4 with Doom Emacs?
I would highly appreciate a guide to setting it up.

view this post on Zulip Adam Topaz (Feb 01 2021 at 01:54):

I haven't had time to play with lean4 in a few weeks, so things may (and probably have) changed. In any case, this worked for me

(package! dash)
(package! flycheck)
(package! dash-functional)
(package! f)
(package! s)
(package! lsp-mode)

(package! lean4-mode :recipe
  (:host github
   :repo "leanprover/lean4"
   :files ("lean4-mode/*.el")))

located in packages.el

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 14:30):

Thanks a lot for the tip @Adam Topaz - though I can't seem to get the "proof goals" window to pop up.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 14:56):

Concretely, when placing my cursor on the intro h line here

theorem ex1 : p  q  q  p := by
  intro h
  cases h with
  | inl h1 =>
    apply Or.inr
    exact h1
  | inr h2 =>
    apply Or.inl
    assumption

I get the following error to show up in my breadcrumb bar:

Error in post-command-hook (lean4-info-buffer-redisplay):
(wrong-type-argument listp #s(hash-table size 4 test equal rehash-size 1.5 rehash-threshold 0.8125 data
("source" "Lean 4 server" "severity" 3 "range" #s(hash-table size 2 test equal rehash-size 1.5 rehash-threshold 0.8125 data
("start" #s(hash-table size 2 test equal rehash-size 1.5 rehash-threshold 0.8125 data ("line" 0 "character" 0))
 "end" #s(hash-table size 2 test equal rehash-size 1.5 rehash-threshold 0.8125 data ("line" 0 "character" 6))))
 "message" "id : ?m.2 → ?m.2")))

view this post on Zulip Adam Topaz (Apr 12 2021 at 14:56):

Sorry, it has now been even longer since I played with lean4, so I can't help with this. BTW as @Sebastian Ullrich mentioned, the last line of the above code might be sufficient.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:16):

Oh, I just saw you were redirecting me here @Sebastian Ullrich , thanks a lot :sweat_smile: .
I think If I can get the goals to show, I will be a very happy camper and most of my needs will be met for now.

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:17):

Last time I tried, the "next error" buffer was working with C-c C-n, as usual. Does lean4+emacs have a goal window now?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:18):

My goal window opens up, but doesn't show anything and I get the error I posted above.

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:20):

Do you have both lean3-mode and lean4-mode installed? If so I think you need to manually activate lean4-mode

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:20):

Assuming lean3 is the default

view this post on Zulip Adam Topaz (Apr 12 2021 at 15:21):

(And again, I'm probably completely wrong since I've been out of the lean4 loop for a while)

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:25):

yes, I think I deactivated lean3 - lemme double check.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 15:32):

This might be a version issue with lsp-mode, they changed data structures at some point. I can take a closer look later.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:41):

Thanks a bunch @Sebastian Ullrich , I appreciate it.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 21:11):

I've upgraded to the latest Doom Emacs

  New revision: ce65645fb8 (2 weeks ago)
...
     (91/172) lsp-mode updated (db385a4 -> eda51c2)

and it seems to still work

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:25):

K, will try.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:26):

Thanks for the follow up!

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:52):

How should lean4 be install for Doom Emacs to pick it up?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:55):

Oh, right, at the end of https://leanprover.github.io/lean4/doc/make/index.html

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:55):

will try

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 21:56):

It also works with emacs-dev, which is how I use it. It will just ignore the lean4-mode coming with that, so you need the package! decl instead.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:58):

Not gonna lie, but I struggle a lot with the nix setup.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:59):

(I'm assuming you are referencing the emacs-dev as an extension of the nix-shell. For some reason it doesn't play nice with my fish shell and that complicates it a bit.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:01):

OK I just saw your tweet about the course with Nix + CI combo and that does sound neat.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 22:14):

Note that we don't actually advertise using Nix for the course :) https://github.com/IPDSnelting/tba-2021#tba-2021

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:23):

Oh neat.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:23):

So does this mean that I have to download a new nix build for every project that I want to use Lean4 in ?

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:58):

@Sebastian Ullrich Emacs works with the nix build now! :tada:

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:58):

Thanks a lot.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 23:01):

I setup Lean3 with the mathlib stuff and Lean4 with emacs so I guess this works for me well enough.


Last updated: May 07 2021 at 13:21 UTC