leanprover-community / lean4-mode Goto Github PK
View Code? Open in Web Editor NEWEmacs major mode for Lean 4
Home Page: https://leanprover.github.io/
License: Apache License 2.0
Emacs major mode for Lean 4
Home Page: https://leanprover.github.io/
License: Apache License 2.0
The option to collapse/expand trace nodes is extremely helpful when navigating e.g. typeclass synthesis traces. But at least with my setup (Doom Emacs + lean4-mode), the traces are always fully expanded with no option to collapse them. Could we get this capability as well?
Per the [ nix-doom-emacs
install instructions thread]#15 (comment)), I'd like to request that lean4-mode
be added to melpa
.
Lean (version 4.4.0, commit ca7d6dadb9e1, Release)
lean4-mode commit: d1c9364
GNU Emacs 28.1 (build 1, x86_64-pc-linux-gnu, GTK+ Version 3.24.20, cairo version 1.16.0) of 2022-05-31
Debugger entered--Lisp error: (error "The connected server(s) does not support method $/...")
signal(error ("The connected server(s) does not support method $/..."))
error("The connected server(s) does not support method %s..." "$/lean/plainGoal")
lsp--send-request-async((:jsonrpc "2.0" :method "$/lean/plainGoal" :params (:textDocument (:uri "file:///home/yuhta/tmp/test.lean") :position (:line 0 :character 9))) (closure (lean4-info-mode-abbrev-table t) (input0) (let* ((_ input0) (goals (if (ht\? _) (progn (gethash "goals" _))))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) tick ignore nil nil :plain-goal)
lsp-request-async("$/lean/plainGoal" (:textDocument (:uri "file:///home/yuhta/tmp/test.lean") :position (:line 0 :character 9)) (closure (lean4-info-mode-abbrev-table t) (input0) (let* ((_ input0) (goals (if (ht\? _) (progn (gethash "goals" _))))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler ignore :mode tick :cancel-token :plain-goal)
(progn (lsp-request-async "$/lean/plainGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goals (if ... ...))) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-goal) (lsp-request-async "$/lean/plainTermGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goal (if ... ...))) (setq lean4-term-goal goal) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-term-goal))
(if (lean4-info-buffer-active lean4-info-buffer-name) (progn (lsp-request-async "$/lean/plainGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goals ...)) (setq lean4-goals goals) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-goal) (lsp-request-async "$/lean/plainTermGoal" (lsp--text-document-position-params) #'(lambda (input0) (let* ((_ input0) (goal ...)) (setq lean4-term-goal goal) (lean4-info-buffer-redisplay-debounced))) :error-handler #'ignore :mode 'tick :cancel-token :plain-term-goal)))
lean4-info-buffer-refresh()
lean4-toggle-info()
funcall-interactively(lean4-toggle-info)
call-interactively(lean4-toggle-info nil nil)
command-execute(lean4-toggle-info)
I prefer to use the eglot language server implementation over lsp-mode
. It would be nice to have an option to set which language server to use, or to make the mode independent of the language server.
I'm not sure if I've done something wrong or if the installation instructions could be made a little more explicit.
Currently, my environment is:
doom-emacs
from nix-community/nix-doom-emacs and manage it via home-manager
.elan
is currently globally available, and leanprover/lean4:stable
is the default toolchain.When I add
(package! lean4-mode :recipe
(:host github
:repo "leanprover/lean4-mode"))
to my packages.el
and rebuild my nixos config (including doom-emacs
), I get the following error:
building Nix...
building the system configuration...
error: evaluation aborted with the following error message: 'Package not available: lean4-mode'
(use '--show-trace' to show detailed location information)
I also got this error before upgrading to 22.05. I also got this error before installing elan
systemwide.
Is there a path I need to set (vaguely comparable to the first set of instructions for installing lean4-mode
) to lean4
binaries?
My other guess is that doom-emacs
is looking in the wrong place (or an out-of-date place) for available packages, but I don't know why that would be the case. Maybe the package name has been tweaked?
Hi!
I have recently installed lean4-mode, following the instructions. I have used the first, "basic" method (i.e. without use-package).
I am, however, getting an error saying that Emacs can't activate the input method 'Lean'.
This error appears both on my Fedora desktop, as well as on my WSL2 Fedora setup on Windows.
Other Emacs input methods seem to work, e.g. the "greek" input method etc.
Due to this error, the lean4-mode does not start. However, after commenting out
(require 'lean4-input) and (set-input-method "Lean") in lean4-mode.el, it works (but \a does not yield alpha and so on, as expected), so "most" of the installation went as planned.
Any idea, how to amend this?
Is it possible to bundle evil keybindings into this package? I made some keybindings for the existing commands (doomemacs)
(map! :after lean4-mode
:localleader
:map lean4-mode-map
:desc "Execute" "R" #'lean4-execute
:desc "Execute in standalone" "r" #'lean4-std-exe
:desc "Toggle info buffer" "t" #'lean4-toggle-info
(:prefix ("e" . "Error")
:desc "Previous error" "p" #'flycheck-previous-error
:desc "Next error" "n" #'flycheck-next-error
:desc "List error" "l" #'flycheck-list-errors
)
:desc "Lake build" "b" #'lean4-lake-build
(:prefix ("p" . "leanpkg")
:desc "Test" "t" #'lean4-leanpkg-test
:desc "Build" "b" #'lean4-leanpkg-build
:desc "Configure" "c" #'lean4-leanpkg-configure
)
)
When i turn on lean4-mode, i saw this:
LSP :: The following servers support current file but do not have automatic installation: lean4-lsp
You may find the installation instructions at https://emacs-lsp.github.io/lsp-mode/page/languages.
(If you have already installed the server check *lsp-log*).
What should i do?
System: arch linux
Emacs: emacs 28.1 (native comp) & doom
Recently, when opening files in a Lean toolchain under .elan/
, lean4-mode has reliably failed to start the server, with an error message from elan
complaining that no default toolchain was configured. This is true and when I configured a default toolchain, the error went away, but then this toolchain would be started instead of the one to which the file belongs.
At that point, my .elan
was a symlink to ~/somedir/.elan
. When I removed the symlink and renamed the latter directory to .elan
, the error went away. So I suspect that the toolchain detection logic checks whether a directory is under .elan/toolchains
and gets confused when this is a symlink.
VSCode doesn't seem to have this issue, so maybe their detection logic can be reused.
For some reason even though there is a ton of space the text that tells you what the result of the #check directive is decides to wrap around. I'm using a 1080p monitor, Windows 10, the most recent git checkout, and emacs 27.9. I'm not sure what specific package is causing this so I have no idea which variable to play with to get it to not wrap.
The recent change in c736c0b to use lake serve
seems to cause a regression when opening files in core (i.e. .elan/toolchains/...
). With the LSP workspace set to ~/.elan/toolchains/leanprover--lean4---nightly-2022-03-18/src/lean
, it complains that ./lakefile.lean
cannot be parsed (probably because it doesn't exist). I can provide more detailed repro instructions if needed.
After #11, I am unable to see the goal in the goal view, and I see the following errors in my *Messages*
buffer:
Error in post-command-hook (lean4-info-buffer-redisplay-debounced): (void-function time-convert)
LSP :: Unable to autoconfigure company-mode. [2 times]
LSP :: lean4-lsp:473680 initialized successfully in folders: (/home/dwrensha/src/mathlib4)
LSP :: Unable to autoconfigure company-mode. [2 times]
Error running timer: (void-function time-convert)
Error running timer ‘lsp--on-idle’: (void-function time-convert) [34 times]
Error processing message (void-function time-convert). [14 times]
Does lean4 mode have something like this tactic state pane here?
When I commented out lean4-mode, 𝕜 can be displayed without problem. However when I enable lean4-mode, 𝕜 becomes square with unicode value (01D55C) in it. There are other symbols also having this problem. This happens even I comment out everything in init.el
and turn on lean4-mode
only.
Contrary to most major modes, syntax highlighting in lean4-mode
is not instantaneous, in the sense that if I start typing def a : Nat :=
, it won't syntax highlight until I have paused my typing, and even then there is a small delay. I haven't read the source code, but this behavior looks like as if syntax highlighting was actually performed by the language server, and passed through lsp
, which I suspect is because parsing lean actually requires (at least partially) understanding what is parsed, due to the possible instructions to modify the parsing behavior.
Yet, this feels pretty annoying, and I was wondering if it was possible to make it more snappy.
Hello, I'm newish to emacs and not sure if this is the place to post this. I have lean4-mode installed, and when I open a .lean file and type #check id
I see the correct type information displayed. However, when I type \a
, I do not get a unicode "alpha" as expected. What should I do to debug this?
I think the VS code extension has a pause button on the info buffer. I couldn't find this functionality, so added some quick and dirty advice to accomplish the same thing. Posting here in case helpful for others/someone wants to use this as inspiration for a PRhttps://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Pause.20emacs.20info
(defvar fov/lean4-pause-info nil "If non-nil, pause info buffer updates.")
(defun fov/lean4-info-buffer-redisplay (old-fun &rest args)
"Suppress call to OLD-FUN if `fov/lean4-pause-info' is non-nil. Otherwise call with ARGS."
(unless fov/lean4-pause-info
(apply old-fun args)))
(defun fov/lean4-toggle-info-pause ()
"Toggle pausing of automatic info refresh."
(interactive)
(setq fov/lean4-pause-info (not fov/lean4-pause-info)))
(defvar lean4-mode-map)
(with-eval-after-load 'lean4-mode
(advice-add 'lean4-info-buffer-redisplay :around #'fov/lean4-info-buffer-redisplay)
(define-key lean4-mode-map (kbd "C-c C-p C-p") #'fov/lean4-toggle-info-pause))
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Pause.20emacs.20info
In this screenshot, the highlighting of dbgTraceIfShared
is a bit funky:
It seems to me that the issue comes from here, where there is no word-end
in the rx
call, and that dbgTraceIfShared
should be part of lean4-debugging
as well.
Would a PR be welcome with this change?
Also, why do they call eval
? It seems to me that eval
on top of quote
should just be ordinary code. Could that be removed in the same PR?
See also leanprover/vscode-lean4#97. This is necessary for the workspace symbol search to work in mathlib4: leanprover/lake#46 (comment)
I updated to Emacs 29.4 today and since then, autocompletion has regularly produced ~3s lags during which the entire editor UI freezes. Unfortunately, I also updated a number of packages during the update, so it's hard to tell where the issue lies exactly. I hope you'll be able to reproduce with the following info.
Emacs: 29.4
Doom Emacs: a99c6b9036bde2f60697ce9f2ac259dfa2266dbf
Relevant packages (?):
lsp-mode cec9e56390e90d7ced3b18a922ab954e782b8628
lsp-ui 00f1fecdfb41c30428734cf27e492f26f46627fb
lean4-mode da7b63d854d010d621e2c82a53d6ae2d94dd53b0
company-mode 1a0fc12a9c3d25e28c22f319e7b097f435b1c27d
Repro:
f465af4466eeb1f195692745fd58bb3f552692f1
.Aesop/RuleTac/Forward.lean
.elabRuleTermForApplyLikeMetaM
and type elabRuleTermForApplyLikeMetaM
instead. This reliably freezes the UI at some point and autocompletion appears once the UI unfreezes again.The freeze doesn't always happen at the same point and it only happens when I type somewhat slower than normal, so perhaps the issue is typing when an autocompletion request is already in-flight.
Disabling autocompletion (lsp-completion-enable nil
) works around the issue.
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)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.