diff --git a/.dir-locals.el b/.dir-locals.el index 285f530..cd1980e 100644 --- a/.dir-locals.el +++ b/.dir-locals.el @@ -1,5 +1,5 @@ -;; -*- no-byte-compile: t; -*- +;;; Directory Local Variables -*- no-byte-compile: t -*- +;;; For more information see (info "(emacs) Directory Variables") -((nil - (bug-reference-url-format - . "https://github.com/leanprover-community/lean4-mode/issues/%s"))) +((nil . ((bug-reference-url-format . "https://github.com/leanprover-community/lean4-mode/issues/%s"))) + (emacs-lisp-mode . ((indent-tabs-mode . nil)))) 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/README.org b/README.org index ac66c63..0172c65 100644 --- a/README.org +++ b/README.org @@ -1,20 +1,16 @@ -#+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 -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 @@ -147,7 +143,7 @@ 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 +will display the =*Lean4 Info*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. | Key | Description | Command | @@ -194,9 +190,55 @@ 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. +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]], 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. Make +sure to not use these =lean-=-prefixed commands in buffers where +Lean4-Mode is the major mode. + +* 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. + +* Changelog + +** 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/lean4-debug.el b/lean4-debug.el deleted file mode 100644 index 5d86a1c..0000000 --- a/lean4-debug.el +++ /dev/null @@ -1,77 +0,0 @@ -;;; lean4-debug.el --- Lean4-Mode Debug Mode -*- 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 a debug mode for `lean4-mode'. - -;;; Code: - -(require 'cl-lib) - -(defvar lean4-debug-mode nil) - -(defvar lean4-debug-buffer-name "*lean4-debug*") - -(defun lean4-turn-on-debug-mode (&optional print-msg) - "Turn on Lean debug. -Print message \"lean: turn on debug mode\" if PRINT-MSG or if called -interactively." - (interactive) - (when (or (called-interactively-p 'any) print-msg) - (message "lean: turn on debug mode")) - (get-buffer-create lean4-debug-buffer-name) - (buffer-disable-undo lean4-debug-buffer-name) - (display-buffer lean4-debug-buffer-name 'display-buffer-reuse-window - '((reusable-frames . t))) - (setq lean4-debug-mode t)) - -(defun lean4-turn-off-debug-mode (&optional print-msg) - "Turn off Lean debug. -Print message \"lean: turn off debug mode\" if PRINT-MSG or if called -interactively." - (interactive) - (when (derived-mode-p 'lean4-mode) - (when (or (called-interactively-p 'any) print-msg) - (message "lean: turn off debug mode")) - (setq lean4-debug-mode nil))) - -(defun lean4-output-to-buffer (buffer-name format-string args) - "Output a message to a buffer. -The buffer is given by BUFFER-NAME. The message is given by FORMAT-STRING -and ARGS." - (with-current-buffer - (get-buffer-create buffer-name) - (save-selected-window - (ignore-errors - (select-window (get-buffer-window buffer-name t))) - (goto-char (point-max)) - (insert (apply #'format format-string args))))) - -(defun lean4-debug (format-string &rest args) - "Display a message at the bottom of the *lean4-debug* buffer. -The message is given by FORMAT-STRING and ARGS." - (when lean4-debug-mode - (let ((time-str (format-time-string "%T.%3N" (current-time)))) - (lean4-output-to-buffer lean4-debug-buffer-name - (concat "%s -- " format-string "\n") - (cons (propertize time-str 'face 'font-lock-keyword-face) - args))))) - -(provide 'lean4-debug) -;;; lean4-debug.el ends here diff --git a/lean4-dev.el b/lean4-dev.el deleted file mode 100644 index f9cc5ba..0000000 --- a/lean4-dev.el +++ /dev/null @@ -1,35 +0,0 @@ -;;; lean4-dev.el --- Lean4-Mode Development Commands -*- lexical-binding: t; -*- - -;; Copyright (c) 2017 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 currently provides `lean4-diff-test-file' command. - -;;; Code: - -(require 'lean4-util) - -(defun lean4-diff-test-file () - "Use interactive ./test_input.sh on file of current buffer." - (interactive) - (save-buffer) - ; yes: auto-agree to copying missing files - (message (shell-command-to-string (format "yes | PATH=%s/bin:$PATH LEAN_NIX_ARGS=--quiet ./test_single.sh -i \"%s\"" (lean4-get-rootdir) (file-name-nondirectory (buffer-file-name)))))) - -(provide 'lean4-dev) -;;; lean4-dev.el ends here diff --git a/lean4-eri.el b/lean4-eri.el index a85b474..f562ddc 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -223,5 +223,24 @@ are calculated." (interactive) (lean4-eri-indent t)) +(defun lean4-eri-tab () + "Lean4 function for TAB indent." + (interactive) + (if (looking-back (rx line-start (* white)) nil) + (lean4-eri-indent) + (let ((indent-line-function 'indent-relative)) + (indent-for-tab-command)))) + +(defun lean4-eri-init () + "Setup buffer-local variables and minor modes for `lean4-eri'." + (setq-local indent-line-function + #'lean4-eri-tab) + (setq-local lisp-indent-function + #'common-lisp-indent-function) + (when (fboundp 'electric-indent-local-mode) + (electric-indent-local-mode -1)) + (when (fboundp 'indent-tabs-mode) + (indent-tabs-mode -1))) + (provide 'lean4-eri) ;;; lean4-eri.el ends here diff --git a/lean4-exec.el b/lean4-exec.el new file mode 100644 index 0000000..40564a6 --- /dev/null +++ b/lean4-exec.el @@ -0,0 +1,229 @@ +;;; lean4-exec.el --- Lean4-Mode Executable Location -*- lexical-binding: t; -*- + +;; Copyright (c) 2024 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 provides a facility to locate the executables of Elan, +;; Lake and Lean so that they can be used to build/compile the current +;; project, start an LSP server or execute some other shell command. + +;;; Code: + +;;;; Elan + +(defcustom lean4-exec-elan-base "elan" + "Basename of Elan executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-elan-full nil + "Full name of Elan executable. + +It may be nil in which case Elan won't be used. Otherwise it should be +a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"elan\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-elan-executable-find () + "Attempt to find Elan executable with `executable-find'." + (declare (side-effect-free t)) + (ensure-list (executable-find lean4-exec-elan-base))) + +(defcustom lean4-exec-elan-init-hook + (list #'lean4-exec-elan-executable-find) + "Hook of functions to determine `lean4-exec-elan-full'. + +This hook is called from `lean4-exec-elan-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-elan-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-elan-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Elan executable." + :group 'lean4-exec + :options '(lean4-exec-elan-executable-find) + :type 'hook) + +(defun lean4-exec-elan-init () + "Buffer-locally set up `lean4-exec-elan-full'. + +Call functions from `lean4-exec-elan-init-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-elan-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-elan-full + (run-hook-with-args-until-success + 'lean4-exec-elan-init-hook))) + +;;;; Lake + +(defcustom lean4-exec-lake-base "lake" + "Basename of Lake executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-lake-full nil + "Full name of Lake executable. + +It may be nil in which case Lake won't be used. Otherwise it should be +a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"lake\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-lake-elan-which () + "When `lean4-exec-elan-full', then attemp to find Lake with Elan." + (declare (side-effect-free t)) + (when lean4-exec-elan-full + (ignore-errors + ;; This assumes that "elan which lake" outputs only a single + ;; line and a final newline. In particular it assumes that the + ;; path to the Lake executable does not contain newlines. + (apply #'process-lines + (append lean4-exec-elan-full '("which" "lake")))))) + +(defun lean4-exec-lake-executable-find () + "Attempt to find Lake executable with `executable-find'." + (declare (side-effect-free t)) + (ensure-list (executable-find lean4-exec-lake-base))) + +(defcustom lean4-exec-lake-init-hook + (list + #'lean4-exec-lake-elan-which + #'lean4-exec-lake-executable-find) + "Hook of functions to determine `lean4-exec-lake-full'. + +This hook is called from `lean4-exec-lake-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-lake-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-lake-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Lake executable." + :group 'lean4-exec + :options '(lean4-exec-lake-executable-find) + :type 'hook) + +(defun lean4-exec-lake-init () + "Buffer-locally set up `lean4-exec-lake-full'. + +Call functions from `lean4-exec-lake-init-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-lake-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-lake-full + (run-hook-with-args-until-success + 'lean4-exec-lake-init-hook))) + +;;;; Lean + +(defcustom lean4-exec-lean-base "lean" + "Basename of Lean4 executable (without suffixes, if any)." + :group 'lean4-exec + :type 'string) + +(defvar-local lean4-exec-lean-full nil + "Full name of Lean4 executable. + +It should be a list of strings, for example: + + (\"docker\" \"compose\" \"debian\" \"exec\" \"lake\" \"lean\") + +Member strings should not be quoted. Consumers of this variable are +expected to quote as needed, e.g. by using `combine-and-quote-strings' +if necessary.") + +(defun lean4-exec-lean-getenv () + "Attempt to find Lean4 executable per `LEAN' environment variable." + (declare (side-effect-free t)) + (ensure-list (getenv "LEAN"))) + +(defun lean4-exec-lean-elan-which () + "When `lean4-exec-elan-full', then attemp to find Lean with Elan." + (declare (side-effect-free t)) + (when lean4-exec-elan-full + (ignore-errors + ;; This assumes that "elan which lean" outputs only a single + ;; line and a final newline. In particular it assumes that the + ;; path to the Lean executable does not contain newlines. + (apply #'process-lines + (append lean4-exec-elan-full '("which" "lean")))))) + +(defun lean4-exec-lean-lake () + "When `lean4-exec-lake-full', return `lean' as its subcommand." + (declare (side-effect-free error-free)) + (when lean4-exec-lake-full + (append lean4-exec-lake-full + ;; We do not use `lean4-exec-lean-base' here because a + ;; user could have set it to "lean4" but Lake only accepts + ;; "lean" as subcommand. + '("lake")))) + +(defcustom lean4-exec-lean-init-hook + (list + #'lean4-exec-lean-getenv + #'lean4-exec-lean-elan-which + #'lean4-exec-lean-lake) + "Hook of functions to determine `lean4-exec-lean-full'. + +This hook is called from `lean4-exec-lean-init'. Each member function +represents a certain method of determining a value suitable for +`lean4-exec-lean-full', which see. If it does not find such a value, it +should return nil. It should probably use `lean4-exec-lean-base' (and +maybe `executable-binary-suffixes') instead of a hard-coded basename for +the Lean4 executable." + :group 'lean4-exec + :options '(lean4-exec-lean-getenv + lean4-exec-lean-elan-which + lean4-exec-lean-lake) + :type 'hook) + +(defun lean4-exec-lean-init () + "Buffer-locally set up `lean4-exec-lean-full'. + +Call functions from `lean4-exec-lean-init-hook' until one succeeds, +i.e. returns non-nil. `lean4-exec-lean-full' is then buffer-locally set +to this value." + (setq-local lean4-exec-lean-full + (run-hook-with-args-until-success + 'lean4-exec-lean-init-hook))) + +;;;; Initialization + +(defun lean4-exec-init () + "Initialize full paths to Elan, Lake and Lean executables. + +If a Lean executable was found, return its path. Otherwise, return nil." + (interactive) + (lean4-exec-elan-init) + (lean4-exec-lake-init) + (lean4-exec-lean-init)) + +(defun lean4-exec-compile-command-init () + "When `lean4-exec-lean-full', setup `compile-command' for `lean4-mode'." + (interactive) + (when lean4-exec-lean-full + (setq-local compile-command + (string-join (append lean4-exec-lean-full '("build")) + " ")))) + +(provide 'lean4-exec) +;;; lean4-exec.el ends here diff --git a/lean4-fringe.el b/lean4-fringe.el index e5ab9e0..851f6a1 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -22,7 +22,6 @@ ;;; Code: -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) @@ -70,6 +69,11 @@ (defvar-local lean4-fringe-data nil) +(defcustom lean4-show-file-progress t + "Highlight file progress in the current buffer." + :group 'lean4 + :type 'boolean) + (defun lean4-fringe-update-progress-overlays () "Update processing bars in the current buffer." (dolist (ov (flatten-tree (overlay-lists))) diff --git a/lean4-info.el b/lean4-info.el index 923cf56..8406da2 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -24,7 +24,6 @@ (require 'dash) (require 'lean4-syntax) -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) (require 'magit-section) @@ -33,10 +32,9 @@ "Lean4-Mode Info." :group 'lean4) -;; Lean Info Mode (for "*lean4-info*" buffer) ;; Automode List ;;;###autoload -(define-derived-mode lean4-info-mode prog-mode "Lean-Info" +(define-derived-mode lean4-info-mode prog-mode "Lean4-Info" "Major mode for Lean4-Mode Info Buffer." :syntax-table lean4-syntax-table :group 'lean4 @@ -48,7 +46,7 @@ (defun lean4-ensure-info-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) @@ -58,7 +56,7 @@ Also choose settings used for the *Lean Goal* buffer." (defun lean4-toggle-info-buffer (buffer) "Create or delete BUFFER. -The buffer is supposed to be the *Lean Goal* buffer." +The buffer is supposed to be the *Lean4 Info* buffer." (-if-let (window (get-buffer-window buffer)) (quit-window nil window) (lean4-ensure-info-buffer buffer) @@ -80,7 +78,7 @@ 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) @@ -100,6 +98,13 @@ The buffer is supposed to be the *Lean Goal* buffer." (forward-line (1- line)) (forward-char column)))) +(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) + (defun lean4-info--insert-highlight-inaccessible-names (&rest text) (let ((begin (point))) (apply #'insert text) @@ -227,7 +232,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (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) @@ -260,33 +265,33 @@ 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-to-seconds - (time-subtract (current-time) - lean4-info-buffer-debounce-begin-time)) - lean4-info-buffer-debounce-upper-bound-sec) - ;; then redisplay immediately. + (time-subtract (current-time) + lean4-info-buffer-debounce-begin-time)) + lean4-info-buffer-debounce-upper-bound-sec) + ;; then redisplay immediately. (progn - ;; We have stopped debouncing. - (setq lean4-info-buffer-debounce-begin-time nil) - (lean4-info-buffer-redisplay)) + ;; We have stopped debouncing. + (setq lean4-info-buffer-debounce-begin-time nil) + (lean4-info-buffer-redisplay)) ;; else cancel current timer, create new debounced timer. (-some-> lean4-info-buffer-debounce-timer cancel-timer) (setq lean4-info-buffer-debounce-timer ; set new timer - (run-with-timer - lean4-info-buffer-debounce-delay-sec - nil ; don't repeat timer - (lambda () - ;; We have stopped debouncing. - (setq lean4-info-buffer-debounce-begin-time nil) - (lean4-info-buffer-redisplay)))))) + (run-with-timer + lean4-info-buffer-debounce-delay-sec + nil ;; don't repeat timer + (lambda () + ;; We have stopped debouncing. + (setq lean4-info-buffer-debounce-begin-time nil) + (lean4-info-buffer-redisplay)))))) (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" diff --git a/lean4-input.el b/lean4-input.el index fce884f..92e2141 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -22,7 +22,7 @@ ;; 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 @@ -145,7 +145,7 @@ This suffix is dropped." ;; 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,9 +162,9 @@ 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 -input method (with the exception of translations corresponding to -ASCII characters). +Translations from these methods will be inherited by the Lean4 input +method (with the exception of translations corresponding to ASCII +characters). The list consists of pairs (qp . tweak), where qp is the name of a Quail package, and tweak is an expression of the same signature as @@ -189,7 +189,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 @@ -222,7 +222,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 +230,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 +238,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 @@ -261,14 +261,15 @@ a list of such pairs." (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 @@ -296,47 +297,21 @@ 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 - -(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-init () + "Setup the input method for `lean4-mode'." (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)))) + (require 'lean4-input) + (set-input-method "Lean4")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Administrative details diff --git a/lean4-lake.el b/lean4-lake.el deleted file mode 100644 index bfca627..0000000 --- a/lean4-lake.el +++ /dev/null @@ -1,50 +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-lake-find-dir-in (dir) - "Find a parent directory of DIR with file \"lakefile.lean\"." - (when dir - (or (when (file-exists-p (expand-file-name "lakefile.lean" dir)) dir) - (lean4-lake-find-dir-in (file-name-directory (directory-file-name dir)))))) - -(defun lean4-lake-find-dir () - "Find a parent directory of the current file with file \"lakefile.lean\"." - (and (buffer-file-name) - (lean4-lake-find-dir-in (directory-file-name (buffer-file-name))))) - -(defun lean4-lake-find-dir-safe () - "Call `lean4-lake-find-dir', error on failure." - (or (lean4-lake-find-dir) - (error "Cannot find lakefile.lean for %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-mode.el b/lean4-mode.el index 5cd91f1..0603874 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -31,28 +31,28 @@ ;;; Commentary: -;; Provides a major mode for the Lean programming language. +;; This is `lean4-mode', an Elpa package for Emacs that provides a +;; major mode for the Lean programming language and theorem prover. +;; The mode features highlighting, diagnostics, goal visualization, +;; among others. For more information, see read the README.org or +;; equally the Info manual (info "(lean4-mode) Top"). -;; 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. +;; This file is the entry point for the equally named package. It +;; defines the major mode, the syntax and other core features. ;;; Code: (require 'cl-lib) -(require 'dash) (require 'pcase) -(require 'lsp-mode) + (require 'lean4-eri) -(require 'lean4-util) -(require 'lean4-settings) -(require 'lean4-syntax) -(require 'lean4-info) -(require 'lean4-dev) +(require 'lean4-exec) (require 'lean4-fringe) -(require 'lean4-lake) +(require 'lean4-info) +(require 'lean4-syntax) + +(require 'dash) +(require 'lsp-mode) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: @@ -67,13 +67,28 @@ (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))) +(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-delete-trailing-whitespace nil + "Delete trailing whitespace before saving buffer to file. + +If this variable is non-nil, Lean4-Mode will delete trailing whitespace +of every line before the buffer is saved to file." + :group 'lean4 + :type 'boolean) + +(defun lean4-whitespace-cleanup () + "When `lean4-delete-trailing-whitespace', delete trailing whitespace." + (when lean4-delete-trailing-whitespace + (delete-trailing-whitespace))) (defun lean4-create-temp-in-system-tempdir (file-name prefix) "Create a temp lean file and return its name. @@ -81,33 +96,6 @@ 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." - (interactive) - (lean4-execute)) - (defun lean4-refresh-file-dependencies () "Refresh the file dependencies. @@ -125,82 +113,32 @@ file, recompiling, and reloading all imports." :version lsp--cur-version :text (lsp--buffer-content))))) -(defun lean4-tab-indent () - "Lean 4 function for TAB indent." - (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.") +(defvar-keymap lean4-mode-map + :doc "Keymap for `lean4-mode'." + "C-c C-k" #'quail-show-key + "C-c C-i" #'lean4-toggle-info + "C-c C-c" #'project-compile + "C-c C-d" #'lean4-refresh-file-dependencies) (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] + `("Lean4" + ["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." + ["List of errors" flycheck-list-errors (bound-and-true-p flycheck-mode)] + ["Restart Lean4 LSP server" lsp-workspace-restart t] + ["Customize lean4-mode" (customize-group 'lean4) t])) + +(defun lean4-lsp-workspace-init () + "Initialize Lean4 `lsp-mode' workspace. + +Starting from function `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"))) @@ -211,91 +149,171 @@ of the parent project." (when root (lsp-workspace-folders-add root)))) +(defun lean4-lsp-semantic-token-init () + "Buffer-locally enable `lsp-mode's support for semantic tokens." + (interactive) + (setq-local lsp-semantic-tokens-enable t)) + +(defcustom lean4-mode-hook + (list #'lean4-input-init + #'lean4-exec-init + #'lean4-exec-compile-command-init + #'lean4-eri-init + #'lean4-lsp-semantic-token-init + #'lean4-lsp-workspace-init + #'lsp) + "Hook run after entering `lean4-mode'. + +Note that there's no need to add `lsp-diagnostics-mode' to this hook as +it will be called by `lsp'. Similarly, `flycheck-mode' should not be +added here because it will be called by `lsp' if the variable +`lsp-diagnostics-provider' is set accordingly." + :options '(lean4-input-init + lean4-exec-init + lean4-exec-compile-command-init + lean4-eri-init + lean4-lsp-semantic-token-init + lean4-lsp-workspace-init + lsp) + :type 'hook + :group 'lean4) + ;;;###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 programming language and theorem prover. \\{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) - (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)))) - -(defun lean4-show-version () - "Print Lean 4 version." + + (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 compilation-mode-font-lock-keywords + nil) + (setq-local font-lock-defaults + lean4-font-lock-defaults) + + ;; Clean up whitespace before saving. + (add-hook 'before-save-hook + #'lean4-whitespace-cleanup + nil 'local) + (add-hook 'post-command-hook + #'lean4-info-buffer-redisplay-debounced + nil 'local) + + ;; Flycheck: + (setq-local flycheck-disabled-checkers + nil) + ;; In Info View, update errors immediately, but delay querying goal. + (add-hook 'flycheck-after-syntax-check-hook + #'lean4-info-buffer-redisplay-debounced + nil 'local) + + ;; lsp-mode: + (add-hook 'lsp-on-idle-hook + #'lean4-info-buffer-refresh + nil 'local)) + +(defun lean4-version-extract () + "Return Lean version as a list (MAJOR MINOR PATCH)." + (when lean4-exec-lean-full + (let* ((executable (car lean4-exec-lean-full)) + (base-arguments (cdr lean4-exec-lean-full))) + (with-temp-buffer + (call-process + executable nil (list t nil) nil + (string-join (append base-arguments '("-v")) " ")) + (goto-char (point-min)) + (re-search-forward + (rx line-start "Lean (version " + (group (one-or-more digit) + (one-or-more "." (one-or-more digit))))) + (version-to-list (match-string 1)))))) + +(defun lean4-version () + "Echo version of Lean used by current buffer." (interactive) - (message "Lean %s" (mapconcat #'number-to-string (lean4--version) "."))) + (message "Lean %s" (mapconcat #'number-to-string + (lean4-version-extract) + "."))) + +(defcustom lean4-version-adapt nil + "Check Lean version. + +In case of legacy version 3, turn on `lean-mode'. +Otherwise, turn on `lean4-mode'." + :group 'lean4 + :type 'boolean) ;;;###autoload -(defun lean4-select-mode () - "Automatically select mode (Lean 3 vs Lean 4)." - (if (and lean4-autodetect-lean3 - (eq 3 (car (lean4--version)))) +(defun lean4-turn-on () + "Turn on `lean4-mode' but with respect to `lean4-version-adapt'." + (if (and + ;; User wants to adapt to Lean version. + lean4-version-adapt + ;; We are able to find a Lean executable. + (lean4-exec-init) + ;; The major version of found Lean executable has is three. + (eq 3 (car-safe (lean4-version-extract)))) (lean-mode) (lean4-mode))) ;; Automatically use lean4-mode for .lean files. ;;;###autoload (add-to-list 'auto-mode-alist - '("\\.lean\\'" . lean4-select-mode)) + '("\\.lean\\'" . lean4-turn-on)) ;;;###autoload (with-eval-after-load 'markdown-mode (add-to-list 'markdown-code-lang-modes - '("lean" . lean4-select-mode))) + '("lean" . lean4-turn-on))) -;; Use utf-8 encoding -;;;### autoload +;; According to the Lean4 reference manual, Lean4 code must be encoded +;; as `utf-8': +;; https://lean-lang.org/doc/reference/latest/Source-Files/Files/ +;;;###autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) -;; LSP init -;; Ref: https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/ +;; 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")))) + '(lean4-mode . "lean4")) + +(defun lean4-lsp-server-command () + "Lean4 LSP server command. + +`lake serve' is preferred over `lean --serve'." + (cond + (lean4-exec-lake-full (append lean4-exec-lake-full '("serve"))) + (lean4-exec-lean-full (append lean4-exec-lean-full '("--serve"))))) (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))))) + (make-lsp-client + :language-id "lean4" + :major-modes '(lean4-mode) + :new-connection + (lsp-stdio-connection #'lean4-lsp-server-command + ;; We don't want to pass the server command to + ;; `executable-find' so that `lean4-exec' + ;; keeps control over the exact path (or not, + ;; if it doesn't want to). + #'always) + :notification-handlers + (ht ("$/lean/fileProgress" #'lean4-fringe-update)) + ;; The semantic token type `leanSorryLike' is a Lean4-specific + ;; extension of LSP. + :semantic-tokens-faces-overrides + '(:types (("leanSorryLike" . font-lock-warning-face))) + :server-id 'lean4)) (provide 'lean4-mode) ;;; lean4-mode.el ends here diff --git a/lean4-mode.info b/lean4-mode.info index 41a8f4c..cb90b18 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -9,22 +9,18 @@ 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,6 +28,8 @@ Lean's Zulip chat. * Usage:: * Configuration:: * Common Pitfalls:: +* Contributing:: +* Changelog:: -- The Detailed Node Listing -- @@ -57,6 +55,14 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Changelog + +* Version 1.1.2: Version 112. +* Version 1.1.1: Version 111. +* Version 1.1.0: Version 110. +* Version 1.0.1: Version 101. +* Version 1.0: Version 10. +  File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top @@ -223,7 +229,7 @@ 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 +will display the ‘*Lean4 Info*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. Key Description Command @@ -300,37 +306,129 @@ 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: Contributing, 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. +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), 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. Make sure to +not use these ‘lean-’-prefixed commands in buffers where Lean4-Mode is +the major mode. + + +File: lean4-mode.info, Node: Contributing, Next: Changelog, Prev: Common Pitfalls, Up: Top + +5 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. + + +File: lean4-mode.info, Node: Changelog, Prev: Contributing, Up: Top + +6 Changelog +*********** + +* Menu: + +* Version 1.1.2: Version 112. +* Version 1.1.1: Version 111. +* Version 1.1.0: Version 110. +* Version 1.0.1: Version 101. +* Version 1.0: Version 10. + + +File: lean4-mode.info, Node: Version 112, Next: Version 111, Up: Changelog + +6.1 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. (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, Next: Version 110, Prev: Version 112, Up: Changelog + +6.2 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’. + + +File: lean4-mode.info, Node: Version 110, Next: Version 101, Prev: Version 111, Up: Changelog + +6.3 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. + + +File: lean4-mode.info, Node: Version 101, Next: Version 10, Prev: Version 110, Up: Changelog + +6.4 Version 1.0.1 +================= + + • 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, Prev: Version 101, Up: Changelog + +6.5 Version 1.0 +=============== + + • Specify "Version" in Emacs-Lisp library header.  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: Installation1437 +Node: Brief and Generic Instructions1680 +Node: Detailed and Concrete Instructions2629 +Node: Instructions for Source-Based Use-Package4286 +Node: Native vc (Emacs 30 or later)5007 +Node: Doom-Emacs5915 +Node: Straight6341 +Node: Usage6841 +Node: lsp-mode8287 +Node: Flycheck8572 +Node: Configuration9182 +Node: lsp-mode (1)9372 +Node: Flycheck (1)9641 +Node: Common Pitfalls10126 +Node: Contributing10751 +Node: Changelog11192 +Node: Version 11211448 +Node: Version 11112224 +Node: Version 11012551 +Node: Version 10112969 +Node: Version 1013252  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index fd205bf..2813c16 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -1,7 +1,7 @@ \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 @@ -13,25 +13,21 @@ @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,6 +36,8 @@ as @emph{Lean-Mode}). * Usage:: * Configuration:: * Common Pitfalls:: +* Contributing:: +* Changelog:: @detailmenu --- The Detailed Node Listing --- @@ -66,6 +64,14 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Changelog + +* Version 1.1.2: Version 112. +* Version 1.1.1: Version 111. +* Version 1.1.0: Version 110. +* Version 1.0.1: Version 101. +* Version 1.0: Version 10. + @end detailmenu @end menu @@ -227,7 +233,7 @@ 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 +will display the @samp{*Lean4 Info*} buffer (like the Lean Info-View pane in VS-Code) in a separate window. @multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} @@ -310,11 +316,91 @@ 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. +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}, which is also known as +@emph{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. Make +sure to not use these @samp{lean-}-prefixed commands in buffers where +Lean4-Mode is the major mode. + +@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. + +@node Changelog +@chapter Changelog + +@menu +* Version 1.1.2: Version 112. +* Version 1.1.1: Version 111. +* Version 1.1.0: Version 110. +* Version 1.0.1: Version 101. +* Version 1.0: Version 10. +@end menu + +@node Version 112 +@section Version 1.1.2 + +@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 +@section Version 1.1.1 + +@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 +@section Version 1.1.0 + +@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 +@section Version 1.0.1 + +@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 +@section Version 1.0 + +@itemize +@item +Specify "Version" in Emacs-Lisp library header. +@end itemize @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-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