Zulip Chat Archive

Stream: lean4

Topic: emacs


Adam Topaz (Jan 05 2021 at 15:18):

Just for future reference, here's the link to the emacs lean4 package
https://github.com/leanprover/lean4/tree/master/lean4-mode

Will this be on melpa at some point soon?

Sebastian Ullrich (Jan 05 2021 at 15:20):

Probably, when it (and the language server) is more stable

Adam Topaz (Jan 05 2021 at 16:53):

Just in case it helps anyone else, the following code in packages.el seems to work for doom emacs

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

Koundinya Vajjha (Jan 05 2021 at 17:32):

@Adam Topaz thank you!

Adam Topaz (Jan 05 2021 at 17:34):

Looks like (require 'lean4-mode) is problematic if you have both lean4-mode and lean-mode installed. And without it you have to manually activate lean4-mode with e.g. M-x. Is there a way to have it automatically activate lean4-mode in a lean4 project?

Kevin Lacker (Jan 05 2021 at 17:42):

maybe https://www.gnu.org/software/emacs/manual/html_node/emacs/Directory-Variables.html

Adam Topaz (Jan 05 2021 at 17:43):

Yeah that's a good workaround.

Simon Hudon (Jan 05 2021 at 20:41):

I just (re)installed lean4-mode (I had a version from before it was based on LSP). I have a weird situation where I'm having status: starting for a very long time

Sebastian Ullrich (Jan 05 2021 at 20:43):

Are you using the Nix setup?

Simon Hudon (Jan 05 2021 at 20:47):

To install Lean4 yes but not to install the emacs mode. Does the nix setup help also with emacs?

Sebastian Ullrich (Jan 05 2021 at 20:50):

There is preliminary integration of the Nix-based build system into editors started as above, which automatically builds dependencies when opening or invalidating a file. There is no progress report yet, and build errors from dependencies will crash the language server; see the stderr logs for the build error in that case.

Sebastian Ullrich (Jan 05 2021 at 20:51):

The language server starting for a long time can mean Nix compiling dependencies in the background, but that shouldn't happen if you pointed lean4-mode manually at the result of nix build.

Simon Hudon (Jan 05 2021 at 20:56):

Do refer to setting lean4-rootdir manually?

Sebastian Ullrich (Jan 05 2021 at 20:56):

Yes, whatever you did to set it up

Simon Hudon (Jan 05 2021 at 20:59):

Ok thanks! I'll need to get back to it a bit later. I'll let you know how it goes

Sebastian Ullrich (Jan 05 2021 at 21:04):

Btw, given my part of the talk yesterday I probably don't have to mention that I will have only limited patience dealing with manual setups not using Nix (completely) from now on :grinning_face_with_smiling_eyes:

Simon Hudon (Jan 06 2021 at 02:21):

That's understandable

Simon Hudon (Jan 06 2021 at 02:27):

For emacs, what is the nix way of doing things?

Simon Hudon (Jan 06 2021 at 02:33):

I really like what you did with the documentation btw. I especially like the button that copies code snippets. For shell code, it also copies $ however

Simon Hudon (Jan 06 2021 at 03:00):

I just saw the following line in the instructions:

nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open

Is this what you refer to as the nix emacs setup? It kind of looks like I'd need a different instance of emacs for each project. That's not very practical

Adam Topaz (Jan 08 2021 at 16:08):

@Simon Hudon did you ever get emacs to behave with nix? If so, could you give some hints on how you set it up?

Sebastian Ullrich (Jan 08 2021 at 16:19):

Simon Hudon said:

It kind of looks like I'd need a different instance of emacs for each project. That's not very practical

FWIW, I use a separate instance per workspace, so that's not really an issue for me. But if you don't want that, the nix-env-selector solution mentioned in the "using nix" topic sounds like the next-best thing.

Simon Hudon (Jan 08 2021 at 16:28):

@Sebastian Ullrich I see. I kind of use emacs as an operating system where I do a whole bunch of stuff until I'm forced to interact with OSX again

Simon Hudon (Jan 08 2021 at 16:29):

@Adam Topaz Sorry I haven't made progress yet. I'm going to try again tonight

Adam Topaz (Jan 08 2021 at 16:30):

nix-env-selector is a vs-code thing right?

Sebastian Ullrich (Jan 08 2021 at 16:33):

Whoops, yeah. I use direnv in Emacs (for things that are not Lean), though that needs one more setup step per project...

Adam Topaz (Jan 08 2021 at 16:36):

Isn't there a way to make this nix build .#lean-dev -o ./lean-dev step happen automatically when opening the nix-shell using a shell.nix file? I think it's also possible to ask nix-shell to set up a link + update the path variable so that lean is symlinked to ./lean-dev. I guess what I'm going for is to have it automatically set up the links + path stuff when I run nix-shell so that emacs is happy when I run emacs from within the nix-shell.

Adam Topaz (Jan 08 2021 at 16:37):

I'll take a look at direnv. Thanks!

Sebastian Ullrich (Jan 08 2021 at 16:37):

If you're running Emacs from within a nix-shell anyway, why not use .#emacs-dev?

Adam Topaz (Jan 08 2021 at 16:37):

Does this not create a whole new installation of emacs?

Sebastian Ullrich (Jan 08 2021 at 16:39):

Yes, it does download "a bit" of stuff. But it will use your .emacs.d.

Adam Topaz (Jan 08 2021 at 16:40):

Oh ok.

Adam Topaz (Jan 08 2021 at 16:43):

"a bit" ~= 1G

Reid Barton (Jan 08 2021 at 16:45):

If you wish to build a Lean program from scratch, you must first invent the universe. -- Carl Sagan

Sebastian Ullrich (Jan 08 2021 at 16:46):

Adam Topaz said:

Isn't there a way to make this nix build .#lean-dev -o ./lean-dev step happen automatically when opening the nix-shell using a shell.nix file?

If you use nix shell .#lean-dev instead, it will put the correct lean binary in your path, which should be sufficient if you've already installed lean4-mode another way.

Adam Topaz (Jan 08 2021 at 16:49):

Hmm... what's the actual command?

Adam Topaz (Jan 08 2021 at 16:49):

I've been using nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix to start the nix shell with the custom nix

Adam Topaz (Jan 08 2021 at 16:54):

Ah I see. You mean run nix shell .#lean-dev in the nix-shell.

Adam Topaz (Jan 08 2021 at 16:54):

Yes, this works

Yury G. Kudryashov (Jul 15 2022 at 16:01):

Is there an example of emacs setup that works both for lean3 and lean4? @Sebastian Ullrich

Yury G. Kudryashov (Jul 15 2022 at 16:01):

BTW, why not put lean4-mode to melpa?

Sebastian Ullrich (Jul 15 2022 at 16:03):

https://github.com/melpa/melpa/pull/8106

Sebastian Ullrich (Jul 15 2022 at 16:03):

Yury G. Kudryashov said:

Is there an example of emacs setup that works both for lean3 and lean4? Sebastian Ullrich

Sorry, I don't use Lean 3 anymore

Yury G. Kudryashov (Jul 15 2022 at 16:11):

I guess, I'll have to use different editors for Lean 3 and Lean 4 (or different instances of emacs).

Tomas Skrivan (Jul 15 2022 at 16:22):

At some point I had both working. I have lean-mode installed through melpa and lean4-mode with straight. The only annoying thing is that for every lean3 file I have to manually switch to lean-mode.

If I remember correctly, I set elan default toolchain to lean3 as all my lean4 code live in lake projects and there Lean version is determined by toolchain file.

Mauricio Collares (Jul 16 2022 at 21:16):

Requiring lean-mode and lean4-mode and doing (setq lean4-autodetect-lean3 t) works for me (or at least worked at some point).

Yury G. Kudryashov (Jul 16 2022 at 22:53):

I'll try later tonight.

Sebastian Ullrich (Dec 09 2022 at 15:34):

After many years of divergence and manual sync, lean4-mode now uses the same abbreviations.json as vscode-lean4: https://github.com/leanprover/lean4-mode/pull/23

Yury G. Kudryashov (Jan 27 2023 at 05:19):

When I add text to a line with multibyte unicode characters (e.g., theorem principal_le_nhdsSet : 𝓟 s ≤ 𝓝ˢ s := fun _s hs =>), Lean server assumes that I added these symbols at a wrong place (probably, at the position "number of symbols before the added char" bytes from the start of the line). Is it a bug in lean4-mode or lsp? How can I debug it?

Yury G. Kudryashov (Jan 27 2023 at 05:20):

Let me update lean4-mode first...

Yury G. Kudryashov (Jan 27 2023 at 05:25):

Still happens with the latest git version. Also, wrong chars are highlighted in case of an error in this line.

Mario Carneiro (Jan 27 2023 at 05:35):

this bug has come up several times, it most likely has to do with characters of more than one UTF-16 code unit (i.e. the codepoint is more than 0xFFFF)

Mario Carneiro (Jan 27 2023 at 05:36):

to test, see whether the diagnostics are misaligned when you use low unicode characters like ⟨⟩, or whether you have to use high unicode like 𝓟

Mario Carneiro (Jan 27 2023 at 05:39):

the bug is caused in part by LSP, which counts characters in UTF-16 (even though most likely neither the server nor the client in your situation speak UTF-16 natively)

Mario Carneiro (Jan 27 2023 at 05:40):

AFAIK this bug does not show up on vscode so I think lean4 is properly counting UTF-16 characters, so they are probably not being counted correctly on the emacs side

Sebastian Ullrich (Jan 27 2023 at 08:27):

https://github.com/emacs-lsp/lsp-mode/issues/2080

David Thrane Christiansen (Jan 27 2023 at 08:33):

LSP is a bit of a mess - it mandates UTF-8 for protocol messages, and until v3.17 it mandated UTF-16 for buffer offsets and positions. Many actual implementations of LSP ignore this, because it's burdensome to re-encode things just to find offsets. This leads to this kind of problem.

But version 3.17 of LSP enables file encoding negotiation, which makes this much easier to solve - I think support for that protocol feature is lacking mostly because few servers yet implement it.

Reid Barton (May 23 2023 at 13:17):

Is there any fix for this issue with the positions being wrong for non-BMP unicode characters in emacs?

Sebastian Ullrich (May 23 2023 at 15:21):

We could implement utf-32 support in the server, though it would be quite a bit of code churn merely to work around an lsp-mode bug to be honest

Reid Barton (May 23 2023 at 16:30):

It's really a VSCode bug

Reid Barton (May 23 2023 at 16:32):

It makes emacs pretty much unusable for category theory unfortunately

Sebastian Ullrich (May 23 2023 at 16:37):

Reid Barton said:

It's really a VSCode bug

What do you mean? lsp-mode is pretending that utf-16 offsets are utf-32 offsets

Reid Barton (May 23 2023 at 17:05):

But there was no sensible reason to have utf-16 offsets in the first place

Reid Barton (May 23 2023 at 17:08):

Is it possible to tell lsp-mode to send the whole file on every change? Or the whole changed line?

Yury G. Kudryashov (Jun 06 2023 at 22:20):

Abbreviations like \ennreal don't work for me in Emacs + Lean 4 mode: it interprets ℝ≥0∞ as a list of possible outputs instead of a single output.

Bulhwi Cha (Jun 07 2023 at 01:51):

This works fine for me:

import Mathlib.Data.Real.ENNReal
open ENNReal

#check 0

Yury G. Kudryashov (Jun 07 2023 at 14:25):

Possibly, my lean4-mode interferes with my lean-mode.

Yury G. Kudryashov (Jul 13 2023 at 03:45):

While trying to make lean4-mode melpa-ready, I found a bug: lean4-mk-check-menu-option calls non-existent lean4-set-check-mode. Choosing these menu entries result in error. Am I right that these modes no longer exist, so I should just drop these options?

Yury G. Kudryashov (Jul 13 2023 at 03:45):

@Leonardo de Moura :up:

Yury G. Kudryashov (Jul 13 2023 at 03:45):

@Bulhwi Cha Did you type this in Emacs using \ennreal abbreviation?

Yury G. Kudryashov (Jul 13 2023 at 04:05):

BTW, what's the status of helm-lean, yasnippet-lean, and company-lean for Lean 4? No longer needed? Not ported yet? Merged into other source files?

Yury G. Kudryashov (Jul 13 2023 at 07:31):

It seems that Emacs reads ("ennreal" "ℝ≥0∞") from JSON file, then quail-defrule splits the second string into a list of characters.

Yury G. Kudryashov (Jul 13 2023 at 07:33):

We should replace each value s in this hash map with (vector s).

Yury G. Kudryashov (Jul 13 2023 at 07:34):

I'll open a PR in the morning.

Yury G. Kudryashov (Jul 13 2023 at 07:35):

BTW, we are getting rid of lines with $CURSOR twice: in the github workflow and in Lisp.

Bulhwi Cha (Jul 13 2023 at 08:22):

Yury G. Kudryashov said:

Bulhwi Cha Did you type this in Emacs using \ennreal abbreviation?

I think I copy-pasted it. Now I have to type \R\ge0\infty.

Yury G. Kudryashov (Jul 13 2023 at 13:09):

leanprover/lean4-mode#41 fixes this

Yury G. Kudryashov (Jul 13 2023 at 19:15):

In lean4-info-buffer-redisplay, what does the first when test do?

Yury G. Kudryashov (Jul 13 2023 at 19:59):

We have a few remaining non-docstring melpazoid warnings:

lean4-info.el with byte-compile using Emacs 28.1:

lean4-info.el:273:1: Warning: variable `_' not left unused
lean4-info.el:273:1: Warning: variable `_' not left unused

lean4-mode.el with package-lint 20230605.1550:

2 issues found:
251:1: warning: `with-eval-after-load' is for use in configurations, and should rarely be used in packages.

lean4-mode.el with melpazoid:

- lean4-mode.el#L280: Loading a package should rarely add hooks

Stderr output while compiling/loading:

Loading quail/latin-ltx...

Any ideas how do we fix them?


Last updated: Dec 20 2023 at 11:08 UTC