Zulip Chat Archive

Stream: lean4

Topic: Doom Emacs setup

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.

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

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.

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")))

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.

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.

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?

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.

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

Adam Topaz (Apr 12 2021 at 15:20):

Assuming lean3 is the default

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)

Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:25):

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

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.

Miguel Raz Guzmán Macedo (Apr 12 2021 at 15:41):

Thanks a bunch @Sebastian Ullrich , I appreciate it.

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

Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:25):

K, will try.

Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:26):

Thanks for the follow up!

Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:52):

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

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

Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:55):

will try

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.

Miguel Raz Guzmán Macedo (Apr 12 2021 at 21:58):

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

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.

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.

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

Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:23):

Oh neat.

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 ?

Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:58):

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

Miguel Raz Guzmán Macedo (Apr 12 2021 at 22:58):

Thanks a lot.

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.

Adam Topaz (Jan 06 2023 at 22:46):

It seems that the (very brief) doom emacs instructions from the lean4-mode readme no longer works. I made a pull request with a fix: https://github.com/leanprover/lean4-mode/pull/26

Andrés Goens (Mar 14 2023 at 15:15):

After updating my emacs, lean-input doesn't seem to work anymore. The last commit seems to be related, but I'm not sure, since doom emacs doesn't use package.el AFAIU. Did anyone else here have an issue with this?

Adam Topaz (Mar 14 2023 at 15:16):

Yeah I havent been using emacs with lean but when I tried I ran into the same issue.

Adam Topaz (Mar 14 2023 at 15:45):

Would the following (in config.el) work as a temporary fix?

(use-package! lean4-mode
  :hook
  (lean4-input-setup))

Adam Topaz (Mar 14 2023 at 15:47):

The answer is no :(

Adam Topaz (Mar 14 2023 at 15:49):

But surely an elisp guru would be able to immediately give us the right recipe to make such a workaround actually work.

Adam Topaz (Mar 14 2023 at 15:50):

Unfortunately, I am not that guru

Andrés Goens (Mar 14 2023 at 16:11):

Adam Topaz said:

Yeah I havent been using emacs with lean but when I tried I ran into the same issue.

it's reassuring to know that at least it's not just me :sweat_smile: maybe it's a good dabble into some elisp :thinking:

Andrés Goens (Mar 14 2023 at 16:30):

ok, so one thing that does work is manually calling M-x set-input-method and then choosing Lean there

Sebastian Ullrich (Mar 14 2023 at 16:34):

What does "doesn't seem to work anymore" mean specifically?

Adam Topaz (Mar 14 2023 at 16:34):

@Sebastian Ullrich at least for me, writing \to doesn't give me the unicode arrow, for example.

Adam Topaz (Mar 14 2023 at 16:35):

I don't know if there are other issues outside of the unicode input support

Sebastian Ullrich (Mar 14 2023 at 16:35):

But after the above command or M-x toggle-input-method (C-\) it works?

Adam Topaz (Mar 14 2023 at 16:39):

let me try

Adam Topaz (Mar 14 2023 at 16:40):

yes! that does it @Sebastian Ullrich

Adam Topaz (Mar 14 2023 at 16:43):

to be precise, I tried toggle-input-method and that made things okay again. I assume set-input-method also works as Andres mentioned, but I didn't check myself.

Sebastian Ullrich (Mar 14 2023 at 16:43):

I'm pretty sure this started after a doom update for me. And this stack trace isn't looking great... image.png

Adam Topaz (Mar 14 2023 at 22:56):

Just curious, has anyone been able to find a usable workaround for this issue?

Bulhwi Cha (Jun 06 2023 at 13:44):

I'm trying to use Doom Emacs for Lean 4 development, but I can't see type information or proof goals. I get the error that says "lean get info: (json-readtable-error 47)."

Mauricio Collares (Jun 06 2023 at 13:53):

This does sound like Lean 3 mode is being activated instead. Try setting (setq lean4-autodetect-lean3 t) (and perhaps loading lean4-mode after lean-mode) to make the two modes coexist peacefully.

Bulhwi Cha (Jun 06 2023 at 14:21):

It didn't work out. Here are some parts of my init.el, config.el, and packages.el:

init.el

config.el

packages.el:

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

Bulhwi Cha (Jun 06 2023 at 14:29):

I didn't include lean-mode in my packages.el file.

Bulhwi Cha (Jun 06 2023 at 15:18):

This issue was already reported: leanprover/lean4-mode#39.

Sebastian Ullrich (Jun 06 2023 at 15:26):

It does look like lean4-mode expects to be loaded after lean-mode. If you look at auto-mode-alist, I assume you will see the Lean 3 extension first

Bulhwi Cha (Jun 06 2023 at 16:14):

Sebastian Ullrich said:

If you look at auto-mode-alist, I assume you will see the Lean 3 extension first

Sorry, I'm not sure how to do it. But installing lean-mode and company-lean didn't solve the issue.

Sebastian Ullrich (Jun 06 2023 at 16:19):

Let me take a step back, do you actually intend to use both Lean 3 and Lean 4? If not, you should not list the lean module in your init.el or otherwise install lean-mode

Bulhwi Cha (Jun 06 2023 at 16:21):

I just want to use Lean 4. That's all.

Sebastian Ullrich (Jun 06 2023 at 16:22):

Then don't use anything lean that's not followed by 4 :)

Bulhwi Cha (Jun 06 2023 at 16:32):

Well, it's still not working:

init.el

config.el

packages.el:

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

Bulhwi Cha (Jun 06 2023 at 16:36):

It works now! Thanks for your help. :grinning:

Leni Aniva (Sep 17 2023 at 21:58):

my apologies for bumping this thread. I created a doom emacs module for Lean 4 and opened a PR in the doomemacs repo.

Joey Eremondi (Sep 27 2023 at 18:01):

@Leni Aniva Very cool! Might it be better to add it to the existing lean module with a +lean4 flag? I just wonder if changes to modules are reviewed faster than entirely new modules

Leni Aniva (Oct 03 2023 at 01:01):

Joey Eremondi said:

Leni Aniva Very cool! Might it be better to add it to the existing lean module with a +lean4 flag? I just wonder if changes to modules are reviewed faster than entirely new modules

I don't think any PRs will go through before this finishes: https://discourse.doomemacs.org/t/do-not-pr/2406. Also if lean4 is added as a flag it would make it impossible to install lean 3 and 4 side by side.

Leni Aniva (Oct 09 2023 at 06:39):

Joey Eremondi said:

Leni Aniva Very cool! Might it be better to add it to the existing lean module with a +lean4 flag? I just wonder if changes to modules are reviewed faster than entirely new modules

This would make sense if we have some sort of mechanism to allow lean 3 and 4 to coexist and automatically determine whether its 3 or 4 from reading the project structure or by reading a .dir-local.el, but I think its better to put this on hold before the doom emacs modules are separated out into their own repository.

Last updated: Dec 20 2023 at 11:08 UTC