diff --git a/.gitignore b/.gitignore index 433da84..2998b25 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .cask *.elc +lean4-mode-autoloads.el \ No newline at end of file diff --git a/CHANGELOG.org b/CHANGELOG.org deleted file mode 100644 index 1ed62fe..0000000 --- a/CHANGELOG.org +++ /dev/null @@ -1,35 +0,0 @@ -#+title: Lean4-Mode - Changelog -#+language: en - -* Version 1.1.2 - -- Fix occasional errors like "The connected server(s) does not support - method =$/lean/plainGoal=" by not wrapping invocations of - ~lsp-protocol~ macro into ~eval-when-compile~ but rather into - ~eval-and-compile~. Thus, the methods should now work, no matter - whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by - loading compiled =.elc= or =.eln= files. ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]]) - -* Version 1.1.1 - -- Assign all customizable user-options to the Lean4-Mode specific - =lean4= group. To customize Lean4-Mode, you now need to type =M-x - customize-group RET lean4 RET=. - -* Version 1.1.0 - -- To =lean4= customization group, add link to local info manual and - use Lean4-Mode Github URL as website. -- Introduce new dependency on Elpa package =compat=. -- Remove dependency on Elpa package Flycheck. It is still supported - but not required. - -* Version 1.0.1 - -- Specify Yury G. Kudryashov as maintainer. -- Rework README. (Now in Org format). -- Provide README as Texi and Info manual too. - -* Version 1.0 - -- Specify "Version" in Emacs-Lisp library header. diff --git a/Makefile b/Makefile index 89e8f6c..7f8c87e 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,28 @@ # GNU- and NonGNU-Elpa accept Org files as package documentation but # Melpa does not. As long as Lean4-Mode is not distributed on GNU- or # NonGNU-Elpa, it should ship with .texi and .info manuals. This -# depends on: GNU Emacs, Make and GNU Texinfo. +# depends on: GNU Emacs, Make, GNU Texinfo and the “sponge” program +# bundled in the “Moreutils” collection that is maintained by Joey +# Hess. -lean4-mode.info lean4-mode.texi: README.org +.PHONY: all autoload clean info +all : autoload info + +clean: + rm -f lean4-mode.info lean4-mode.texi lean4-mode-autoloads.el + +autoload: lean4-mode-autoloads.el +lean4-mode-autoloads.el : $(wildcard *.el) + emacs --batch \ + --eval '(setq make-backup-files nil)' \ + --eval '(setq generated-autoload-file "./$@")' \ + --eval "(require 'autoload)" \ + -f batch-update-autoloads '.' + cat $@ | sponge | sed s/"This file is part of GNU Emacs"/"This file is NOT part of GNU Emacs"/ > $@ + +info: lean4-mode.info lean4-mode.texi +lean4-mode.info lean4-mode.texi : README.org emacs --batch \ - "--eval=(require 'ox-texinfo)" \ - '--eval=(find-file "$<")' \ - '--eval=(org-texinfo-export-to-info)' + --eval "(require 'ox-texinfo)" \ + --eval '(find-file "$<")' \ + --eval '(org-texinfo-export-to-info)' diff --git a/README.org b/README.org index ac66c63..af9afa5 100644 --- a/README.org +++ b/README.org @@ -1,39 +1,43 @@ -#+title: Lean4-Mode - Emacs major mode for Lean language +#+title: Emacs Lean4-Mode #+language: en #+export_file_name: lean4-mode.texi #+texinfo_dir_category: Emacs misc features #+texinfo_dir_title: Lean4-Mode: (lean4-mode). -#+texinfo_dir_desc: Emacs major mode for Lean language +#+texinfo_dir_desc: Emacs major mode for Lean4 language -This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing -code written in version 4 of the programming language and theorem -prover [[https://lean-lang.org][Lean]]. +This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by a major mode for [[https://lean-lang.org][Lean]] version 4, a +programming language and theorem prover. -The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues -tracked there too. Further discussions and question-answering takes -place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat. - -For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known -as /Lean-Mode/). +Lean4-Mode is developed on [[https://github.com/leanprover-community/lean4-mode][Github]]. Bugs and feature requests are also +tracked there. Further discussions take place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs]] channel +on the Lean Zulip chat platform. * Installation -** Brief and Generic Instructions +** Brief, Generic Instructions First, install the dependencies of Lean4-Mode: - [[https://lean-lang.org/lean4/doc/setup.html][Lean]] (version 4) - Emacs (version 27 or later) - Emacs packages [[https://github.com/magnars/dash.el][Dash]] (available on GNU-Elpa), [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (available on Melpa) +Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: -- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]]. -- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to that local - repository to the ~load-path~ list. -# Note that (require 'lean4-mode) is not necessary when the user -# relies on autoloading and uses the default settings. +- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository]]. +- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to your local + repository to ~load-path~. + +Third, ensure Lean4-Mode is loaded by one of the following ways: +- Load it eagerly. +- Load it lazily by associating ~lean4-mode~ with the =.lean= file + extension and setting it up as autoloaded command. +- Load it lazily by generating an autoload file (with the Make target + called =autoload=) and loading that in your init file. Make sure to + regenerate the autoload file, whenever you change the Lean4-Mode + repository (e.g. =git pull=). -** Detailed and Concrete Instructions +** Detailed, Native Instructions Install Lean version 4. @@ -72,29 +76,64 @@ Lean4-Mode repository to the ~load-path~ list: (add-to-list 'load-path "~/path/to/lean4-mode") #+end_src -Lean4-Mode should now already be enabled when you open a file with -=.lean= extension. But you can optionally also already load -Lean4-Mode on Emacs startup, e.g. in order to customize variables: +Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + +If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: #+begin_src elisp (require 'lean4-mode) #+end_src +If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 source +file is opened the first time, put in your init file: +#+begin_src elisp +(autoload 'lean4-mode "lean4-mode" nil t) +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) +#+end_src + +If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your +Git repository changes (e.g. =git pull=), run =make autoload= +inside. And put this in your init file: +#+begin_src elisp +(require 'lean4-mode-autoloads) +#+end_src + ** Instructions for Source-Based Use-Package +This section instructs how to set up Lean4-Mode through the +~use-package~ macro that is built into Emacs since version 29. + If you use a source-based package-manager (e.g. =package-vc.el=, Straight or Elpaca), then make sure to list the ="data"= directory in your Lean4-Mode package recipe. -If you use the ~use-package~ macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure -to specify ~lean4-mode~ as a =:command=. +When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like ~lean4-mode-hook~ have non-nil initialization +values. And since ~use-package~ applies the =:hook= specifications +before package loading, you should avoid it. Instead, put +=(add-hook 'lean4-...-hook #'...)= under the =:config= section. (See +/Common Pitfalls/ section below.) + +Use-Package [[https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html][involves]] some complexity when it comes to deciding whether +to load a package eagerly (/demand/) or lazily (/defer/). For example, +it depends on your configuration (e.g. ~use-package-always-defer~, +~use-package-always-demand~). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via =:demand t=. Alternatively, +you can defer loading e.g. via =:defer t= together with +=:mode "\\.lean\\'"= (which associates Lean4-Mode with the =.lean= +file extension) and =:commands lean4-mode= (which will set up +autoloading). Following subsections show concrete examples. *** Native =:vc= (Emacs 30 or later) -GNU Emacs comes with =use-package.el= built-in since version 29. And -since version 30, it also comes with a built-in =:vc= keyword for the +Since version 30, Emacs comes with a built-in =:vc= keyword for the ~use-package~ macro that utilizes =package-vc.el= to install Emacs packages from remote source repositories. @@ -106,23 +145,24 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :mode "\\.lean\\'" + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) #+end_src -*** Doom-Emacs +*** Doom ~package!~ If you use Doom-Emacs, you can place the following code in your Doom initialization file: #+begin_src elisp (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) #+end_src *** Straight @@ -133,6 +173,7 @@ place the following code in your Emacs initialization file: #+begin_src elisp (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) @@ -140,23 +181,23 @@ place the following code in your Emacs initialization file: * Usage -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with =.lean= extension. Emacs will ask you to identify the /project/ this file belongs to. If you then type =#check id=, the word =#check= will be underlined, and hovering over it will show you the type of ~id~. -To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This -will display the =*Lean Goals*= buffer (like the Lean Info-View pane +To view the proof state, run ~lean4-info-mode~ (=C-c C-i=). This +will display the =*Lean4 Info*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. -| Key | Description | Command | -|------------------------+--------------------------------------------------------+-----------------------------------| -| =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | -| =C-c C-d= | Recompile and reload imports | ~lean4-refresh-file-dependencies~ | -| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-std-exe~ | -| =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | -| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | +| Key | Description | Command | +|------------------------+--------------------------------------------------------+-----------------------------| +| =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | +| =C-c C-d= | Recompile and reload imports | ~lean4-lsp-document-reopen~ | +| =C-c C-x= or =C-c C-l= | Execute Lean4 in stand-alone mode | ~lean4-execute~ | +| =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | +| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-info-mode~ | ** lsp-mode @@ -194,9 +235,162 @@ option accordingly. * Common Pitfalls -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix =lean-= for its symbols. E.g. you should not use -=lean-=-prefixed commands in a buffer with Lean4-Mode as major mode. +** Coexistence with Lean3-Mode + +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]]. It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + +- Lean3-Mode uses =lean-= as prefix (e.g. for commands) whereas + Lean4-Mode uses =lean4-= as prefix. When Lean4-Mode is active, + you must not use commands with prefix =lean-=. + +- Both packages associate the =.lean= file extension with their + respective commands. Even more confusingly, they use different + functions and regular expressions to do so. + + Lean3-Mode: + #+begin_src elisp + ;;;###autoload + (push '("\\.lean$" . lean-mode) auto-mode-alist) + #+end_src + + Lean4-Mode: + #+begin_src elisp + ;;;###autoload + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) + #+end_src + + Make sure that both packages are loaded, autoloaded and configured + in such a way ~auto-mode-alist~ ends up with your desired value. + +- In particular, if you want Emacs to automatically detect whether + Lean3- or Lean4-Mode should be used for a particular file or + project, you'll need to define your own Elisp function and associate + it with the Lean file extension. If desired, you can even do this + directory locally (via the special "variable" =eval= in + =.dir-locals.el=). + +** Partial value of ~lean4-mode-hook~ or other hook variables + +If you customize a hook variable like ~lean4-mode-hook~ e.g. with +~add-hook~ or Use-Package's =:hook= keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +~lean4-mode-hook~ may not contain the ~lsp~ command and as a +consequence ~lsp-mode~ won't start automatically together with +Lean4-Mode. + +There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your ~add-hook~ form before it loads +the definition of the hook from Lean4-Mode package. (3.) ~add-hook~ +effectively initializes the passed hook-variable to nil when the +symbol has no value cell. And (4.), Use-Package applies passed =:hook= +specifications before package loading. + +If you do not use Use-Package, the solution is to load Lean4-Mode +before calling ~add-hook~, e.g. with ~require~: +#+begin_src elisp +(require 'lean4-mode) +(add-hook 'lean4-...-hook #'...) +#+end_src + +Or with ~with-eval-after-load~: +#+begin_src elisp +(with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) +(with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) +#+end_src + +If you do Use-Package, you can solve the problem by calling ~add-hook~ +within the =:config= section: +#+begin_src elisp +(use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) +#+end_src + +* Changelog + +** Upcoming Version + +Documentation: +- The changelog is now part of the readme (and thus of the Info + manual). + +User interface: +- The tool-bar menu of Lean4-Mode does not list the + ~flycheck-list-errors~ anymore. Please use the “Show all errors” + entry in Flycheck's menu instead. (Fixes [[https://github.com/leanprover-community/lean4-mode/issues/91][#91]].) + +Features: +- The variable ~lean4-delete-trailing-whitespace~ has been removed + together with related code. Instead of reinventing the wheel, + Lean4-Mode demands users to use Emacs' built-in facilities for this + kind of use case. For example, you might want to define a function + that buffer-locally adds ~delete-trailing-whitespace~ to + ~before-save-hook~, and add that hereby defined function to + ~lean4-mode-hook~. +- The variable ~lean4-autodetect-lean3~ has been removed along with + the command ~lean4-select-mode~ and related code. If you still use + legacy version 3 of Lean for some files or projects, you could + directory- or file-locally associate the =.lean= file extension with + Lean3-Mode in ~auto-mode-alist~. +- The command ~lean4-show-version~ has been removed. Lean4-Mode now + assumes Lean version 4. In order to determine the minor version, you + may type =M-! lean --version RET= or similar. +- The functions ~lean4-input-export-translations~ and + ~lean4-input-export-translations-to-stdout~ have been removed. We + expect that noone has been using it. If you do use it, let us know, + so we can reconsider our decision in case of a substantial amount of + users. Otherwise, please just define these functions in your Emacs + initialization file yourself. +- The command ~lean4-std-exe~ has been removed. It was just the same + as ~lean4-execute~ which continues to exist. + +** Version 1.1.2 from 2024-12-10 + +- Fix occasional errors like "The connected server(s) does not support + method =$/lean/plainGoal=" by not wrapping invocations of + ~lsp-protocol~ macro into ~eval-when-compile~ but rather into + ~eval-and-compile~. Thus, the methods should now work, no matter + whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by + loading compiled =.elc= or =.eln= files. ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]]) + +** Version 1.1.1 from 2024-12-02 + +- Assign all customizable user-options to the Lean4-Mode specific + =lean4= group. To customize Lean4-Mode, you now need to type =M-x + customize-group RET lean4 RET=. + +** Version 1.1.0 from 2024-12-01 + +- To =lean4= customization group, add link to local info manual and + use Lean4-Mode Github URL as website. +- Introduce new dependency on Elpa package =compat=. +- Remove dependency on Elpa package Flycheck. It is still supported + but not required. + +** Version 1.0.1 from 2024-11-21 + +- Specify Yury G. Kudryashov as maintainer. +- Rework README. (Now in Org format). +- Provide README as Texi and Info manual too. + +** Version 1.0 from 2024-11-16 + +- Specify "Version" in Emacs-Lisp library header. + +* Contributing + +When you contribute to Lean4-Mode, add a personal copyright like +=;; Copyright (c) 2024 Firstname Lastname= to the header of respective +files. + +You can use Emacs' built-in ~bug-reference-mode~ and +~bug-reference-prog-mode~ in this repository to make mentions of +issues like =#123= clickable. diff --git a/lean4-eri.el b/lean4-eri.el index a85b474..745d507 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -1,10 +1,10 @@ -;;; lean4-eri.el --- Lean4-Mode Indentation -*- lexical-binding: t; -*- +;;; lean4-eri.el --- Lean4 indentation -*- lexical-binding: t; -*- ;; Copyright (c) 2005-2010 Ulf Norell, Nils Anders Danielsson, ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, ;; Marcin Benke, Darin Morrison. -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -20,6 +20,10 @@ ;;; Commentary: +;; This file eventually defines the `lean4-eri-tab' command that +;; context-sensitively indents the current line, as appropriate for +;; the Lean4 language. + ;; This file is based on eri.el which was part of Agda-Mode: ;; https://github.com/agda/agda/blob/b40c6fc2e0ced7b547553654f81e5898082d700c/src/data/emacs-mode/eri.el @@ -223,5 +227,12 @@ are calculated." (interactive) (lean4-eri-indent t)) +(defun lean4-eri-tab () + "Lean4 function for TAB indent." + (interactive) + (cond ((looking-back (rx line-start (* white)) nil) + (lean4-eri-indent)) + (t (indent-for-tab-command)))) + (provide 'lean4-eri) ;;; lean4-eri.el ends here diff --git a/lean4-fringe.el b/lean4-fringe.el index e5ab9e0..b695de9 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -1,8 +1,8 @@ -;;; lean4-fringe.el --- Lean4-Mode Processing Progress in Fringe -*- lexical-binding: t; -*- +;;; lean4-fringe.el --- Lean4 fringe progress -*- lexical-binding: t; -*- -;; Copyright (c) 2016 Microsoft Corporation. All rights reserved. +;; Copyright (c) 2016 Microsoft Corporation -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -18,14 +18,26 @@ ;;; Commentary: -;; Show Lean processing progress in the editor fringe +;; In `lean4-mode', indicate the processing progress of `lsp-mode' in +;; Emacs window fringes. + +;; For documentation on Emacs fringes, see (info "(emacs) Fringes") or +;; equally: https://gnu.org/s/emacs/manual/html_node/emacs/Fringes ;;; Code: -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) +(defgroup lean4-fringe nil + "Lean4 lsp-mode processing progress in fringes." + :group 'lean4) + +(defcustom lean4-fringe-show-file-progress t + "Highlight file progress in the current buffer." + :group 'lean4-fringe + :type 'boolean) + (eval-and-compile (lsp-interface (lean:LeanFileProgressProcessingInfo (:range :kind) nil) @@ -38,8 +50,8 @@ (defface lean4-fringe-face nil - "Face to highlight Lean file progress." - :group 'lean4) + "Face to highlight Lean4 file progress." + :group 'lean4-fringe) (if (fboundp 'define-fringe-bitmap) (define-fringe-bitmap 'lean4-fringe-fringe-bitmap @@ -51,8 +63,8 @@ (((class color) (background dark)) :background "navajo white") (t :inverse-video t)) - "Face to highlight the fringe of Lean file processing progress." - :group 'lean4) + "Face to highlight the fringe of Lean4 file processing progress." + :group 'lean4-fringe) (defface lean4-fringe-fringe-fatal-error-face '((((class color) (background light)) @@ -60,8 +72,8 @@ (((class color) (background dark)) :background "red") (t :inverse-video t)) - "Face to highlight the fringe of Lean file fatal errors." - :group 'lean4) + "Face to highlight the fringe of Lean4 file fatal errors." + :group 'lean4-fringe) (lsp-defun lean4-fringe-fringe-face ((&lean:LeanFileProgressProcessingInfo :kind)) (cond @@ -75,7 +87,7 @@ (dolist (ov (flatten-tree (overlay-lists))) (when (eq (overlay-get ov 'face) 'lean4-fringe-face) (delete-overlay ov))) - (when lean4-show-file-progress + (when lean4-fringe-show-file-progress (seq-doseq (item lean4-fringe-data) (let* ((reg (lean4-fringe-region item)) (ov (make-overlay (car reg) (cdr reg)))) diff --git a/lean4-info.el b/lean4-info.el index 923cf56..a892e96 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -1,8 +1,8 @@ -;;; lean4-info.el --- Lean4-Mode Info View -*- lexical-binding: t; -*- +;;; lean4-info.el --- Lean4 info -*- lexical-binding: t; -*- -;; Copyright (c) 2016 Gabriel Ebner. All rights reserved. +;; Copyright (c) 2016 Gabriel Ebner -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -18,37 +18,103 @@ ;;; Commentary: -;; This library provides an advanced LSP feature for `lean4-mode'. +;; This file defines `lean4-info-mode', a minor mode for `lean4-mode' +;; that keeps a buffer updated with an appealing display of LSP backed +;; information relevant at point, such as proof goals, type signatures +;; and error messages. + +;;;; Details on Debouncing + +;; We want to update the Lean4 info buffer as seldom as possible, +;; since magit-section is slow at rendering. We wait a small duration +;; (`debounce-delay-sec') when we get a redisplay request, to see if +;; there is a redisplay request in the future that invalidates the +;; current request (debouncing). Pictorially: + +;; (a) One request: +;; --r1 +;; --r1.wait +;; ----------r1.render + +;; (b) Two requests in quick succession: +;; +;; --r1 +;; --r1.wait +;; --------r2(cancel r1.wait) +;; --------r2.wait +;; ---------------r2.render + +;; (c) Two requests, not in succession: +;; +;; --r1 +;; --r1.wait +;; ---------r1.render +;; ------------------r2 +;; ------------------r2.wait +;; -------------------------r2.render + +;; This delaying can lead to a pathological case where we continually +;; stagger, while not rendering anything: +;; +;; --r1 +;; --r1.wait +;; --------r2(cancel r1.wait) +;; --------r2.wait +;; --------------r3(cancel r2.wait) +;; ---------------r3.wait +;; ---------------------r4(cancel r3.wait) +;; ---------------------... + +;; We prevent this pathological case by keeping track of when when we +;; began debouncing in `lean4-info-buffer-debounce-begin-time'. If we +;; have been debouncing for longer than +;; `lean4-info-buffer-debounce-upper-bound-sec', then we immediately +;; write instead of debouncing; `max-debounces' times. Upon trying to +;; stagger the `max-debounces'th request, we immediately render: +;; +;; begin-time:nil----t0----------------nil------- +;; -------r1 | +;; -------r1.wait | +;; -------|-----r2(cancel r1.wait) +;; -------|-----r2.wait | +;; -------|-----------r3(cancel r2.wait) +;; -------|-----------r3.wait +;; -------|-----------------r4(cancel r3.wait) +;; -------|-----------------| +;; >-----------------< +;; >longer than `debounce-upper-bound-sec'< +;; -------------------------r4.render(FORCED) ;;; Code: (require 'dash) -(require 'lean4-syntax) -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) (require 'magit-section) +(require 'lean4-syntax) + (defgroup lean4-info nil "Lean4-Mode Info." :group 'lean4) -;; Lean Info Mode (for "*lean4-info*" buffer) -;; Automode List +(defcustom lean4-info-highlight-inaccessibles t + "Use font to highlight inaccessible names. +Set this variable to t to highlight inaccessible names in the info display +using `font-lock-comment-face' instead of the `✝` suffix used by Lean4." + :group 'lean4-info + :type 'boolean) + ;;;###autoload -(define-derived-mode lean4-info-mode prog-mode "Lean-Info" - "Major mode for Lean4-Mode Info Buffer." +(define-derived-mode lean4-info-mockup-mode prog-mode "Lean4-Info" + "Major mode used internally to syntax highlight Lean4." :syntax-table lean4-syntax-table - :group 'lean4 - (set (make-local-variable 'font-lock-defaults) lean4-info-font-lock-defaults) - (set (make-local-variable 'indent-tabs-mode) nil) - (set 'compilation-mode-font-lock-keywords '()) - (set (make-local-variable 'lisp-indent-function) - 'common-lisp-indent-function)) - -(defun lean4-ensure-info-buffer (buffer) + :group 'lean4-info + (setq-local font-lock-defaults lean4-info-font-lock-defaults)) + +(defun lean4-info-ensure-buffer (buffer) "Create BUFFER if it does not exist. -Also choose settings used for the *Lean Goal* buffer." +Also choose settings used for the *Lean4 Info* buffer." (unless (get-buffer buffer) (with-current-buffer (get-buffer-create buffer) (buffer-disable-undo) @@ -56,14 +122,6 @@ Also choose settings used for the *Lean Goal* buffer." (set-syntax-table lean4-syntax-table) (setq buffer-read-only t)))) -(defun lean4-toggle-info-buffer (buffer) - "Create or delete BUFFER. -The buffer is supposed to be the *Lean Goal* buffer." - (-if-let (window (get-buffer-window buffer)) - (quit-window nil window) - (lean4-ensure-info-buffer buffer) - (display-buffer buffer))) - (defun lean4-info-buffer-active (buffer) "Check whether given info BUFFER should show info for current buffer." (and @@ -80,10 +138,10 @@ The buffer is supposed to be the *Lean Goal* buffer." (:range :fullRange :message) (:code :relatedInformation :severity :source :tags)))) -(defconst lean4-info-buffer-name "*Lean Goal*") +(defconst lean4-info-buffer-name "*Lean4 Info*") -(defvar lean4-goals nil) -(defvar lean4-term-goal nil) +(defvar lean4-info-goals nil) +(defvar lean4-info-term-goal nil) (lsp-defun lean4-diagnostic-full-start-line ((&lean:Diagnostic :full-range (&Range :start (&Position :line)))) line) @@ -103,7 +161,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (defun lean4-info--insert-highlight-inaccessible-names (&rest text) (let ((begin (point))) (apply #'insert text) - (when lean4-highlight-inaccessible-names + (when lean4-info-highlight-inaccessibles (let ((end (point-marker))) (goto-char begin) (while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" end t) @@ -114,9 +172,9 @@ The buffer is supposed to be the *Lean Goal* buffer." 'fixedcase 'literal)) (goto-char end))))) -(defun lean4--insert-goal-text (text delimiter) +(defun lean4-info--insert-goal-text (text delimiter) (lean4-info--insert-highlight-inaccessible-names - (lsp--fontlock-with-mode text 'lean4-info-mode) + (lsp--fontlock-with-mode text 'lean4-info-mockup-mode) delimiter)) (defun lean4-info--mk-message-section (value caption messages buffer) @@ -152,90 +210,32 @@ The buffer is supposed to be the *Lean Goal* buffer." (progn (erase-buffer) (magit-insert-section (magit-section 'root) - (when-let ((goals lean4-goals)) ;; capture for deferred rendering + (when-let ((goals lean4-info-goals)) ;; capture for deferred rendering (magit-insert-section (magit-section 'goals) (magit-insert-heading "Goals:") (magit-insert-section-body (if (> (length goals) 0) (seq-doseq (g goals) (magit-insert-section (magit-section) - (lean4--insert-goal-text g "\n\n"))) + (lean4-info--insert-goal-text g "\n\n"))) (insert "goals accomplished\n\n"))))) - (when-let ((term-goal lean4-term-goal)) ;; capture for deferred rendering + (when-let ((term-goal lean4-info-term-goal)) ;; capture for deferred rendering (magit-insert-section (magit-section 'term-goal) (magit-insert-heading "Expected type:") (magit-insert-section-body - (lean4--insert-goal-text term-goal "\n")))) + (lean4-info--insert-goal-text term-goal "\n")))) (lean4-info--mk-message-section 'errors-here "Messages here:" errors-here buffer) (lean4-info--mk-message-section 'errors-below "Messages below:" errors-below buffer) (lean4-info--mk-message-section 'errors-above "Messages above:" errors-above buffer))))))) -;; Debouncing -;; ~~~~~~~~~~~ -;; We want to update the Lean4 info buffer as seldom as possible, -;; since magit-section is slow at rendering. We -;; wait a small duration (`debounce-delay-sec') when we get a -;; redisplay request, to see if there is a redisplay request in the -;; future that invalidates the current request (debouncing). -;; Pictorially, -;; (a) One request: -;; --r1 -;; --r1.wait -;; ----------r1.render -;; (b) Two requests in quick succession: -;; --r1 -;; --r1.wait -;; --------r2(cancel r1.wait) -;; --------r2.wait -;; ---------------r2.render -;; (c) Two requests, not in succession: -;; --r1 -;; --r1.wait -;; ---------r1.render -;; ------------------r2 -;; ------------------r2.wait -;; -------------------------r2.render -;; This delaying can lead to a pathological case where we continually -;; stagger, while not rendering anything: -;; --r1 -;; --r1.wait -;; --------r2(cancel r1.wait) -;; --------r2.wait -;; --------------r3(cancel r2.wait) -;; ---------------r3.wait -;; ---------------------r4(cancel r3.wait) -;; ---------------------... -;; We prevent this pathological case by keeping track of when -;; when we began debouncing in `lean4-info-buffer-debounce-begin-time'. -;; If we have been debouncing for longer than -;; `lean4-info-buffer-debounce-upper-bound-sec', then we -;; immediately write instead of debouncing; -;; `max-debounces' times. Upon trying to stagger the -;; `max-debounces'th request, we immediately render: -;; begin-time:nil----t0----------------nil------- -;; -------r1 | -;; -------r1.wait | -;; -------|-----r2(cancel r1.wait) -;; -------|-----r2.wait | -;; -------|-----------r3(cancel r2.wait) -;; -------|-----------r3.wait -;; -------|-----------------r4(cancel r3.wait) -;; -------|-----------------| -;; >-----------------< -;; >longer than `debounce-upper-bound-sec'< -;; -------------------------r4.render(FORCED) - - (defcustom lean4-info-buffer-debounce-delay-sec 0.1 - "Duration of time we wait before writing to *Lean Goal*." + "Duration of time we wait before writing to *Lean4 Info*." :group 'lean4-info :type 'number) - (defvar lean4-info-buffer-debounce-timer nil "Timer that is used to debounce Lean4 info view refresh.") - (defvar lean4-info-buffer-debounce-begin-time nil "Return the time we have begun debouncing. @@ -252,7 +252,7 @@ the request." :group 'lean4-info :type 'number) -;; Debounce implementation modifed from lsp-lens +;; This is based on lsp-lens.el from lsp-mode: ;; https://github.com/emacs-lsp/lsp-mode/blob/2f0ea2e396ec9a570f2a2aeb097c304ddc61ebee/lsp-lens.el#L140 (defun lean4-info-buffer-redisplay-debounced () "Debounced version of `lean4-info-buffer-redisplay'. @@ -260,20 +260,20 @@ the request." This version ensures that info buffer is not repeatedly written to. This is to prevent lag, because magit is quite slow at building sections." - ;; if we have not begun debouncing, setup debouncing begin time. + ;; If we have not begun debouncing, setup debouncing begin time. (if (not lean4-info-buffer-debounce-begin-time) (setq lean4-info-buffer-debounce-begin-time (current-time))) - ;; if time since we began debouncing is too long... + ;; If time since we began debouncing is too long... (if (>= (time-to-seconds (time-subtract (current-time) lean4-info-buffer-debounce-begin-time)) lean4-info-buffer-debounce-upper-bound-sec) - ;; then redisplay immediately. + ;; then redisplay immediately. (progn - ;; We have stopped debouncing. + ;; We have stopped debouncing. (setq lean4-info-buffer-debounce-begin-time nil) (lean4-info-buffer-redisplay)) - ;; else cancel current timer, create new debounced timer. + ;; Else, cancel current timer and create new debounced timer. (-some-> lean4-info-buffer-debounce-timer cancel-timer) (setq lean4-info-buffer-debounce-timer ; set new timer (run-with-timer @@ -286,13 +286,13 @@ sections." (defun lean4-info-buffer-refresh () - "Refresh the *Lean Goal* buffer." + "Refresh the *Lean4 Info* buffer." (when (lean4-info-buffer-active lean4-info-buffer-name) (lsp-request-async "$/lean/plainGoal" (lsp--text-document-position-params) (-lambda ((ignored &as &lean:PlainGoal? :goals)) - (setq lean4-goals goals) + (setq lean4-info-goals goals) (lean4-info-buffer-redisplay-debounced)) :error-handler #'ignore :mode 'tick @@ -301,20 +301,47 @@ sections." "$/lean/plainTermGoal" (lsp--text-document-position-params) (-lambda ((ignored &as &lean:PlainTermGoal? :goal)) - (setq lean4-term-goal goal) + (setq lean4-info-term-goal goal) (lean4-info-buffer-redisplay-debounced)) :error-handler #'ignore :mode 'tick - :cancel-token :plain-term-goal) - ;; may lead to flickering - ;(lean4-info-buffer-redisplay) - )) - -(defun lean4-toggle-info () - "Show infos at the current point." - (interactive) - (lean4-toggle-info-buffer lean4-info-buffer-name) - (lean4-info-buffer-refresh)) + :cancel-token :plain-term-goal))) + +(defcustom lean4-info-hookings + (list + (cons 'flycheck-after-syntax-check-hook + #'lean4-info-buffer-redisplay-debounced) + (cons 'post-command-hook + #'lean4-info-buffer-redisplay-debounced) + (cons 'lsp-on-idle-hook + #'lean4-info-buffer-refresh)) + "Pairs of hooks and functions to be toggled by `lean4-info-mode'. + +The value should be an alist associating hook variables with functions. +When `lean4-info-mode' is turned on, the function will be added +buffer-locally to the hook. When turned off, it'll be removed +buffer-locally." + :type '(repeat (cons variable function)) + :group 'lean4-info) + +(define-minor-mode lean4-info-mode + "Minor mode for `lean4-mode' to keep Lean4 Info buffer updated." + :lighter "ⓘ" + (if lean4-info-mode + (progn + (lean4-info-ensure-buffer lean4-info-buffer-name) + (display-buffer lean4-info-buffer-name) + (lean4-info-buffer-refresh) + (mapc (lambda (hooking) + (when (boundp (car hooking)) + (add-hook (car hooking) (cdr hooking) nil 'local))) + lean4-info-hookings)) + (when-let* ((window (get-buffer-window lean4-info-buffer-name))) + (quit-window nil window) + (mapc (lambda (hooking) + (when (boundp (car hooking)) + (remove-hook (car hooking) (cdr hooking) 'local))) + lean4-info-hookings)))) (provide 'lean4-info) ;;; lean4-info.el ends here diff --git a/lean4-input.el b/lean4-input.el index fce884f..83d09f7 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -1,10 +1,10 @@ -;;; lean4-input.el --- Lean4-Mode Input Method -*- lexical-binding: t; -*- +;;; lean4-input.el --- Lean4 input -*- lexical-binding: t; -*- ;; Copyright (c) 2005-2012 Ulf Norell, Nils Anders Danielsson, ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, ;; Marcin Benke, Darin Morrison. -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -22,13 +22,13 @@ ;; A highly customisable input method which can inherit from other ;; Quail input methods. By default the input method is geared towards -;; the input of mathematical and other symbols in Lean programs. +;; the input of mathematical and other symbols in Lean4 programs. -;; Use M-x customize-group lean4-input to customise this input method. -;; Note that the functions defined under "Functions used to tweak -;; translation pairs" below can be used to tweak both the key -;; translations inherited from other input methods as well as the -;; ones added specifically for this one. +;; Use M-x customize-group lean4-input RET to customize this input +;; method. Note that the functions defined under "Functions used to +;; tweak translation pairs" below can be used to tweak both the key +;; translations inherited from other input methods as well as the ones +;; added specifically for this one. ;; Use lean4-input-show-translations to see all the characters which ;; can be typed using this input method (except for those @@ -39,18 +39,19 @@ ;;; Code: -(require 'quail) (require 'cl-lib) +(require 'map) +(require 'quail) (require 'subr-x) + (require 'dash) -(require 'map) -;; Quail is quite stateful, so be careful when editing this code. Note -;; that with-temp-buffer is used below whenever buffer-local state is -;; modified. +;; Quail is quite stateful, so be careful when editing this code. +;; Note that `with-temp-buffer' is used below whenever buffer-local +;; state is modified. -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Utility functions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Utility functions (defun lean4-input-concat-map (f xs) "Concat (map F XS)." @@ -72,8 +73,8 @@ First remove all space and newline characters." (setq seq (cons (+ from i) seq))) (concat (nreverse seq)))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions used to tweak translation pairs +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Functions used to tweak translation pairs (defun lean4-input-compose (f g) "\\x -> concatMap F (G x)." @@ -134,18 +135,20 @@ This suffix is dropped." (lean4-input-drop-end (length suffix)) (lean4-input-suffix suffix))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Customization +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Customization -;; The :set keyword is set to 'lean4-input-incorporate-changed-setting -;; so that the input method gets updated immediately when users -;; customize it. However, the setup functions cannot be run before all -;; variables have been defined. Hence the :initialize keyword is set to -;; 'custom-initialize-default to ensure that the setup is not performed -;; until lean4-input-setup is called at the end of this file. +;; The `:set' keyword is set to +;; `lean4-input-incorporate-changed-setting' so that the input method +;; gets updated immediately when users customize it. However, the +;; setup functions cannot be run before all variables have been +;; defined. Hence the `:initialize' keyword is set to +;; `custom-initialize-default' to ensure that the setup is not +;; performed until `lean4-input-setup' is called at the end of this +;; file. (defgroup lean4-input nil - "The Lean input method. + "The Lean4 input method. After tweaking these settings you may want to inspect the resulting translations using `lean4-input-show-translations'." :group 'lean4 @@ -162,7 +165,7 @@ translations using `lean4-input-show-translations'." (lean4-input-prefix "^")) (lean4-input-prefix "_")))))) "List of parent Quail input methods. -Translations from these methods will be inherited by the Lean +Translations from these methods will be inherited by the Lean4 input method (with the exception of translations corresponding to ASCII characters). @@ -189,7 +192,7 @@ order for the change to take effect." :type 'directory) (defcustom lean4-input-user-translations nil - "A list of translations specific to the Lean input method. + "A list of translations specific to the Lean4 input method. Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). All the translation strings are possible translations of the given key sequence; if there is more than one you can choose @@ -211,7 +214,7 @@ from other input methods." Result is a list of pairs (KEY-SEQUENCE . TRANSLATION) that contains all translations from QP Except for those corresponding to ASCII." (with-temp-buffer - (activate-input-method qp) ; To make sure that the package is loaded. + (activate-input-method qp) ;; Ensure that package is loaded. (unless (quail-package qp) (error "%s is not a Quail package" qp)) (let ((decode-map (list 'decode-map))) @@ -222,7 +225,7 @@ that contains all translations from QP Except for those corresponding to ASCII." "Display all translations used by the Quail package QP (a string). \(Except for those corresponding to ASCII)." (interactive (list (read-input-method-name - "Quail input method (default %s): " "Lean"))) + "Quail input method (default %s): " "Lean4"))) (let ((buf (concat "*" qp " input method translations*"))) (with-output-to-temp-buffer buf (with-current-buffer buf @@ -230,7 +233,7 @@ that contains all translations from QP Except for those corresponding to ASCII." (cons 'decode-map (lean4-input-get-translations qp))))))) (defun lean4-input-add-translations (trans) - "Add the given translations TRANS to the Lean input method. + "Add the given translations TRANS to the Lean4 input method. TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The translations are appended to the current translations." (with-temp-buffer @@ -238,13 +241,13 @@ translations are appended to the current translations." (when key (quail-defrule (concat "\\" key) tr - "Lean" t))) + "Lean4" t))) trans))) (defun lean4-input-inherit-package (qp &optional fun) "Inherit translations from the Quail package QP. Add all translations from the Quail package QP (except for those -corresponding to ASCII) to the list of Lean Quail rules. +corresponding to ASCII) to the list of Lean4 Quail rules. The optional function FUN can be used to modify the translations. It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return @@ -254,21 +257,21 @@ a list of such pairs." (if fun (lean4-input-concat-map fun trans) trans)))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Setting up the input method +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Setting up the input method (defvar json-key-type) (declare-function json-read "json") (defun lean4-input-setup () - "Set up the Lean input method. -Use customisable variables and parent input methods to setup Lean input method." - + "Set up the Lean4 input method. +Use customisable variables and parent input methods to setup Lean4 input +method." ;; Create (or reset) the input method. (with-temp-buffer - (quail-define-package "Lean" "UTF-8" "∏" t ; guidance - "Lean input method. -The purpose of this input method is to edit Lean programs, but + (quail-define-package "Lean4" "UTF-8" "∏" t ; guidance + "Lean4 input method. +The purpose of this input method is to edit Lean4 programs, but since it is highly customisable it can be made useful for other tasks as well." nil nil nil nil nil nil t ; maximum-shortest @@ -281,9 +284,10 @@ tasks as well." "abbreviations.json" lean4-input-data-directory)) (thread-last - (let ((json-key-type 'string)) ;; make sure json key is a string. - ;; Prefer emacs native support implemented in C (since 27.1). - ;; Back-up is still useful in case Emacs in not compiled `--with-json`. + (let ((json-key-type 'string)) ;; Make sure json key is string. + ;; Prefer Emacs native support implemented in C (since 27.1). + ;; Back-up is still useful in case Emacs in not compiled + ;; `--with-json'. (if (fboundp 'json-parse-buffer) (json-parse-buffer) (require 'json) @@ -296,50 +300,23 @@ tasks as well." (eval (cdr def))))) (defun lean4-input-incorporate-changed-setting (sym val) - "Update the Lean input method. + "Update the Lean4 input method. Set SYM default value to VAL, then call `lean4-input-setup'. Suitable for use in the :set field of `defcustom'." (set-default sym val) (lean4-input-setup)) ;; Set up the input method. - (cl-eval-when (load eval) (lean4-input-setup)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Export Translations +;; Administrative details -(defun lean4-input-export-translations () - "Export the current translations in a javascript format. -Print (input, output) pairs in Javascript format to the buffer -*lean4-translations*. The output can be copy-pasted to -leanprover.github.io/tutorial/js/input-method.js" +(defun lean4-input-set () (interactive) - (with-current-buffer - (get-buffer-create "*lean4-translations*") - (let ((exclude-list '("\\newline"))) - (insert "var corrections = {") - (--each - (--filter (not (member (car it) exclude-list)) - (lean4-input-get-translations "Lean")) - (let* ((input (substring (car it) 1)) - (outputs (cdr it))) - (insert (format "%s:\"" (prin1-to-string input))) - (cond ((vectorp outputs) - (insert (elt outputs 0))) - (t (insert-char outputs))) - (insert (format "\",\n")))) - (insert "};")))) - -(defun lean4-input-export-translations-to-stdout () - "Print current translations to stdout." - (lean4-input-export-translations) - (with-current-buffer "*lean4-translations*" - (princ (buffer-string)))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details + "Select and activate the `Lean4' input method." + (set-input-method "Lean4")) (provide 'lean4-input) ;;; lean4-input.el ends here diff --git a/lean4-lake.el b/lean4-lake.el deleted file mode 100644 index 125aca1..0000000 --- a/lean4-lake.el +++ /dev/null @@ -1,52 +0,0 @@ -;;; lean4-lake.el --- Lean4-Mode Lake Integration -*- lexical-binding: t; -*- - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library provides integration with Lake, Lean 4 build system and package -;; manager. - -;;; Code: - -(require 'lean4-util) -(require 'lean4-settings) - -(defun lean4-root-dir-p (dir) - "Check if directory DIR contains \"lakefile.lean\" or \"lakefile.toml\"." - (or - (file-exists-p (expand-file-name "lakefile.lean" dir)) - (file-exists-p (expand-file-name "lakefile.toml" dir)))) - -(defun lean4-lake-find-dir () - "Find a parent directory of the current file with a Lake file. - - It looks for files named \"lakefile.lean\" or \"lakefile.toml\" file." - (and (buffer-file-name) - (locate-dominating-file (buffer-file-name) #'lean4-root-dir-p))) - -(defun lean4-lake-find-dir-safe () - "Call `lean4-lake-find-dir', error on failure." - (or (lean4-lake-find-dir) - (error "Cannot find lakefile in any directory above %s" (buffer-file-name)))) - -(defun lean4-lake-build () - "Call lake build." - (interactive) - (let ((default-directory (file-name-as-directory (lean4-lake-find-dir-safe)))) - (compile (concat (lean4-get-executable lean4-lake-name) " build")))) - -(provide 'lean4-lake) -;;; lean4-lake.el ends here diff --git a/lean4-lsp.el b/lean4-lsp.el new file mode 100644 index 0000000..6ffab8a --- /dev/null +++ b/lean4-lsp.el @@ -0,0 +1,105 @@ +;;; lean4-lsp.el --- Lean4 lsp-mode -*- lexical-binding: t; -*- + +;; Copyright (c) 2025 Mekeor Melire + +;; This file is NOT part of GNU Emacs. + +;; Licensed under the Apache License, Version 2.0 (the "License"); you +;; may not use this file except in compliance with the License. You +;; may obtain a copy of the License at +;; +;; http://www.apache.org/licenses/LICENSE-2.0 +;; +;; Unless required by applicable law or agreed to in writing, software +;; distributed under the License is distributed on an "AS IS" BASIS, +;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +;; implied. See the License for the specific language governing +;; permissions and limitations under the License. + +;;; Commentary: + +;; This file defines the `lean4-lsp-mode', a minor mode for +;; `lean4-mode' that appropriately sets up `lsp-mode'. + +;;; Code: + +(require 'compat) ;; for `defvar-keymap' +(require 'lsp-mode) + +(defgroup lean4-lsp nil + "`lsp-mode' for Lean4." + :group 'lean4) + +(defun lean4-lsp-document-reopen () + "Refresh the file dependencies. + +This function restarts the server subprocess for the current +file, recompiling, and reloading all imports." + (interactive) + (lsp-notify + "textDocument/didClose" + `(:textDocument ,(lsp--text-document-identifier))) + (lsp-notify + "textDocument/didOpen" + (list :textDocument + (list :uri (lsp--buffer-uri) + :languageId (lsp-buffer-language) + :version lsp--cur-version + :text (lsp--buffer-content))))) + +(defun lean4-lsp-workspace-add () + "Create an LSP workspace. + +Starting from `(buffer-file-name)`, repeatedly look up the +directory hierarchy for a directory containing a file +\"lean-toolchain\", and use the last such directory found, if any. +This allows us to edit files in child packages using the settings +of the parent project." + (let (root) + (when-let ((file-name (buffer-file-name))) + (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) + ;; We found a toolchain file, but maybe it belongs to a + ;; package. Continue looking until there are no more + ;; toolchain files. + (setq root dir + file-name (file-name-directory (directory-file-name dir))))) + (when root + (lsp-workspace-folders-add root)))) + +(defun lean4-lsp-semantic-tokens-enable () + "Buffer-locally set `lsp-semantic-tokens-enable' to t." + (interactive) + (setq-local lsp-semantic-tokens-enable t)) + +(defcustom lean4-lsp-mode-hook + (list #'lsp + #'lean4-lsp-semantic-tokens-enable + #'lean4-lsp-workspace-add) + "Hook run by `lean4-lsp-mode'." + :options '( lsp + lean4-lsp-semantic-tokens-enable + lean4-lsp-workspace-add) + :type 'hook + :group 'lean4-lsp) + +(defvar-keymap lean4-lsp-mode-map + "C-c C-d" #'lean4-lsp-document-reopen) + +(define-minor-mode lean4-lsp-mode + "Minor mode for `lean4-mode' for using `lsp-mode' as LSP client.") + +;;;; Registration + +(add-to-list 'lsp-language-id-configuration + '(lean4-mode . "lean4")) + +(lsp-register-client + (make-lsp-client :new-connection (lsp-stdio-connection '("lake" "serve")) + :major-modes '(lean4-mode) + :language-id "lean4" + :server-id 'lean4-lsp + :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) + :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) + +(provide 'lean4-lsp) +;;; lean4-lsp.el ends here diff --git a/lean4-markdown.el b/lean4-markdown.el new file mode 100644 index 0000000..6fb5fc8 --- /dev/null +++ b/lean4-markdown.el @@ -0,0 +1,32 @@ +;;; lean4-markdown.el --- Lean4 markdown -*- lexical-binding: t; -*- + +;; Copyright (c) 2025 Mekeor Melire + +;; This file is NOT part of GNU Emacs. + +;; Licensed under the Apache License, Version 2.0 (the "License"); you +;; may not use this file except in compliance with the License. You +;; may obtain a copy of the License at +;; +;; http://www.apache.org/licenses/LICENSE-2.0 +;; +;; Unless required by applicable law or agreed to in writing, software +;; distributed under the License is distributed on an "AS IS" BASIS, +;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +;; implied. See the License for the specific language governing +;; permissions and limitations under the License. + +;;; Commentary: + +;; This file mutates `markdown-code-lang-modes' so that +;; `markdown-mode' supports Lean4 code blocks. + +;;; Code: + +(require 'markdown-mode) + +(add-to-list 'markdown-code-lang-modes + '("lean4" . lean4-mode)) + +(provide 'lean4-markdown) +;;; lean4-markdown.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 3994c99..d156cd4 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -1,7 +1,7 @@ -;;; lean4-mode.el --- Major mode for Lean language -*- lexical-binding: t; -*- +;;; lean4-mode.el --- Lean4 major mode -*- lexical-binding: t; -*- -;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. -;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved. +;; Copyright (c) 2013, 2014 Microsoft Corporation +;; Copyright (c) 2014, 2015 Soonho Kong ;; Author: Leonardo de Moura ;; Soonho Kong @@ -15,7 +15,7 @@ ;; SPDX-License-Identifier: Apache-2.0 ;; Version: 1.1.2 -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -31,270 +31,108 @@ ;;; Commentary: -;; Provides a major mode for the Lean programming language. - -;; Provides highlighting, diagnostics, goal visualization, -;; and many other useful features for Lean users. - -;; See the README.md for more advanced features and the -;; associated keybindings. +;; Lean4-Mode is a package providing an equally named major mode for +;; Lean version 4, a programming language and theorem prover. Consult +;; the readme or equivalent manual for further information. ;;; Code: (require 'cl-lib) -(require 'dash) (require 'pcase) -(require 'lsp-mode) + +(require 'dash) + (require 'lean4-eri) -(require 'lean4-util) -(require 'lean4-settings) -(require 'lean4-syntax) -(require 'lean4-info) (require 'lean4-fringe) -(require 'lean4-lake) +(require 'lean4-info) +(require 'lean4-input) +(require 'lean4-lsp) +(require 'lean4-markdown) +(require 'lean4-syntax) -;; Declare symbols defined in external dependencies. This silences -;; byte-compiler warnings: +;; Suppress byte-compiler warnings: (defvar compilation-mode-font-lock-keywords) -(defvar flycheck-after-syntax-check-hook) -(defvar flycheck-disabled-checkers) -(defvar flycheck-mode) -(defvar lsp--cur-version) -(defvar markdown-code-lang-modes) -(declare-function flycheck-list-errors "ext:flycheck") -(declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") -(declare-function lean-mode "ext:lean-mode") (declare-function quail-show-key "quail") -(defun lean4-compile-string (lake-name exe-name args file-name) - "Command to run EXE-NAME with extra ARGS and FILE-NAME. -If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command -\"EXE-NAME ARGS FILE-NAME\"." - (if lake-name - (format "%s env %s %s %s" lake-name exe-name args file-name) - (format "%s %s %s" exe-name args file-name))) - -(defun lean4-create-temp-in-system-tempdir (file-name prefix) - "Create a temp lean file and return its name. -The new file has prefix PREFIX (defaults to `flymake') and the same extension as -FILE-NAME." - (make-temp-file (or prefix "flymake") nil (file-name-extension file-name))) - -(defun lean4-execute (&optional arg) - "Execute Lean in the current buffer with an optional argument ARG." - (interactive) - (when (called-interactively-p 'any) - (setq arg (read-string "arg: " arg))) - (let* ((cc compile-command) - (dd default-directory) - (use-lake (lean4-lake-find-dir)) - (default-directory (if use-lake (lean4-lake-find-dir) dd)) - (target-file-name - (or - (buffer-file-name) - (flymake-proc-init-create-temp-buffer-copy 'lean4-create-temp-in-system-tempdir)))) - (compile (lean4-compile-string - (if use-lake (shell-quote-argument (expand-file-name (lean4-get-executable lean4-lake-name))) nil) - (shell-quote-argument (expand-file-name (lean4-get-executable lean4-executable-name))) - (or arg "") - (shell-quote-argument (expand-file-name target-file-name)))) - ;; restore old value - (setq compile-command cc) - (setq default-directory dd))) - -(defun lean4-std-exe () - "Execute Lean in the current buffer." +(defgroup lean4 nil + "Major mode for Lean4 programming language and theorem prover." + :group 'languages + :link '(info-link :tag "Info Manual" "(lean4-mode)") + :link '(url-link + :tag "Website" + "https://github.com/leanprover-community/lean4-mode") + :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") + :prefix "lean4-") + +(defcustom lean4-mode-hook (list #'lean4-input-set #'lean4-lsp-mode) + "Hook run after entering `lean4-mode'." + :options '(flycheck-mode lean4-input-set lean4-lsp-mode) + :type 'hook + :group 'lean4) + +(defcustom lean4-location-root nil + "Lean4 project root, used as `default-directory'." + :type 'directory + :group 'lean4) + +(defun lean4-execute () + "Execute Lean4 in the current buffer." (interactive) - (lean4-execute)) - -(defun lean4-refresh-file-dependencies () - "Refresh the file dependencies. - -This function restarts the server subprocess for the current -file, recompiling, and reloading all imports." - (interactive) - (lsp-notify - "textDocument/didClose" - `(:textDocument ,(lsp--text-document-identifier))) - (lsp-notify - "textDocument/didOpen" - (list :textDocument - (list :uri (lsp--buffer-uri) - :languageId (lsp-buffer-language) - :version lsp--cur-version - :text (lsp--buffer-content))))) - -(defun lean4-tab-indent () - "Lean 4 function for TAB indent." + (let* ((default-directory + (or lean4-location-root default-directory))) + (compile (if-let* ((file (buffer-file-name))) + (concat "lean " file " ") + "lean ")))) + +(defun lean4-lake-build () + "Build Lean4 project with Lake." (interactive) - (cond ((looking-back (rx line-start (* white)) nil) - (lean4-eri-indent)) - (t (indent-for-tab-command)))) - -(defun lean4-set-keys () - "Setup Lean 4 keybindings." - (local-set-key lean4-keybinding-std-exe1 #'lean4-std-exe) - (local-set-key lean4-keybinding-std-exe2 #'lean4-std-exe) - (local-set-key lean4-keybinding-show-key #'quail-show-key) - (local-set-key lean4-keybinding-tab-indent #'lean4-tab-indent) - ;; (local-set-key lean4-keybinding-hole #'lean4-hole) - (local-set-key lean4-keybinding-lean4-toggle-info #'lean4-toggle-info) - ;; (local-set-key lean4-keybinding-lean4-message-boxes-toggle #'lean4-message-boxes-toggle) - (local-set-key lean4-keybinding-lake-build #'lean4-lake-build) - (local-set-key lean4-keybinding-refresh-file-dependencies #'lean4-refresh-file-dependencies) - ;; This only works as a mouse binding due to the event, so it is not abstracted - ;; to avoid user confusion. - ;; (local-set-key (kbd "") #'lean4-right-click-show-menu) - ) - -(define-abbrev-table 'lean4-abbrev-table - '()) - -(defvar lean4-mode-map (make-sparse-keymap) - "Keymap used in Lean mode.") + (let* ((default-directory + (or lean4-location-root default-directory))) + (compile "lake build "))) + +(defvar-keymap lean4-mode-map + :doc "Keymap for `lean4-mode'." + "C-c C-x" #'lean4-execute + "C-c C-l" #'lean4-execute + "C-c C-k" #'quail-show-key + "TAB" #'lean4-eri-tab + "C-c C-i" #'lean4-info-mode + "C-c C-p C-l" #'lean4-lake-build) (easy-menu-define lean4-mode-menu lean4-mode-map - "Menu for the Lean major mode." - `("Lean 4" - ["Execute lean" lean4-execute t] - ["Toggle info display" lean4-toggle-info t] - ;; TODO: Bug#91: We offers a Flycheck-based menu-item when - ;; Flycheck is in use. Users who use built-in Flymake should also - ;; be offered a working menu-item. Alternatively, the menu-item - ;; could also be dropped for both cases. - ["List of errors" flycheck-list-errors flycheck-mode] - ["Restart lean process" lsp-workspace-restart t] - ["Customize lean4-mode" (customize-group 'lean) t])) - -(defconst lean4-hooks-alist - '( - ;; Handle events that may start automatic syntax checks - (before-save-hook . lean4-whitespace-cleanup) - ;; info view - ;; update errors immediately, but delay querying goal - (flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay-debounced) - (post-command-hook . lean4-info-buffer-redisplay-debounced) - (lsp-on-idle-hook . lean4-info-buffer-refresh)) - "Hooks which lean4-mode needs to hook in. - -The `car' of each pair is a hook variable, the `cdr' a function -to be added or removed from the hook variable if Flycheck mode is -enabled and disabled respectively.") - -(defun lean4-mode-setup () - "Default lean4-mode setup." - ;; Right click menu sources - ;;(setq lean4-right-click-item-functions '(lean4-info-right-click-find-definition - ;; lean4-hole-right-click)) - ;; Flycheck - (setq-local flycheck-disabled-checkers '()) - ;; Lean massively benefits from semantic tokens, so change default to enabled - (setq-local lsp-semantic-tokens-enable t) - (lean4-create-lsp-workspace)) - -(defun lean4-create-lsp-workspace () - "Create an LSP workspace. - -Starting from `(buffer-file-name)`, repeatedly look up the -directory hierarchy for a directory containing a file -\"lean-toolchain\", and use the last such directory found, if any. -This allows us to edit files in child packages using the settings -of the parent project." - (let (root) - (when-let ((file-name (buffer-file-name))) - (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) - ;; We found a toolchain file, but maybe it belongs to a package. - ;; Continue looking until there are no more toolchain files. - (setq root dir - file-name (file-name-directory (directory-file-name dir))))) - (when root - (lsp-workspace-folders-add root)))) + "Menu for the Lean4 major mode." + `("Lean4" + ["Execute Lean4" lean4-execute t] + ["Toggle Info" lean4-info-mode t] + ["Customize" (customize-group 'lean) t])) ;;;###autoload -(define-derived-mode lean4-mode prog-mode "Lean 4" - "Major mode for Lean language. +(define-derived-mode lean4-mode prog-mode "Lean4" + "Major mode for Lean4 language. \\{lean4-mode-map}" :syntax-table lean4-syntax-table - :abbrev-table lean4-abbrev-table :group 'lean4 - (set (make-local-variable 'comment-start) "--") - (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*") - (set (make-local-variable 'comment-end) "") - (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)") - (set (make-local-variable 'comment-padding) 1) - (set (make-local-variable 'comment-use-syntax) t) - (set (make-local-variable 'font-lock-defaults) lean4-font-lock-defaults) - (set (make-local-variable 'indent-tabs-mode) nil) - (set 'compilation-mode-font-lock-keywords '()) - (require 'lean4-input) - (set-input-method "Lean") - (set (make-local-variable 'lisp-indent-function) - 'common-lisp-indent-function) - (lean4-set-keys) + (setq-local comment-end "") + (setq-local comment-end-skip "[ \t]*\\(-/\\|\\s>\\)") + (setq-local comment-padding 1) + (setq-local comment-start "--") + (setq-local comment-start-skip "[-/]-[ \t]*") + (setq-local comment-use-syntax t) + (setq-local font-lock-defaults lean4-font-lock-defaults) + (setq-local indent-tabs-mode nil) + (setq-local lisp-indent-function 'common-lisp-indent-function) + (lean4-input-set) (if (fboundp 'electric-indent-local-mode) - (electric-indent-local-mode -1)) - ;; (abbrev-mode 1) - (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist) - (add-hook hook fn nil 'local)) - (lean4-mode-setup)) - -(defun lean4--version () - "Return Lean version as a list `(MAJOR MINOR PATCH)'." - (with-temp-buffer - (call-process (lean4-get-executable "lean") nil (list t nil) nil "-v") - (goto-char (point-min)) - (re-search-forward (rx bol "Lean (version " (group (+ digit) (+ "." (+ digit))))) - (version-to-list (match-string 1)))) + (electric-indent-local-mode -1))) -(defun lean4-show-version () - "Print Lean 4 version." - (interactive) - (message "Lean %s" (mapconcat #'number-to-string (lean4--version) "."))) - -;;;###autoload -(defun lean4-select-mode () - "Automatically select mode (Lean 3 vs Lean 4)." - (if (and lean4-autodetect-lean3 - (eq 3 (car (lean4--version)))) - (lean-mode) - (lean4-mode))) - -;; Automatically use lean4-mode for .lean files. ;;;###autoload (add-to-list 'auto-mode-alist - '("\\.lean\\'" . lean4-select-mode)) + '("\\.lean\\'" . lean4-mode)) ;;;###autoload -(with-eval-after-load 'markdown-mode - (add-to-list 'markdown-code-lang-modes - '("lean" . lean4-select-mode))) - -;; Use utf-8 encoding -;;;### autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) -;; LSP init -;; Ref: https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/ -(add-to-list 'lsp-language-id-configuration - '(lean4-mode . "lean")) - -(defun lean4--server-cmd () - "Return Lean server command. -If found lake version at least 3.1.0, then return '/path/to/lake serve', -otherwise return '/path/to/lean --server'." - (condition-case nil - (if (string-version-lessp (car (process-lines (lean4-get-executable "lake") "--version")) "3.1.0") - `(,(lean4-get-executable lean4-executable-name) "--server") - `(,(lean4-get-executable "lake") "serve")) - (error `(,(lean4-get-executable lean4-executable-name) "--server")))) - -(lsp-register-client - (make-lsp-client :new-connection (lsp-stdio-connection #'lean4--server-cmd) - :major-modes '(lean4-mode) - :server-id 'lean4-lsp - :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) - :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) - (provide 'lean4-mode) ;;; lean4-mode.el ends here diff --git a/lean4-mode.info b/lean4-mode.info index 41a8f4c..f327c07 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -3,28 +3,24 @@ lean4-mode.texi. INFO-DIR-SECTION Emacs misc features START-INFO-DIR-ENTRY -* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language. +* Lean4-Mode: (lean4-mode). Emacs major mode for Lean4 language. END-INFO-DIR-ENTRY  File: lean4-mode.info, Node: Top, Next: Installation, Up: (dir) -Lean4-Mode - Emacs major mode for Lean language -*********************************************** +Emacs Lean4-Mode +**************** This package extends GNU Emacs (https://www.gnu.org/software/emacs/) by -providing a major mode for editing code written in version 4 of the -programming language and theorem prover Lean (https://lean-lang.org). +a major mode for Lean (https://lean-lang.org) version 4, a programming +language and theorem prover. - The Lean4-Mode source code is developed at Github -(https://github.com/leanprover-community/lean4-mode) and its issues -tracked there too. Further discussions and question-answering takes -place in the #Emacs channel -(https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs) of -Lean's Zulip chat. - - For legacy version 3 of Lean, use the archived Lean3-Mode -(https://github.com/leanprover/lean3-mode) (also known as _Lean-Mode_). + Lean4-Mode is developed on Github +(https://github.com/leanprover-community/lean4-mode). Bugs and feature +requests are also tracked there. Further discussions take place in the +#Emacs (https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs) +channel on the Lean Zulip chat platform. * Menu: @@ -32,19 +28,21 @@ Lean's Zulip chat. * Usage:: * Configuration:: * Common Pitfalls:: +* Changelog:: +* Contributing:: -- The Detailed Node Listing -- Installation -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: Instructions for Source-Based Use-Package * Native vc (Emacs 30 or later):: -* Doom-Emacs:: +* Doom package!:: * Straight:: Usage @@ -57,6 +55,20 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Common Pitfalls + +* Coexistence with Lean3-Mode:: +* Partial value of lean4-mode-hook or other hook variables:: + +Changelog + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. +  File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top @@ -66,15 +78,15 @@ File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top * Menu: -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package::  -File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed and Concrete Instructions, Up: Installation +File: lean4-mode.info, Node: Brief Generic Instructions, Next: Detailed Native Instructions, Up: Installation -1.1 Brief and Generic Instructions -================================== +1.1 Brief, Generic Instructions +=============================== First, install the dependencies of Lean4-Mode: • Lean (https://lean-lang.org/lean4/doc/setup.html) (version 4) @@ -84,19 +96,29 @@ First, install the dependencies of Lean4-Mode: Magit-Section (https://github.com/magit/magit/blob/main/lisp/magit-section.el) (available on Melpa) + Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: - • Clone the Git repository of Lean4-Mode + • Clone the Git repository (https://github.com/leanprover-community/lean4-mode). • In your Emacs initialization file (https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html), - add the path to that local repository to the ‘load-path’ list. + add the path to your local repository to ‘load-path’. + + Third, ensure Lean4-Mode is loaded by one of the following ways: + • Load it eagerly. + • Load it lazily by associating ‘lean4-mode’ with the ‘.lean’ file + extension and setting it up as autoloaded command. + • Load it lazily by generating an autoload file (with the Make target + called ‘autoload’) and loading that in your init file. Make sure + to regenerate the autoload file, whenever you change the Lean4-Mode + repository (e.g. ‘git pull’).  -File: lean4-mode.info, Node: Detailed and Concrete Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief and Generic Instructions, Up: Installation +File: lean4-mode.info, Node: Detailed Native Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief Generic Instructions, Up: Installation -1.2 Detailed and Concrete Instructions -====================================== +1.2 Detailed, Native Instructions +================================= Install Lean version 4. @@ -130,41 +152,73 @@ approach, add the following to your Emacs initialization file (e.g. Lean4-Mode repository to the ‘load-path’ list: (add-to-list 'load-path "~/path/to/lean4-mode") - Lean4-Mode should now already be enabled when you open a file with -‘.lean’ extension. But you can optionally also already load Lean4-Mode -on Emacs startup, e.g. in order to customize variables: + Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + + If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: (require 'lean4-mode) + If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 +source file is opened the first time, put in your init file: + (autoload 'lean4-mode "lean4-mode" nil t) + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) + + If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your Git +repository changes (e.g. ‘git pull’), run ‘make autoload’ inside. And +put this in your init file: + (require 'lean4-mode-autoloads) +  -File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed and Concrete Instructions, Up: Installation +File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed Native Instructions, Up: Installation 1.3 Instructions for Source-Based Use-Package ============================================= -If you use a source-based package-manager (e.g. ‘package-vc.el’, +This section instructs how to set up Lean4-Mode through the +‘use-package’ macro that is built into Emacs since version 29. + + If you use a source-based package-manager (e.g. ‘package-vc.el’, Straight or Elpaca), then make sure to list the ‘"data"’ directory in your Lean4-Mode package recipe. - If you use the ‘use-package’ macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure to -specify ‘lean4-mode’ as a ‘:command’. + When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like ‘lean4-mode-hook’ have non-nil initialization values. +And since ‘use-package’ applies the ‘:hook’ specifications before +package loading, you should avoid it. Instead, put ‘(add-hook +'lean4-...-hook #'...)’ under the ‘:config’ section. (See _Common +Pitfalls_ section below.) + + Use-Package involves +(https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html) +some complexity when it comes to deciding whether to load a package +eagerly (_demand_) or lazily (_defer_). For example, it depends on your +configuration (e.g. ‘use-package-always-defer’, +‘use-package-always-demand’). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via ‘:demand t’. Alternatively, +you can defer loading e.g. via ‘:defer t’ together with ‘:mode +"\\.lean\\'"’ (which associates Lean4-Mode with the ‘.lean’ file +extension) and ‘:commands lean4-mode’ (which will set up autoloading). Following subsections show concrete examples. * Menu: * Native vc (Emacs 30 or later):: -* Doom-Emacs:: +* Doom package!:: * Straight::  -File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom-Emacs, Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom package!, Up: Instructions for Source-Based Use-Package 1.3.1 Native ‘:vc’ (Emacs 30 or later) -------------------------------------- -GNU Emacs comes with ‘use-package.el’ built-in since version 29. And -since version 30, it also comes with a built-in ‘:vc’ keyword for the +Since version 30, Emacs comes with a built-in ‘:vc’ keyword for the ‘use-package’ macro that utilizes ‘package-vc.el’ to install Emacs packages from remote source repositories. @@ -175,28 +229,29 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :mode "\\.lean\\'" + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + ))  -File: lean4-mode.info, Node: Doom-Emacs, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Doom package!, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package -1.3.2 Doom-Emacs ----------------- +1.3.2 Doom ‘package!’ +--------------------- If you use Doom-Emacs, you can place the following code in your Doom initialization file: (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data")))  -File: lean4-mode.info, Node: Straight, Prev: Doom-Emacs, Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Straight, Prev: Doom package!, Up: Instructions for Source-Based Use-Package 1.3.3 Straight -------------- @@ -206,6 +261,7 @@ the following code in your Emacs initialization file: (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) @@ -216,23 +272,23 @@ File: lean4-mode.info, Node: Usage, Next: Configuration, Prev: Installation, 2 Usage ******* -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with ‘.lean’ extension. Emacs will ask you to identify the _project_ this file belongs to. If you then type ‘#check id’, the word ‘#check’ will be underlined, and hovering over it will show you the type of ‘id’. - To view the proof state, run ‘lean4-toggle-info’ (‘C-c C-i’). This -will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in + To view the proof state, run ‘lean4-info-mode’ (‘C-c C-i’). This +will display the ‘*Lean4 Info*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. Key Description Command ----------------------------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------------- ‘C-c C-k’ Echo the keystroke needed to input the symbol at point ‘quail-show-key’ -‘C-c C-d’ Recompile and reload imports ‘lean4-refresh-file-dependencies’ -‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-std-exe’ +‘C-c C-d’ Recompile and reload imports ‘lean4-lsp-document-reopen’ +‘C-c C-x’ or ‘C-c C-l’ Execute Lean4 in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ -‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’ +‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-info-mode’ * Menu: @@ -300,37 +356,247 @@ installed, then customize the ‘lsp-diagnostics-provider’ user option accordingly.  -File: lean4-mode.info, Node: Common Pitfalls, Prev: Configuration, Up: Top +File: lean4-mode.info, Node: Common Pitfalls, Next: Changelog, Prev: Configuration, Up: Top 4 Common Pitfalls ***************** -Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, -use Lean3-Mode (https://github.com/leanprover/lean3-mode), which is also -known as Lean-Mode due to historical reasons. In principle, it is fine -to have both Lean3-Mode and Lean4-Mode installed at the same time. But -note that Lean3-Mode uses the prefix ‘lean-’ for its symbols. E.g. you -should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as -major mode. +* Menu: + +* Coexistence with Lean3-Mode:: +* Partial value of lean4-mode-hook or other hook variables:: + + +File: lean4-mode.info, Node: Coexistence with Lean3-Mode, Next: Partial value of lean4-mode-hook or other hook variables, Up: Common Pitfalls + +4.1 Coexistence with Lean3-Mode +=============================== + +Lean4-Mode only supports version 4 of Lean. For editing code written in +deprecated version 3, use Lean3-Mode +(https://github.com/leanprover/lean3-mode). It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + + • Lean3-Mode uses ‘lean-’ as prefix (e.g. for commands) whereas + Lean4-Mode uses ‘lean4-’ as prefix. When Lean4-Mode is active, you + must not use commands with prefix ‘lean-’. + + • Both packages associate the ‘.lean’ file extension with their + respective commands. Even more confusingly, they use different + functions and regular expressions to do so. + + Lean3-Mode: + ;;;###autoload + (push '("\\.lean$" . lean-mode) auto-mode-alist) + + Lean4-Mode: + ;;;###autoload + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) + + Make sure that both packages are loaded, autoloaded and configured + in such a way ‘auto-mode-alist’ ends up with your desired value. + + • In particular, if you want Emacs to automatically detect whether + Lean3- or Lean4-Mode should be used for a particular file or + project, you'll need to define your own Elisp function and + associate it with the Lean file extension. If desired, you can + even do this directory locally (via the special "variable" ‘eval’ + in ‘.dir-locals.el’). + + +File: lean4-mode.info, Node: Partial value of lean4-mode-hook or other hook variables, Prev: Coexistence with Lean3-Mode, Up: Common Pitfalls + +4.2 Partial value of ‘lean4-mode-hook’ or other hook variables +============================================================== + +If you customize a hook variable like ‘lean4-mode-hook’ e.g. with +‘add-hook’ or Use-Package's ‘:hook’ keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +‘lean4-mode-hook’ may not contain the ‘lsp’ command and as a consequence +‘lsp-mode’ won't start automatically together with Lean4-Mode. + + There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your ‘add-hook’ form before it loads +the definition of the hook from Lean4-Mode package. (3.) ‘add-hook’ +effectively initializes the passed hook-variable to nil when the symbol +has no value cell. And (4.), Use-Package applies passed ‘:hook’ +specifications before package loading. + + If you do not use Use-Package, the solution is to load Lean4-Mode +before calling ‘add-hook’, e.g. with ‘require’: + (require 'lean4-mode) + (add-hook 'lean4-...-hook #'...) + + Or with ‘with-eval-after-load’: + (with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) + (with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) + + If you do Use-Package, you can solve the problem by calling +‘add-hook’ within the ‘:config’ section: + (use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) + + +File: lean4-mode.info, Node: Changelog, Next: Contributing, Prev: Common Pitfalls, Up: Top + +5 Changelog +*********** + +* Menu: + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. + + +File: lean4-mode.info, Node: Upcoming Version, Next: Version 112 from 2024-12-10, Up: Changelog + +5.1 Upcoming Version +==================== + +Documentation: + • The changelog is now part of the readme (and thus of the Info + manual). + + User interface: + • The tool-bar menu of Lean4-Mode does not list the + ‘flycheck-list-errors’ anymore. Please use the “Show all errors” + entry in Flycheck's menu instead. (Fixes #91 + (https://github.com/leanprover-community/lean4-mode/issues/91).) + + Features: + • The variable ‘lean4-delete-trailing-whitespace’ has been removed + together with related code. Instead of reinventing the wheel, + Lean4-Mode demands users to use Emacs' built-in facilities for this + kind of use case. For example, you might want to define a function + that buffer-locally adds ‘delete-trailing-whitespace’ to + ‘before-save-hook’, and add that hereby defined function to + ‘lean4-mode-hook’. + • The variable ‘lean4-autodetect-lean3’ has been removed along with + the command ‘lean4-select-mode’ and related code. If you still use + legacy version 3 of Lean for some files or projects, you could + directory- or file-locally associate the ‘.lean’ file extension + with Lean3-Mode in ‘auto-mode-alist’. + • The command ‘lean4-show-version’ has been removed. Lean4-Mode now + assumes Lean version 4. In order to determine the minor version, + you may type ‘M-! lean --version RET’ or similar. + • The functions ‘lean4-input-export-translations’ and + ‘lean4-input-export-translations-to-stdout’ have been removed. We + expect that noone has been using it. If you do use it, let us + know, so we can reconsider our decision in case of a substantial + amount of users. Otherwise, please just define these functions in + your Emacs initialization file yourself. + • The command ‘lean4-std-exe’ has been removed. It was just the same + as ‘lean4-execute’ which continues to exist. + + +File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog + +5.2 Version 1.1.2 from 2024-12-10 +================================= + + • Fix occasional errors like "The connected server(s) does not + support method ‘$/lean/plainGoal’" by not wrapping invocations of + ‘lsp-protocol’ macro into ‘eval-when-compile’ but rather into + ‘eval-and-compile’. Thus, the methods should now work, no matter + whether Lean4-Mode was loaded by interpreting ‘.el’ Elisp code or + by loading compiled ‘.elc’ or ‘.eln’ files. (Bug#54 + (https://github.com/leanprover-community/lean4-mode/issues/54), + Zulip discussion + (https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table)) + + +File: lean4-mode.info, Node: Version 111 from 2024-12-02, Next: Version 110 from 2024-12-01, Prev: Version 112 from 2024-12-10, Up: Changelog + +5.3 Version 1.1.1 from 2024-12-02 +================================= + + • Assign all customizable user-options to the Lean4-Mode specific + ‘lean4’ group. To customize Lean4-Mode, you now need to type ‘M-x + customize-group RET lean4 RET’. + + +File: lean4-mode.info, Node: Version 110 from 2024-12-01, Next: Version 101 from 2024-11-21, Prev: Version 111 from 2024-12-02, Up: Changelog + +5.4 Version 1.1.0 from 2024-12-01 +================================= + + • To ‘lean4’ customization group, add link to local info manual and + use Lean4-Mode Github URL as website. + • Introduce new dependency on Elpa package ‘compat’. + • Remove dependency on Elpa package Flycheck. It is still supported + but not required. + + +File: lean4-mode.info, Node: Version 101 from 2024-11-21, Next: Version 10 from 2024-11-16, Prev: Version 110 from 2024-12-01, Up: Changelog + +5.5 Version 1.0.1 from 2024-11-21 +================================= + + • Specify Yury G. Kudryashov as maintainer. + • Rework README. (Now in Org format). + • Provide README as Texi and Info manual too. + + +File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 from 2024-11-21, Up: Changelog + +5.6 Version 1.0 from 2024-11-16 +=============================== + + • Specify "Version" in Emacs-Lisp library header. + + +File: lean4-mode.info, Node: Contributing, Prev: Changelog, Up: Top + +6 Contributing +************** + +When you contribute to Lean4-Mode, add a personal copyright like ‘;; +Copyright (c) 2024 Firstname Lastname’ to the header of respective +files. + + You can use Emacs' built-in ‘bug-reference-mode’ and +‘bug-reference-prog-mode’ in this repository to make mentions of issues +like ‘#123’ clickable.  Tag Table: -Node: Top223 -Node: Installation1492 -Node: Brief and Generic Instructions1735 -Node: Detailed and Concrete Instructions2684 -Node: Instructions for Source-Based Use-Package4341 -Node: Native vc (Emacs 30 or later)5062 -Node: Doom-Emacs5970 -Node: Straight6396 -Node: Usage6896 -Node: lsp-mode8342 -Node: Flycheck8627 -Node: Configuration9237 -Node: lsp-mode (1)9427 -Node: Flycheck (1)9696 -Node: Common Pitfalls10181 +Node: Top224 +Node: Installation1781 +Node: Brief Generic Instructions2072 +Node: Detailed Native Instructions3528 +Node: Instructions for Source-Based Use-Package5678 +Node: Native vc (Emacs 30 or later)7594 +Node: Doom package!8460 +Node: Straight8930 +Node: Usage9459 +Node: lsp-mode10881 +Node: Flycheck11166 +Node: Configuration11776 +Node: lsp-mode (1)11966 +Node: Flycheck (1)12235 +Node: Common Pitfalls12720 +Node: Coexistence with Lean3-Mode12959 +Node: Partial value of lean4-mode-hook or other hook variables14681 +Node: Changelog16402 +Node: Upcoming Version16863 +Node: Version 112 from 2024-12-1018929 +Node: Version 111 from 2024-12-0219794 +Node: Version 110 from 2024-12-0120201 +Node: Version 101 from 2024-11-2120699 +Node: Version 10 from 2024-11-1621062 +Node: Contributing21295  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index fd205bf..00968f1 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -1,37 +1,33 @@ \input texinfo @c -*- texinfo -*- @c %**start of header @setfilename lean4-mode.info -@settitle Lean4-Mode - Emacs major mode for Lean language +@settitle Emacs Lean4-Mode @documentencoding UTF-8 @documentlanguage en @c %**end of header @dircategory Emacs misc features @direntry -* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language. +* Lean4-Mode: (lean4-mode). Emacs major mode for Lean4 language. @end direntry @finalout @titlepage -@title Lean4-Mode - Emacs major mode for Lean language +@title Emacs Lean4-Mode @end titlepage @contents @ifnottex @node Top -@top Lean4-Mode - Emacs major mode for Lean language +@top Emacs Lean4-Mode -This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by providing a major mode for editing -code written in version 4 of the programming language and theorem -prover @uref{https://lean-lang.org, Lean}. +This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by a major mode for @uref{https://lean-lang.org, Lean} version 4, a +programming language and theorem prover. -The Lean4-Mode source code is developed at @uref{https://github.com/leanprover-community/lean4-mode, Github} and its issues -tracked there too. Further discussions and question-answering takes -place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs channel} of Lean's Zulip chat. - -For legacy version 3 of Lean, use the archived @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode} (also known -as @emph{Lean-Mode}). +Lean4-Mode is developed on @uref{https://github.com/leanprover-community/lean4-mode, Github}. Bugs and feature requests are also +tracked there. Further discussions take place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs} channel +on the Lean Zulip chat platform. @end ifnottex @@ -40,20 +36,22 @@ as @emph{Lean-Mode}). * Usage:: * Configuration:: * Common Pitfalls:: +* Changelog:: +* Contributing:: @detailmenu --- The Detailed Node Listing --- Installation -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: Instructions for Source-Based Use-Package * Native @samp{vc} (Emacs 30 or later):: -* Doom-Emacs:: +* Doom @code{package!}:: * Straight:: Usage @@ -66,6 +64,20 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Common Pitfalls + +* Coexistence with Lean3-Mode:: +* Partial value of @code{lean4-mode-hook} or other hook variables:: + +Changelog + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. + @end detailmenu @end menu @@ -73,13 +85,13 @@ Configuration @chapter Installation @menu -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: @end menu -@node Brief and Generic Instructions -@section Brief and Generic Instructions +@node Brief Generic Instructions +@section Brief, Generic Instructions First, install the dependencies of Lean4-Mode: @itemize @@ -91,18 +103,33 @@ Emacs (version 27 or later) Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (available on GNU-Elpa), @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (available on Melpa) @end itemize +Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: @itemize @item -Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository of Lean4-Mode}. +Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository}. @item -In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to that local -repository to the @code{load-path} list. +In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to your local +repository to @code{load-path}. @end itemize -@node Detailed and Concrete Instructions -@section Detailed and Concrete Instructions +Third, ensure Lean4-Mode is loaded by one of the following ways: +@itemize +@item +Load it eagerly. +@item +Load it lazily by associating @code{lean4-mode} with the @samp{.lean} file +extension and setting it up as autoloaded command. +@item +Load it lazily by generating an autoload file (with the Make target +called @samp{autoload}) and loading that in your init file. Make sure to +regenerate the autoload file, whenever you change the Lean4-Mode +repository (e.g. @samp{git pull}). +@end itemize + +@node Detailed Native Instructions +@section Detailed, Native Instructions Install Lean version 4. @@ -141,37 +168,72 @@ Lean4-Mode repository to the @code{load-path} list: (add-to-list 'load-path "~/path/to/lean4-mode") @end lisp -Lean4-Mode should now already be enabled when you open a file with -@samp{.lean} extension. But you can optionally also already load -Lean4-Mode on Emacs startup, e.g. in order to customize variables: +Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + +If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: @lisp (require 'lean4-mode) @end lisp +If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 source +file is opened the first time, put in your init file: +@lisp +(autoload 'lean4-mode "lean4-mode" nil t) +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) +@end lisp + +If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your +Git repository changes (e.g. @samp{git pull}), run @samp{make autoload} +inside. And put this in your init file: +@lisp +(require 'lean4-mode-autoloads) +@end lisp + @node Instructions for Source-Based Use-Package @section Instructions for Source-Based Use-Package +This section instructs how to set up Lean4-Mode through the +@code{use-package} macro that is built into Emacs since version 29. + If you use a source-based package-manager (e.g. @samp{package-vc.el}, Straight or Elpaca), then make sure to list the @samp{"data"} directory in your Lean4-Mode package recipe. -If you use the @code{use-package} macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure -to specify @code{lean4-mode} as a @samp{:command}. +When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like @code{lean4-mode-hook} have non-nil initialization +values. And since @code{use-package} applies the @samp{:hook} specifications +before package loading, you should avoid it. Instead, put +@samp{(add-hook 'lean4-...-hook #'...)} under the @samp{:config} section. (See +@emph{Common Pitfalls} section below.) + +Use-Package @uref{https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html, involves} some complexity when it comes to deciding whether +to load a package eagerly (@emph{demand}) or lazily (@emph{defer}). For example, +it depends on your configuration (e.g. @code{use-package-always-defer}, +@code{use-package-always-demand}). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via @samp{:demand t}. Alternatively, +you can defer loading e.g. via @samp{:defer t} together with +@samp{:mode "\\.lean\\'"} (which associates Lean4-Mode with the @samp{.lean} +file extension) and @samp{:commands lean4-mode} (which will set up +autoloading). Following subsections show concrete examples. @menu * Native @samp{vc} (Emacs 30 or later):: -* Doom-Emacs:: +* Doom @code{package!}:: * Straight:: @end menu @node Native @samp{vc} (Emacs 30 or later) @subsection Native @samp{:vc} (Emacs 30 or later) -GNU Emacs comes with @samp{use-package.el} built-in since version 29. And -since version 30, it also comes with a built-in @samp{:vc} keyword for the +Since version 30, Emacs comes with a built-in @samp{:vc} keyword for the @code{use-package} macro that utilizes @samp{package-vc.el} to install Emacs packages from remote source repositories. @@ -183,24 +245,25 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :mode "\\.lean\\'" + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) @end lisp -@node Doom-Emacs -@subsection Doom-Emacs +@node Doom @code{package!} +@subsection Doom @code{package!} If you use Doom-Emacs, you can place the following code in your Doom initialization file: @lisp (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) @end lisp @node Straight @@ -212,6 +275,7 @@ place the following code in your Emacs initialization file: @lisp (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) @@ -220,17 +284,17 @@ place the following code in your Emacs initialization file: @node Usage @chapter Usage -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with @samp{.lean} extension. Emacs will ask you to identify the @emph{project} this file belongs to. If you then type @samp{#check id}, the word @samp{#check} will be underlined, and hovering over it will show you the type of @code{id}. -To view the proof state, run @code{lean4-toggle-info} (@samp{C-c C-i}). This -will display the @samp{*Lean Goals*} buffer (like the Lean Info-View pane +To view the proof state, run @code{lean4-info-mode} (@samp{C-c C-i}). This +will display the @samp{*Lean4 Info*} buffer (like the Lean Info-View pane in VS-Code) in a separate window. -@multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} +@multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaa} @headitem Key @tab Description @tab Command @@ -239,16 +303,16 @@ in VS-Code) in a separate window. @tab @code{quail-show-key} @item @samp{C-c C-d} @tab Recompile and reload imports -@tab @code{lean4-refresh-file-dependencies} +@tab @code{lean4-lsp-document-reopen} @item @samp{C-c C-x} or @samp{C-c C-l} -@tab Execute Lean in stand-alone mode -@tab @code{lean4-std-exe} +@tab Execute Lean4 in stand-alone mode +@tab @code{lean4-execute} @item @samp{C-c C-p C-l} @tab Builds package with lake @tab @code{lean4-lake-build} @item @samp{C-c C-i} @tab Toggle Info-View which shows goals and errors at point -@tab @code{lean4-toggle-info-buffer} +@tab @code{lean4-info-mode} @end multitable @menu @@ -310,11 +374,225 @@ option accordingly. @node Common Pitfalls @chapter Common Pitfalls -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix @samp{lean-} for its symbols. E.g. you should not use -@samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode. +@menu +* Coexistence with Lean3-Mode:: +* Partial value of @code{lean4-mode-hook} or other hook variables:: +@end menu + +@node Coexistence with Lean3-Mode +@section Coexistence with Lean3-Mode + +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}. It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + +@itemize +@item +Lean3-Mode uses @samp{lean-} as prefix (e.g. for commands) whereas +Lean4-Mode uses @samp{lean4-} as prefix. When Lean4-Mode is active, +you must not use commands with prefix @samp{lean-}. + +@item +Both packages associate the @samp{.lean} file extension with their +respective commands. Even more confusingly, they use different +functions and regular expressions to do so. + +Lean3-Mode: +@lisp +;;;###autoload +(push '("\\.lean$" . lean-mode) auto-mode-alist) +@end lisp + +Lean4-Mode: +@lisp +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) +@end lisp + +Make sure that both packages are loaded, autoloaded and configured +in such a way @code{auto-mode-alist} ends up with your desired value. + +@item +In particular, if you want Emacs to automatically detect whether +Lean3- or Lean4-Mode should be used for a particular file or +project, you'll need to define your own Elisp function and associate +it with the Lean file extension. If desired, you can even do this +directory locally (via the special "variable" @samp{eval} in +@samp{.dir-locals.el}). +@end itemize + +@node Partial value of @code{lean4-mode-hook} or other hook variables +@section Partial value of @code{lean4-mode-hook} or other hook variables + +If you customize a hook variable like @code{lean4-mode-hook} e.g. with +@code{add-hook} or Use-Package's @samp{:hook} keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +@code{lean4-mode-hook} may not contain the @code{lsp} command and as a +consequence @code{lsp-mode} won't start automatically together with +Lean4-Mode. + +There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your @code{add-hook} form before it loads +the definition of the hook from Lean4-Mode package. (3.) @code{add-hook} +effectively initializes the passed hook-variable to nil when the +symbol has no value cell. And (4.), Use-Package applies passed @samp{:hook} +specifications before package loading. + +If you do not use Use-Package, the solution is to load Lean4-Mode +before calling @code{add-hook}, e.g. with @code{require}: +@lisp +(require 'lean4-mode) +(add-hook 'lean4-...-hook #'...) +@end lisp + +Or with @code{with-eval-after-load}: +@lisp +(with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) +(with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) +@end lisp + +If you do Use-Package, you can solve the problem by calling @code{add-hook} +within the @samp{:config} section: +@lisp +(use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) +@end lisp + +@node Changelog +@chapter Changelog + +@menu +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. +@end menu + +@node Upcoming Version +@section Upcoming Version + +Documentation: +@itemize +@item +The changelog is now part of the readme (and thus of the Info +manual). +@end itemize + +User interface: +@itemize +@item +The tool-bar menu of Lean4-Mode does not list the +@code{flycheck-list-errors} anymore. Please use the “Show all errors” +entry in Flycheck's menu instead. (Fixes @uref{https://github.com/leanprover-community/lean4-mode/issues/91, #91}.) +@end itemize + +Features: +@itemize +@item +The variable @code{lean4-delete-trailing-whitespace} has been removed +together with related code. Instead of reinventing the wheel, +Lean4-Mode demands users to use Emacs' built-in facilities for this +kind of use case. For example, you might want to define a function +that buffer-locally adds @code{delete-trailing-whitespace} to +@code{before-save-hook}, and add that hereby defined function to +@code{lean4-mode-hook}. +@item +The variable @code{lean4-autodetect-lean3} has been removed along with +the command @code{lean4-select-mode} and related code. If you still use +legacy version 3 of Lean for some files or projects, you could +directory- or file-locally associate the @samp{.lean} file extension with +Lean3-Mode in @code{auto-mode-alist}. +@item +The command @code{lean4-show-version} has been removed. Lean4-Mode now +assumes Lean version 4. In order to determine the minor version, you +may type @samp{M-! lean --version RET} or similar. +@item +The functions @code{lean4-input-export-translations} and +@code{lean4-input-export-translations-to-stdout} have been removed. We +expect that noone has been using it. If you do use it, let us know, +so we can reconsider our decision in case of a substantial amount of +users. Otherwise, please just define these functions in your Emacs +initialization file yourself. +@item +The command @code{lean4-std-exe} has been removed. It was just the same +as @code{lean4-execute} which continues to exist. +@end itemize + +@node Version 112 from 2024-12-10 +@section Version 1.1.2 from 2024-12-10 + +@itemize +@item +Fix occasional errors like "The connected server(s) does not support +method @samp{$/lean/plainGoal}" by not wrapping invocations of +@code{lsp-protocol} macro into @code{eval-when-compile} but rather into +@code{eval-and-compile}. Thus, the methods should now work, no matter +whether Lean4-Mode was loaded by interpreting @samp{.el} Elisp code or by +loading compiled @samp{.elc} or @samp{.eln} files. (@uref{https://github.com/leanprover-community/lean4-mode/issues/54, Bug#54}, @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table, Zulip discussion}) +@end itemize + +@node Version 111 from 2024-12-02 +@section Version 1.1.1 from 2024-12-02 + +@itemize +@item +Assign all customizable user-options to the Lean4-Mode specific +@samp{lean4} group. To customize Lean4-Mode, you now need to type @samp{M-x + customize-group RET lean4 RET}. +@end itemize + +@node Version 110 from 2024-12-01 +@section Version 1.1.0 from 2024-12-01 + +@itemize +@item +To @samp{lean4} customization group, add link to local info manual and +use Lean4-Mode Github URL as website. +@item +Introduce new dependency on Elpa package @samp{compat}. +@item +Remove dependency on Elpa package Flycheck. It is still supported +but not required. +@end itemize + +@node Version 101 from 2024-11-21 +@section Version 1.0.1 from 2024-11-21 + +@itemize +@item +Specify Yury G@. Kudryashov as maintainer. +@item +Rework README@. (Now in Org format). +@item +Provide README as Texi and Info manual too. +@end itemize + +@node Version 10 from 2024-11-16 +@section Version 1.0 from 2024-11-16 + +@itemize +@item +Specify "Version" in Emacs-Lisp library header. +@end itemize + +@node Contributing +@chapter Contributing + +When you contribute to Lean4-Mode, add a personal copyright like +@samp{;; Copyright (c) 2024 Firstname Lastname} to the header of respective +files. + +You can use Emacs' built-in @code{bug-reference-mode} and +@code{bug-reference-prog-mode} in this repository to make mentions of +issues like @samp{#123} clickable. @bye diff --git a/lean4-settings.el b/lean4-settings.el deleted file mode 100644 index 910e533..0000000 --- a/lean4-settings.el +++ /dev/null @@ -1,151 +0,0 @@ -;;; lean4-settings.el --- Lean4-Mode User-Options -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library defines custom variables for `lean4-mode'. - -;;; Code: - -(require 'cl-lib) -(require 'lsp-mode) - -(defgroup lean4 nil - "Major mode for Lean4 programming language and theorem prover." - :group 'languages - :link '(info-link :tag "Info Manual" "(lean4-mode)") - :link '(url-link - :tag "Website" - "https://github.com/leanprover-community/lean4-mode") - :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") - :prefix "lean4-") - -(defgroup lean4-keybinding nil - "Keybindings for lean4-mode." - :prefix "lean4-" - :group 'lean4) - -(defconst lean4-default-executable-name - (cl-case system-type - (windows-nt "lean.exe") - (t "lean")) - "Default executable name of Lean.") - -(defconst lean4-default-lake-name - (cl-case system-type - (windows-nt "lake.exe") - (t "lake")) - "Default executable name of Lake.") - -(defcustom lean4-mode-hook (list #'lsp) - "Hook run after entering `lean4-mode'." - :options '(flycheck-mode lsp) - :type 'hook - :group 'lean4) - -(defcustom lean4-rootdir nil - "Full pathname of lean root directory. It should be defined by user." - :group 'lean4 - :type 'string) - -(defcustom lean4-executable-name lean4-default-executable-name - "Name of lean executable." - :group 'lean4 - :type 'string) - -(defcustom lean4-lake-name lean4-default-lake-name - "Name of lake executable." - :group 'lake - :type 'string) - -(defcustom lean4-memory-limit 1024 - "Memory limit for lean process in megabytes." - :group 'lean4 - :type 'number) - -(defcustom lean4-timeout-limit 100000 - "Deterministic timeout limit. - -It is approximately the maximum number of memory allocations in thousands." - :group 'lean4 - :type 'number) - -(defcustom lean4-extra-arguments nil - "Extra command-line arguments to the lean process." - :group 'lean4 - :type '(list string)) - -(defcustom lean4-delete-trailing-whitespace nil - "Automatically delete trailing shitespace. -Set this variable to true to automatically delete trailing -whitespace when a buffer is loaded from a file or when it is -written." - :group 'lean4 - :type 'boolean) - -(defcustom lean4-highlight-inaccessible-names t - "Use font to highlight inaccessible names. -Set this variable to t to highlight inaccessible names in the info display -using `font-lock-comment-face' instead of the `✝` suffix used by Lean." - :group 'lean4 - :type 'boolean) - -(defcustom lean4-show-file-progress t - "Highlight file progress in the current buffer." - :group 'lean4 - :type 'boolean) - - -(defcustom lean4-autodetect-lean3 nil - "Autodetect Lean version. -Use elan to check if current project uses Lean 3 or Lean 4 and initialize the -right mode when visiting a file. If elan has a default Lean version, Lean files -outside a project will default to that mode." - :group 'lean4 - :type 'boolean) - -(defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x") - "Main Keybinding for `lean4-std-exe'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-std-exe2 (kbd "C-c C-l") - "Alternative Keybinding for `lean4-std-exe'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-show-key (kbd "C-c C-k") - "Lean Keybinding for `quail-show-key'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-server-restart (kbd "C-c C-r") - "Lean Keybinding for server-restart." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-tab-indent (kbd "TAB") - "Lean Keybinding for `lean4-tab-indent'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-auto-complete (kbd "S-SPC") - "Lean Keybinding for auto completion." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-lean4-toggle-info (kbd "C-c C-i") - "Lean Keybinding for `lean4-toggle-info'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-lake-build (kbd "C-c C-p C-l") - "Lean Keybinding for `lean4-lake-build'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-refresh-file-dependencies (kbd "C-c C-d") - "Lean Keybinding for `lean4-refresh-file-dependencies'." - :group 'lean4-keybinding :type 'key-sequence) - -(provide 'lean4-settings) -;;; lean4-settings.el ends here diff --git a/lean4-syntax.el b/lean4-syntax.el index 26b7fd1..6bfb41e 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -1,8 +1,8 @@ -;;; lean4-syntax.el --- Lean4-Mode Syntax Definitions -*- lexical-binding: t; -*- +;;; lean4-syntax.el --- Lean4 syntax -*- lexical-binding: t; -*- -;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. +;; Copyright (c) 2013, 2014 Microsoft Corporation -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You @@ -22,9 +22,10 @@ ;;; Code: -(require 'dash) (require 'rx) +(require 'dash) + (defconst lean4-keywords1 '("import" "prelude" "protected" "private" "noncomputable" "unsafe" "partial" "renaming" "hiding" "begin" "constant" @@ -39,9 +40,11 @@ "exists" "if" "then" "else" "from" "init_quot" "return" "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" "elab" "initialize" "builtin_initialize" "register_builtin_option" "induction" "cases" "generalizing" "unif_hint" "deriving") - "Lean keywords ending with `word' (not symbol).") + "Lean4 keywords ending with `word' (not symbol).") + (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end))) + (defconst lean4-constants '("#" "@" "!" "$" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ" @@ -50,21 +53,27 @@ "⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o" "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1" "^c" "≃c" "≅c" "×c" "×f" "×n" "+c" "+f" "+n" "ℕ₋₂") - "Lean constants.") + "Lean4 constants.") + (defconst lean4-constants-regexp (regexp-opt lean4-constants)) + (defconst lean4-numerals-regexp (eval `(rx word-start (one-or-more digit) (optional (and "." (zero-or-more digit))) word-end))) -(defconst lean4-warnings '("sorry") "Lean warnings.") +(defconst lean4-warnings '("sorry") "Lean4 warnings.") + (defconst lean4-warnings-regexp (eval `(rx word-start (or ,@lean4-warnings) word-end))) -(defconst lean4-debugging '("unreachable!" "panic!" "assert!" "dbg_trace") "Lean debugging.") + +(defconst lean4-debugging + '("unreachable!" "panic!" "assert!" "dbg_trace") + "Lean4 debugging.") + (defconst lean4-debugging-regexp (eval `(rx word-start (or ,@lean4-debugging) word-end))) - (defconst lean4-syntax-table (let ((st (make-syntax-table))) ;; Matching parens @@ -130,7 +139,7 @@ ?' ?_ ?! ??) (modify-syntax-entry it "w" st)) - ;; Lean operator chars + ;; Operator chars (--each (string-to-list "#$%&*+<=>@^|~:") (modify-syntax-entry it "." st)) @@ -197,7 +206,7 @@ (2 nil t) (3 font-lock-comment-face t))))) -;; Syntax Highlighting for Lean Info Mode +;; Syntax Highlighting for Lean4 Info (defconst lean4-info-font-lock-defaults (let ((new-entries `(;; Please add more after this: diff --git a/lean4-util.el b/lean4-util.el deleted file mode 100644 index 273a530..0000000 --- a/lean4-util.el +++ /dev/null @@ -1,64 +0,0 @@ -;;; lean4-util.el --- Lean4-Mode Utilities -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library provides utilities for `lean4-mode'. - -;;; Code: - -(require 'compat) -(require 'lean4-settings) - -(defun lean4-setup-rootdir () - "Search for lean executable in variable `exec-path'. -Try to find an executable named `lean4-executable-name' in variable `exec-path'. -On succsess, return path to the directory with this executable." - (let ((root (executable-find lean4-executable-name))) - (when root - (setq lean4-rootdir (file-name-directory - (directory-file-name - (file-name-directory root))))) - lean4-rootdir)) - -(defun lean4-get-rootdir () - "Search for lean executable in `lean4-rootdir' and variable `exec-path'. -First try to find an executable named `lean4-executable-name' in -`lean4-rootdir'. On failure, search in variable `exec-path'." - (if lean4-rootdir - (let ((lean4-path (expand-file-name lean4-executable-name (expand-file-name "bin" lean4-rootdir)))) - (unless (file-exists-p lean4-path) - (error "Incorrect `lean4-rootdir' value, path '%s' does not exist" lean4-path)) - lean4-rootdir) - (or - (lean4-setup-rootdir) - (error - (concat "Lean was not found in the `exec-path' and `lean4-rootdir' is not defined. " - "Please set it via M-x customize-variable RET lean4-rootdir RET."))))) - -(defun lean4-get-executable (exe-name) - "Return fullpath of lean executable EXE-NAME." - (file-name-concat (lean4-get-rootdir) "bin" exe-name)) - -(defun lean4-whitespace-cleanup () - "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t." - (when lean4-delete-trailing-whitespace - (delete-trailing-whitespace))) - -(provide 'lean4-util) -;;; lean4-util.el ends here