emacs

Stream: lean4

[Adam Topaz]

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]

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

[Adam Topaz]

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]

@Adam Topaz thank you!

[Adam Topaz]

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]

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

[Adam Topaz]

Yeah that's a good workaround.

[Simon Hudon]

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]

Are you using the Nix setup?

[Simon Hudon]

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

[Sebastian Ullrich]

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]

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]

Do refer to setting lean4-rootdir manually?

[Sebastian Ullrich]

Yes, whatever you did to set it up

[Simon Hudon]

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

[Sebastian Ullrich]

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]

That's understandable

[Simon Hudon]

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

[Simon Hudon]

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]

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]

@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]

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]

@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]

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

[Adam Topaz]

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

[Sebastian Ullrich]

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

[Adam Topaz]

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]

I'll take a look at direnv. Thanks!

[Sebastian Ullrich]

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

[Adam Topaz]

Does this not create a whole new installation of emacs?

[Sebastian Ullrich]

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

[Adam Topaz]

Oh ok.

[Adam Topaz]

"a bit" ~= 1G

[Reid Barton]

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

[Sebastian Ullrich]

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]

Hmm... what's the actual command?

[Adam Topaz]

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]

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

[Adam Topaz]

Yes, this works

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

BTW, why not put lean4-mode to melpa?

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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]

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

[Tomas Skrivan]

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]

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]

I'll try later tonight.

[Sebastian Ullrich]

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]

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]

Let me update lean4-mode first...

[Yury G. Kudryashov]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[David Thrane Christiansen]

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]

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

[Sebastian Ullrich]

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]

It's really a VSCode bug

[Reid Barton]

It makes emacs pretty much unusable for category theory unfortunately

[Sebastian Ullrich]

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]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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]

This works fine for me:

import Mathlib.Data.Real.ENNReal
open ENNReal

#check ℝ≥0∞

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

@Leonardo de Moura :up:

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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]

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]

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

[Yury G. Kudryashov]

I'll open a PR in the morning.

[Yury G. Kudryashov]

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

[Bulhwi Cha]

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]

leanprover/lean4-mode#41 fixes this

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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?