diff --git a/.dir-locals.el b/.dir-locals.el new file mode 100644 index 0000000..285f530 --- /dev/null +++ b/.dir-locals.el @@ -0,0 +1,5 @@ +;; -*- no-byte-compile: t; -*- + +((nil + (bug-reference-url-format + . "https://github.com/leanprover-community/lean4-mode/issues/%s"))) diff --git a/.github/workflows/melpazoid.yml b/.github/workflows/melpazoid.yml index 4e0d05b..3453178 100644 --- a/.github/workflows/melpazoid.yml +++ b/.github/workflows/melpazoid.yml @@ -25,7 +25,11 @@ jobs: env: LOCAL_REPO: ${{ github.workspace }} # RECIPE is your recipe as written for MELPA: - RECIPE: (lean4-mode :fetcher github :repo "leanprover/lean4-mode" :files (:defaults ("data" "data/*.json"))) + RECIPE: >- + (lean4-mode + :fetcher github + :repo "leanprover-community/lean4-mode" + :files (:defaults ("data" "data/*.json"))) # set this to false (or remove it) if the package isn't on MELPA: # EXIST_OK: true run: echo $GITHUB_REF && make -C ~/melpazoid diff --git a/CHANGELOG.org b/CHANGELOG.org index 60ec926..0a891ef 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -1,7 +1,13 @@ #+title: Lean4-Mode - Changelog #+language: en -* Development +* 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 diff --git a/README.org b/README.org index eff7672..b9f420b 100644 --- a/README.org +++ b/README.org @@ -1,13 +1,13 @@ -#+title: Lean4-Mode - Emacs major-mode for Lean language +#+title: Lean4-Mode - Emacs major mode for Lean language #+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 Lean language -This package extends GNU Emacs by providing a major-mode for editing +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 Lean. +prover [[https://lean-lang.org][Lean]]. 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 @@ -20,18 +20,18 @@ known as /Lean-Mode/). ** Brief and Generic Instructions -Install dependencies: -- [[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]] (which is available on GNU-Elpa - package-archive), [[https://www.flycheck.org][Flycheck]], [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (which are - available on Melpa package-archive) +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) -Install Lean4-Mode: +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 and -- load Lean4-Mode with =(require 'lean4-mode)=. + 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. ** Detailed and Concrete Instructions @@ -39,37 +39,43 @@ Install Lean version 4. Install Emacs version 27 or later. -Install the Emacs packages Dash, Flycheck, lsp-mode and Magit-Section. -Dash is the only one of these packages that is available in the -default [[https://elpa.gnu.org][GNU Elpa]] package-archive. You can install the remaining three -packages either from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive. For later -approach, add the following to your Emacs initialization file +Install the Emacs packages Dash, lsp-mode and Magit-Section. Dash is +the only one of these packages that is available in the default [[https://elpa.gnu.org][GNU +Elpa]] package-archive. You can install the remaining packages either +from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive. For later approach, add +the following to your Emacs initialization file (e.g. =~/.emacs.d/init.el=): #+begin_src elisp (require 'package) + (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) -(package-initialize) -(let ((need-to-refresh t)) - (dolist (package '(dash flycheck lsp-mode magit-section)) - (unless (package-installed-p package) - (when need-to-refresh - (package-refresh-contents) - (setq need-to-refresh nil)) - (package-install package)))) + +(add-to-list 'package-selected-packages 'dash) +(add-to-list 'package-selected-packages 'lsp-mode) +(add-to-list 'package-selected-packages 'magit-section) + +(package-refresh-contents) +(package-install-selected-packages 'no-confirm) #+end_src Clone the Git repository of Lean4-Mode: #+begin_src shell -git clone https://github.com/leanprover-community/lean4-mode.git /path/to/lean4-mode +git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode #+end_src In your Emacs initialization file, add the path to your local -Lean4-Mode repository to the ~load-path~ list and load Lean4-Mode: +Lean4-Mode repository to the ~load-path~ list: +#+begin_src elisp +(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: #+begin_src elisp -(add-to-list 'load-path "/path/to/lean4-mode") (require 'lean4-mode) #+end_src @@ -93,17 +99,18 @@ since version 30, it also comes with a built-in =:vc= keyword for the packages from remote source repositories. #+begin_src elisp -;; Use Melpa as package archive: (require 'package) (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) (package-initialize) -;; Install Lean4-Mode: (use-package lean4-mode :commands lean4-mode :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :newest)) + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) #+end_src *** Doom-Emacs @@ -112,10 +119,10 @@ 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/lean4-mode" - :files ("*.el" "data"))) +(package! lean4-mode + :recipe (:host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) #+end_src *** Straight @@ -127,7 +134,7 @@ place the following code in your Emacs initialization file: (use-package lean4-mode :commands lean4-mode :straight (lean4-mode :type git :host github - :repo "leanprover/lean4-mode" + :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) #+end_src @@ -137,20 +144,12 @@ If things are working correctly, you should see the word "Lean 4" 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~. The mode-line will -show =FlyC:0/1=, indicating that there are no errors and one piece of -information displayed. +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 VS-Code) in a separate window. -If you want breadcrumbs of namespaces and sections to be shown in the -header-line, set the user option ~lsp-headerline-breadcrumb-enable~ to -~t~. - -* Key Bindings and Commands - | Key | Description | Command | |------------------------+--------------------------------------------------------+-----------------------------------| | =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | @@ -158,13 +157,37 @@ header-line, set the user option ~lsp-headerline-breadcrumb-enable~ to | =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~ | -|------------------------+--------------------------------------------------------+-----------------------------------| -| =C-c ! n= | Flycheck: Go to next error | ~flycheck-next-error~ | -| =C-c ! p= | Flycheck: Go to previous error | ~flycheck-previous-error~ | -For key bindings from ~lsp-mode~, see [[https://emacs-lsp.github.io/lsp-mode/page/keybindings/][its respective documentation]] and +** lsp-mode + +For key bindings from lsp-mode, see [[https://emacs-lsp.github.io/lsp-mode/page/keybindings/][its respective documentation]] and note that not all capabilities are supported by Lean4-Mode. -In the default configuration, the Flycheck annotation =FlyC:N/M= -indicates the number of errors (~N~) and responses (~M~) from Lean; -clicking on =FlyC= opens the Flycheck menu. +** Flycheck + +You may optionally use Lean4-Mode together with Flycheck. In that +case, the mode-line will show =FlyC:E/N=, indicating that there are +=E= number of errors and =N= number of notes. Following keys will be +available by default (via ~flycheck-mode-map~): + +| Key | Description | Command | +|-----------+----------------------+---------------------------| +| =C-c ! n= | Go to next error | ~flycheck-next-error~ | +| =C-c ! p= | Go to previous error | ~flycheck-previous-error~ | + +* Configuration + +** lsp-mode + +If you want breadcrumbs of namespaces and sections to be shown in the +header-line, set the user option ~lsp-headerline-breadcrumb-enable~ to +~t~. + +** Flycheck + +Flycheck is an optional but supported dependency of Lean4-Mode. If +Flycheck is installed, lsp-mode and thus Lean4-Mode will by default +use it. If you want to customize this behavior, e.g. if you'd like to +use Emacs' built-in Flymake package instead of Flycheck while keeping +later installed, then customize the ~lsp-diagnostics-provider~ user +option accordingly. diff --git a/lean4-debug.el b/lean4-debug.el index ac5342f..5d86a1c 100644 --- a/lean4-debug.el +++ b/lean4-debug.el @@ -1,25 +1,20 @@ -;;; lean4-debug.el --- Debug mode for lean4-mode -*- lexical-binding: t -*- +;;; lean4-debug.el --- Lean4-Mode Debug Mode -*- lexical-binding: t; -*- ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. -;; Author: Soonho Kong -;; SPDX-License-Identifier: Apache-2.0 - ;; This file is not part of GNU Emacs. -;;; License: - -;; 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: +;; 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. +;; 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: @@ -51,7 +46,7 @@ interactively." Print message \"lean: turn off debug mode\" if PRINT-MSG or if called interactively." (interactive) - (when (eq major-mode 'lean4-mode) + (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))) diff --git a/lean4-dev.el b/lean4-dev.el index a1b9619..f9cc5ba 100644 --- a/lean4-dev.el +++ b/lean4-dev.el @@ -1,25 +1,20 @@ -;;; lean4-dev.el --- Development commands for lean4-mode -*- lexical-binding: t -*- +;;; lean4-dev.el --- Lean4-Mode Development Commands -*- lexical-binding: t; -*- ;; Copyright (c) 2017 Microsoft Corporation. All rights reserved. -;; Author: Sebastian Ullrich -;; SPDX-License-Identifier: Apache-2.0 - ;; This file is not part of GNU Emacs. -;;; License: - -;; 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: +;; 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. +;; 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: diff --git a/lean4-eri.el b/lean4-eri.el index 85be9fa..a85b474 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -1,24 +1,27 @@ -;;; lean4-eri.el --- Enhanced relative indentation (eri) -*- lexical-binding: t -*- +;;; lean4-eri.el --- Lean4-Mode Indentation -*- lexical-binding: t; -*- -;; SPDX-License-Identifier: Apache-2.0 +;; Copyright (c) 2005-2010 Ulf Norell, Nils Anders Danielsson, +;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, +;; Marcin Benke, Darin Morrison. -;;; License: +;; 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: +;; 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. +;; 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: -;; Adapted from agda-mode (https://github.com/agda/agda/blob/master/src/data/emacs-mode/eri.el) +;; 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 ;;; Code: diff --git a/lean4-fringe.el b/lean4-fringe.el index b81ae8c..77490eb 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -1,29 +1,25 @@ -;;; lean4-fringe.el --- Show Lean processing progress in the editor fringe -*- lexical-binding: t; -*- -;; +;;; lean4-fringe.el --- Lean4-Mode Processing Progress in Fringe -*- lexical-binding: t; -*- + ;; Copyright (c) 2016 Microsoft Corporation. All rights reserved. -;; Released under Apache 2.0 license as described in the file LICENSE. -;; -;; Authors: Gabriel Ebner, Sebastian Ullrich -;; SPDX-License-Identifier: Apache-2.0 -;;; License: +;; 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: +;; 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. +;; 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: -;; + ;; Show Lean processing progress in the editor fringe -;; + ;;; Code: (require 'lean4-settings) diff --git a/lean4-info.el b/lean4-info.el index 5d6817f..3f6c928 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -1,28 +1,20 @@ -;;; lean4-info.el --- Emacs mode for Lean theorem prover -*- lexical-binding: t -*- -;; +;;; lean4-info.el --- Lean4-Mode Info View -*- lexical-binding: t; -*- + ;; Copyright (c) 2016 Gabriel Ebner. All rights reserved. -;; -;; Author: Gabriel Ebner -;; Maintainer: Gabriel Ebner -;; Created: Oct 29, 2016 -;; Keywords: languages -;; Version: 0.1 -;; URL: https://github.com/leanprover/lean4-mode -;; SPDX-License-Identifier: Apache-2.0 - -;;; License: - -;; 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: + +;; 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. +;; 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: @@ -38,14 +30,14 @@ (require 'magit-section) (defgroup lean4-info nil - "Lean Info." + "Lean4-Mode Info." :group 'lean) ;; Lean Info Mode (for "*lean4-info*" buffer) ;; Automode List ;;;###autoload (define-derived-mode lean4-info-mode prog-mode "Lean-Info" - "Major mode for Lean Info Buffer." + "Major mode for Lean4-Mode Info Buffer." :syntax-table lean4-syntax-table :group 'lean (set (make-local-variable 'font-lock-defaults) lean4-info-font-lock-defaults) @@ -73,7 +65,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (display-buffer buffer))) (defun lean4-info-buffer-active (buffer) - "Check whether the given info BUFFER should show info for the current buffer." + "Check whether given info BUFFER should show info for current buffer." (and ;; info buffer visible (on any frame) (get-buffer-window buffer t) @@ -252,8 +244,9 @@ Otherwise, is a timestamp as given by `current-time'.") 0.5 "Maximum time we are allowed to stagger debouncing. -If we recieve a request such that we have been debouncing for longer than -`lean4-info-buffer-debounce-begin-time', then we immediately run the request." +If we recieve a request such that we have been debouncing for longer +than `lean4-info-buffer-debounce-begin-time', then we immediately run +the request." :group 'lean4-info :type 'number) @@ -261,8 +254,10 @@ If we recieve a request such that we have been debouncing for longer than ;; 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'. -This version ensures that info buffer is not repeatedly written to. This is to -prevent lag, because magit is quite slow at building sections." + +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 (not lean4-info-buffer-debounce-begin-time) (setq lean4-info-buffer-debounce-begin-time (current-time))) diff --git a/lean4-input.el b/lean4-input.el index 040e7f7..14c7a10 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -1,40 +1,42 @@ -;;; lean4-input.el --- The Lean input method (based/copied from Agda) -*- lexical-binding: t -*- -;;; -;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language. -;;; We did minor modifications -;; SPDX-License-Identifier: Apache-2.0 -;; +;;; lean4-input.el --- Lean4-Mode Input Method -*- lexical-binding: t; -*- + +;; Copyright (c) 2005-2012 Ulf Norell, Nils Anders Danielsson, +;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, +;; Marcin Benke, Darin Morrison. -;;; License: +;; 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: +;; 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. +;; 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: -;; -;;;; A highly customisable input method which can inherit from other + +;; 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. -;; + ;; 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 lean4-input-show-translations to see all the characters which ;; can be typed using this input method (except for those ;; corresponding to ASCII characters). +;; This file is based on agda-input.el from Agda-Mode: +;; https://github.com/agda/agda/blob/d2cbd2dd4f49fa84c5ca6fcf464c3211adcc0088/src/data/emacs-mode/agda-input.el + ;;; Code: (require 'quail) @@ -182,7 +184,7 @@ order for the change to take effect." (defcustom lean4-input-data-directory (expand-file-name "data/" (file-name-directory (or load-file-name (buffer-file-name)))) - "Directory in which translations.json resides." + "Directory in which abbreviations.json resides." :group 'lean4-input :type 'directory) @@ -306,10 +308,7 @@ Suitable for use in the :set field of `defcustom'." (lean4-input-setup)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Administrative details - -(provide 'lean4-input) -;;; lean4-input.el ends here +;; Export Translations (defun lean4-input-export-translations () "Export the current translations in a javascript format. @@ -338,3 +337,9 @@ leanprover.github.io/tutorial/js/input-method.js" (lean4-input-export-translations) (with-current-buffer "*lean4-translations*" (princ (buffer-string)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Administrative details + +(provide 'lean4-input) +;;; lean4-input.el ends here diff --git a/lean4-lake.el b/lean4-lake.el index 37d32df..bfca627 100644 --- a/lean4-lake.el +++ b/lean4-lake.el @@ -1,21 +1,18 @@ -;;; lean4-lake.el --- Lake integration for lean4-mode -*- lexical-binding: t -*- +;;; lean4-lake.el --- Lean4-Mode Lake Integration -*- lexical-binding: t; -*- -;; SPDX-License-Identifier: Apache-2.0 ;; This file is not part of GNU Emacs. -;;; License: - -;; 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: +;; 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. +;; 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: diff --git a/lean4-mode.el b/lean4-mode.el index fb52fa5..fed60a9 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -1,4 +1,4 @@ -;;; lean4-mode.el --- A major mode for the Lean language -*- lexical-binding: t -*- +;;; lean4-mode.el --- Major mode for Lean language -*- lexical-binding: t; -*- ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. ;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved. @@ -10,24 +10,24 @@ ;; Maintainer: Yury G. Kudryashov ;; Created: Jan 09, 2014 ;; Keywords: languages -;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0")) -;; URL: https://github.com/leanprover/lean4-mode +;; Package-Requires: ((emacs "27.1") (compat "28.1") (dash "2.18.0") (magit-section "2.90.1") (lsp-mode "8.0.0")) +;; URL: https://github.com/leanprover-community/lean4-mode ;; SPDX-License-Identifier: Apache-2.0 -;; Version: 1.0.1 +;; Version: 1.1.0 -;;; License: +;; 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: +;; 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. +;; 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: @@ -44,7 +44,6 @@ (require 'cl-lib) (require 'dash) (require 'pcase) -(require 'flycheck) (require 'lsp-mode) (require 'lean4-eri) (require 'lean4-util) @@ -55,12 +54,17 @@ (require 'lean4-fringe) (require 'lean4-lake) -;; Silence byte-compiler +;; Declare symbols defined in external dependencies. This silences +;; 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) -(defvar compilation-mode-font-lock-keywords) -(declare-function lean-mode "ext:lean-mode") +(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) @@ -153,11 +157,15 @@ file, recompiling, and reloading all imports." (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] - ["List of errors" flycheck-list-errors flycheck-mode] - ["Restart lean process" lsp-workspace-restart t] - ["Customize lean4-mode" (customize-group 'lean) t])) + ["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 '( @@ -203,12 +211,11 @@ of the parent project." (when root (lsp-workspace-folders-add root)))) -;; Automode List ;;;###autoload (define-derived-mode lean4-mode prog-mode "Lean 4" - "Major mode for Lean. -\\{lean4-mode-map} -Invokes `lean4-mode-hook'." + "Major mode for Lean language. + +\\{lean4-mode-map}" :syntax-table lean4-syntax-table :abbrev-table lean4-abbrev-table :group 'lean @@ -256,11 +263,13 @@ Invokes `lean4-mode-hook'." ;; Automatically use lean4-mode for .lean files. ;;;###autoload -(push '("\\.lean$" . lean4-select-mode) auto-mode-alist) +(add-to-list 'auto-mode-alist + '("\\.lean\\'" . lean4-select-mode)) ;;;###autoload (with-eval-after-load 'markdown-mode - (add-to-list 'markdown-code-lang-modes '("lean" . lean4-select-mode))) + (add-to-list 'markdown-code-lang-modes + '("lean" . lean4-select-mode))) ;; Use utf-8 encoding ;;;### autoload @@ -288,7 +297,5 @@ otherwise return '/path/to/lean --server'." :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) -(add-hook 'lean4-mode-hook #'lsp) - (provide 'lean4-mode) ;;; lean4-mode.el ends here diff --git a/lean4-mode.info b/lean4-mode.info index 6966f13..a46a9b8 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -3,18 +3,18 @@ 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 Lean language. END-INFO-DIR-ENTRY  File: lean4-mode.info, Node: Top, Next: Installation, Up: (dir) -Lean4-Mode - Emacs major-mode for Lean language +Lean4-Mode - Emacs major mode for Lean language *********************************************** -This package extends GNU Emacs by providing a major-mode for editing -code written in version 4 of the programming language and theorem prover -Lean. +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). The Lean4-Mode source code is developed at Github (https://github.com/leanprover-community/lean4-mode) and its issues @@ -31,7 +31,7 @@ _Lean-Mode_). * Installation:: * Usage:: -* Key Bindings and Commands:: +* Configuration:: -- The Detailed Node Listing -- @@ -47,6 +47,16 @@ Instructions for Source-Based Use-Package * Doom-Emacs:: * Straight:: +Usage + +* lsp-mode:: +* Flycheck:: + +Configuration + +* lsp-mode: lsp-mode (1). +* Flycheck: Flycheck (1). +  File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top @@ -66,23 +76,21 @@ File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed an 1.1 Brief and Generic Instructions ================================== -Install dependencies: - • Lean version 4 (https://lean-lang.org/lean4/doc/setup.html) - • Emacs version 27 or later - • Emacs packages Dash (https://github.com/magnars/dash.el) (which is - available on GNU-Elpa package-archive), Flycheck - (https://www.flycheck.org), lsp-mode - (https://emacs-lsp.github.io/lsp-mode) and Magit-Section +First, install the dependencies of Lean4-Mode: + • Lean (https://lean-lang.org/lean4/doc/setup.html) (version 4) + • Emacs (version 27 or later) + • Emacs packages Dash (https://github.com/magnars/dash.el) (available + on GNU-Elpa), lsp-mode (https://emacs-lsp.github.io/lsp-mode), and + Magit-Section (https://github.com/magit/magit/blob/main/lisp/magit-section.el) - (which are available on Melpa package-archive) + (available on Melpa) - Install Lean4-Mode: + Second, install Lean4-Mode itself: • Clone the Git repository of Lean4-Mode (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 and - • load Lean4-Mode with ‘(require 'lean4-mode)’. + add the path to that local repository to the ‘load-path’ list.  File: lean4-mode.info, Node: Detailed and Concrete Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief and Generic Instructions, Up: Installation @@ -94,33 +102,37 @@ Install Lean version 4. Install Emacs version 27 or later. - Install the Emacs packages Dash, Flycheck, lsp-mode and -Magit-Section. Dash is the only one of these packages that is available -in the default GNU Elpa (https://elpa.gnu.org) package-archive. You can -install the remaining three packages either from source or from Melpa + Install the Emacs packages Dash, lsp-mode and Magit-Section. Dash is +the only one of these packages that is available in the default GNU Elpa +(https://elpa.gnu.org) package-archive. You can install the remaining +packages either from source or from Melpa (https://melpa.org/#/getting-started) package-archive. For later approach, add the following to your Emacs initialization file (e.g. ‘~/.emacs.d/init.el’): (require 'package) + (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) - (package-initialize) - (let ((need-to-refresh t)) - (dolist (package '(dash flycheck lsp-mode magit-section)) - (unless (package-installed-p package) - (when need-to-refresh - (package-refresh-contents) - (setq need-to-refresh nil)) - (package-install package)))) + + (add-to-list 'package-selected-packages 'dash) + (add-to-list 'package-selected-packages 'lsp-mode) + (add-to-list 'package-selected-packages 'magit-section) + + (package-refresh-contents) + (package-install-selected-packages 'no-confirm) Clone the Git repository of Lean4-Mode: - git clone https://github.com/leanprover-community/lean4-mode.git /path/to/lean4-mode + git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode In your Emacs initialization file, add the path to your local -Lean4-Mode repository to the ‘load-path’ list and load Lean4-Mode: - (add-to-list 'load-path "/path/to/lean4-mode") +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: (require 'lean4-mode)  @@ -156,17 +168,18 @@ since version 30, it also 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. - ;; Use Melpa as package archive: (require 'package) (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) (package-initialize) - ;; Install Lean4-Mode: (use-package lean4-mode :commands lean4-mode :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :newest)) + :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 @@ -177,10 +190,10 @@ File: lean4-mode.info, Node: Doom-Emacs, Next: Straight, Prev: Native vc (Ema If you use Doom-Emacs, you can place the following code in your Doom initialization file: - (package! lean4-mode :recipe - (:host github - :repo "leanprover/lean4-mode" - :files ("*.el" "data"))) + (package! lean4-mode + :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 @@ -194,11 +207,11 @@ the following code in your Emacs initialization file: (use-package lean4-mode :commands lean4-mode :straight (lean4-mode :type git :host github - :repo "leanprover/lean4-mode" + :repo "leanprover-community/lean4-mode" :files ("*.el" "data")))  -File: lean4-mode.info, Node: Usage, Next: Key Bindings and Commands, Prev: Installation, Up: Top +File: lean4-mode.info, Node: Usage, Next: Configuration, Prev: Installation, Up: Top 2 Usage ******* @@ -207,24 +220,12 @@ If things are working correctly, you should see the word "Lean 4" 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’. The mode-line will show -‘FlyC:0/1’, indicating that there are no errors and one piece of -information displayed. +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 VS-Code) in a separate window. - If you want breadcrumbs of namespaces and sections to be shown in the -header-line, set the user option ‘lsp-headerline-breadcrumb-enable’ to -‘t’. - - -File: lean4-mode.info, Node: Key Bindings and Commands, Prev: Usage, Up: Top - -3 Key Bindings and Commands -*************************** - Key Description Command ---------------------------------------------------------------------------------------------------------------------- ‘C-c C-k’ Echo the keystroke needed to input the symbol at point ‘quail-show-key’ @@ -232,30 +233,89 @@ Key Description ‘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’ -‘C-c ! n’ Flycheck: Go to next error ‘flycheck-next-error’ -‘C-c ! p’ Flycheck: Go to previous error ‘flycheck-previous-error’ - For key bindings from ‘lsp-mode’, see its respective documentation +* Menu: + +* lsp-mode:: +* Flycheck:: + + +File: lean4-mode.info, Node: lsp-mode, Next: Flycheck, Up: Usage + +2.1 lsp-mode +============ + +For key bindings from lsp-mode, see its respective documentation (https://emacs-lsp.github.io/lsp-mode/page/keybindings/) and note that not all capabilities are supported by Lean4-Mode. - In the default configuration, the Flycheck annotation ‘FlyC:N/M’ -indicates the number of errors (‘N’) and responses (‘M’) from Lean; -clicking on ‘FlyC’ opens the Flycheck menu. + +File: lean4-mode.info, Node: Flycheck, Prev: lsp-mode, Up: Usage + +2.2 Flycheck +============ + +You may optionally use Lean4-Mode together with Flycheck. In that case, +the mode-line will show ‘FlyC:E/N’, indicating that there are ‘E’ number +of errors and ‘N’ number of notes. Following keys will be available by +default (via ‘flycheck-mode-map’): + +Key Description Command +--------------------------------------------------------------- +‘C-c ! n’ Go to next error ‘flycheck-next-error’ +‘C-c ! p’ Go to previous error ‘flycheck-previous-error’ + + +File: lean4-mode.info, Node: Configuration, Prev: Usage, Up: Top + +3 Configuration +*************** + +* Menu: + +* lsp-mode: lsp-mode (1). +* Flycheck: Flycheck (1). + + +File: lean4-mode.info, Node: lsp-mode (1), Next: Flycheck (1), Up: Configuration + +3.1 lsp-mode +============ + +If you want breadcrumbs of namespaces and sections to be shown in the +header-line, set the user option ‘lsp-headerline-breadcrumb-enable’ to +‘t’. + + +File: lean4-mode.info, Node: Flycheck (1), Prev: lsp-mode (1), Up: Configuration + +3.2 Flycheck +============ + +Flycheck is an optional but supported dependency of Lean4-Mode. If +Flycheck is installed, lsp-mode and thus Lean4-Mode will by default use +it. If you want to customize this behavior, e.g. if you'd like to use +Emacs' built-in Flymake package instead of Flycheck while keeping later +installed, then customize the ‘lsp-diagnostics-provider’ user option +accordingly.  Tag Table: Node: Top223 -Node: Installation1324 -Node: Brief and Generic Instructions1567 -Node: Detailed and Concrete Instructions2624 -Node: Instructions for Source-Based Use-Package4178 -Node: Native vc (Emacs 30 or later)4899 -Node: Doom-Emacs5752 -Node: Straight6152 -Node: Usage6642 -Node: Key Bindings and Commands7562 +Node: Installation1476 +Node: Brief and Generic Instructions1719 +Node: Detailed and Concrete Instructions2668 +Node: Instructions for Source-Based Use-Package4325 +Node: Native vc (Emacs 30 or later)5046 +Node: Doom-Emacs5954 +Node: Straight6380 +Node: Usage6880 +Node: lsp-mode8326 +Node: Flycheck8611 +Node: Configuration9221 +Node: lsp-mode (1)9387 +Node: Flycheck (1)9656  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 9b5cd44..c4f92c7 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -1,30 +1,30 @@ \input texinfo @c -*- texinfo -*- @c %**start of header @setfilename lean4-mode.info -@settitle Lean4-Mode - Emacs major-mode for Lean language +@settitle Lean4-Mode - Emacs major mode for Lean language @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 Lean language. @end direntry @finalout @titlepage -@title Lean4-Mode - Emacs major-mode for Lean language +@title Lean4-Mode - Emacs major mode for Lean language @end titlepage @contents @ifnottex @node Top -@top Lean4-Mode - Emacs major-mode for Lean language +@top Lean4-Mode - Emacs major mode for Lean language -This package extends GNU Emacs by providing a major-mode for editing +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 Lean. +prover @uref{https://lean-lang.org, Lean}. 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 @@ -38,7 +38,7 @@ known as @emph{Lean-Mode}). @menu * Installation:: * Usage:: -* Key Bindings and Commands:: +* Configuration:: @detailmenu --- The Detailed Node Listing --- @@ -55,6 +55,16 @@ Instructions for Source-Based Use-Package * Doom-Emacs:: * Straight:: +Usage + +* lsp-mode:: +* Flycheck:: + +Configuration + +* lsp-mode: lsp-mode (1). +* Flycheck: Flycheck (1). + @end detailmenu @end menu @@ -70,27 +80,24 @@ Instructions for Source-Based Use-Package @node Brief and Generic Instructions @section Brief and Generic Instructions -Install dependencies: +First, install the dependencies of Lean4-Mode: @itemize @item -@uref{https://lean-lang.org/lean4/doc/setup.html, Lean version 4} +@uref{https://lean-lang.org/lean4/doc/setup.html, Lean} (version 4) @item -Emacs version 27 or later +Emacs (version 27 or later) @item -Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (which is available on GNU-Elpa -package-archive), @uref{https://www.flycheck.org, Flycheck}, @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} (which are -available on Melpa package-archive) +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 -Install Lean4-Mode: +Second, install Lean4-Mode itself: @itemize @item Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository of Lean4-Mode}. @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 and -@item -load Lean4-Mode with @samp{(require 'lean4-mode)}. +repository to the @code{load-path} list. @end itemize @node Detailed and Concrete Instructions @@ -100,37 +107,43 @@ Install Lean version 4. Install Emacs version 27 or later. -Install the Emacs packages Dash, Flycheck, lsp-mode and Magit-Section. -Dash is the only one of these packages that is available in the -default @uref{https://elpa.gnu.org, GNU Elpa} package-archive. You can install the remaining three -packages either from source or from @uref{https://melpa.org/#/getting-started, Melpa} package-archive. For later -approach, add the following to your Emacs initialization file +Install the Emacs packages Dash, lsp-mode and Magit-Section. Dash is +the only one of these packages that is available in the default @uref{https://elpa.gnu.org, GNU +Elpa} package-archive. You can install the remaining packages either +from source or from @uref{https://melpa.org/#/getting-started, Melpa} package-archive. For later approach, add +the following to your Emacs initialization file (e.g. @samp{~/.emacs.d/init.el}): @lisp (require 'package) + (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) -(package-initialize) -(let ((need-to-refresh t)) - (dolist (package '(dash flycheck lsp-mode magit-section)) - (unless (package-installed-p package) - (when need-to-refresh - (package-refresh-contents) - (setq need-to-refresh nil)) - (package-install package)))) + +(add-to-list 'package-selected-packages 'dash) +(add-to-list 'package-selected-packages 'lsp-mode) +(add-to-list 'package-selected-packages 'magit-section) + +(package-refresh-contents) +(package-install-selected-packages 'no-confirm) @end lisp Clone the Git repository of Lean4-Mode: @example -git clone https://github.com/leanprover-community/lean4-mode.git /path/to/lean4-mode +git clone https://github.com/leanprover-community/lean4-mode.git ~/path/to/lean4-mode @end example In your Emacs initialization file, add the path to your local -Lean4-Mode repository to the @code{load-path} list and load Lean4-Mode: +Lean4-Mode repository to the @code{load-path} list: +@lisp +(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: @lisp -(add-to-list 'load-path "/path/to/lean4-mode") (require 'lean4-mode) @end lisp @@ -162,17 +175,18 @@ since version 30, it also comes with a built-in @samp{:vc} keyword for the packages from remote source repositories. @lisp -;; Use Melpa as package archive: (require 'package) (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) (package-initialize) -;; Install Lean4-Mode: (use-package lean4-mode :commands lean4-mode :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :newest)) + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) @end lisp @node Doom-Emacs @@ -182,10 +196,10 @@ 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/lean4-mode" - :files ("*.el" "data"))) +(package! lean4-mode + :recipe (:host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) @end lisp @node Straight @@ -198,7 +212,7 @@ place the following code in your Emacs initialization file: (use-package lean4-mode :commands lean4-mode :straight (lean4-mode :type git :host github - :repo "leanprover/lean4-mode" + :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) @end lisp @@ -209,21 +223,12 @@ If things are working correctly, you should see the word "Lean 4" 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}. The mode-line will -show @samp{FlyC:0/1}, indicating that there are no errors and one piece of -information displayed. +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 in VS-Code) in a separate window. -If you want breadcrumbs of namespaces and sections to be shown in the -header-line, set the user option @code{lsp-headerline-breadcrumb-enable} to -@code{t}. - -@node Key Bindings and Commands -@chapter Key Bindings and Commands - @multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} @headitem Key @tab Description @@ -243,19 +248,62 @@ header-line, set the user option @code{lsp-headerline-breadcrumb-enable} to @item @samp{C-c C-i} @tab Toggle Info-View which shows goals and errors at point @tab @code{lean4-toggle-info-buffer} +@end multitable + +@menu +* lsp-mode:: +* Flycheck:: +@end menu + +@node lsp-mode +@section lsp-mode + +For key bindings from lsp-mode, see @uref{https://emacs-lsp.github.io/lsp-mode/page/keybindings/, its respective documentation} and +note that not all capabilities are supported by Lean4-Mode. + +@node Flycheck +@section Flycheck + +You may optionally use Lean4-Mode together with Flycheck. In that +case, the mode-line will show @samp{FlyC:E/N}, indicating that there are +@samp{E} number of errors and @samp{N} number of notes. Following keys will be +available by default (via @code{flycheck-mode-map}): + +@multitable {aaaaaaaaa} {aaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaa} +@headitem Key +@tab Description +@tab Command @item @samp{C-c ! n} -@tab Flycheck: Go to next error +@tab Go to next error @tab @code{flycheck-next-error} @item @samp{C-c ! p} -@tab Flycheck: Go to previous error +@tab Go to previous error @tab @code{flycheck-previous-error} @end multitable -For key bindings from @code{lsp-mode}, see @uref{https://emacs-lsp.github.io/lsp-mode/page/keybindings/, its respective documentation} and -note that not all capabilities are supported by Lean4-Mode. +@node Configuration +@chapter Configuration + +@menu +* lsp-mode: lsp-mode (1). +* Flycheck: Flycheck (1). +@end menu + +@node lsp-mode (1) +@section lsp-mode + +If you want breadcrumbs of namespaces and sections to be shown in the +header-line, set the user option @code{lsp-headerline-breadcrumb-enable} to +@code{t}. + +@node Flycheck (1) +@section Flycheck -In the default configuration, the Flycheck annotation @samp{FlyC:N/M} -indicates the number of errors (@code{N}) and responses (@code{M}) from Lean; -clicking on @samp{FlyC} opens the Flycheck menu. +Flycheck is an optional but supported dependency of Lean4-Mode. If +Flycheck is installed, lsp-mode and thus Lean4-Mode will by default +use it. If you want to customize this behavior, e.g. if you'd like to +use Emacs' built-in Flymake package instead of Flycheck while keeping +later installed, then customize the @code{lsp-diagnostics-provider} user +option accordingly. @bye diff --git a/lean4-settings.el b/lean4-settings.el index 53cd9ed..a7165db 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -1,25 +1,20 @@ -;;; lean4-settings.el --- Custom variables for lean4-mode -*- lexical-binding: t -*- +;;; lean4-settings.el --- Lean4-Mode User-Options -*- lexical-binding: t; -*- ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. -;; Released under Apache 2.0 license as described in the file LICENSE. -;; -;; Author: Soonho Kong -;; SPDX-License-Identifier: Apache-2.0 -;; -;;; License: +;; 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: +;; 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. +;; 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: @@ -28,13 +23,17 @@ ;;; Code: (require 'cl-lib) +(require 'lsp-mode) (defgroup lean4 nil - "Lean 4 programming language and theorem prover." - :prefix "lean4-" + "Major mode for Lean4 programming language and theorem prover." :group 'languages - :link '(url-link :tag "Website" "http://leanprover.github.io") - :link '(url-link :tag "Github" "https://github.com/leanprover/lean4")) + :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." @@ -53,6 +52,12 @@ (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 'lean diff --git a/lean4-syntax.el b/lean4-syntax.el index 39b41b0..26b7fd1 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -1,25 +1,20 @@ -;;; lean4-syntax.el --- Syntax definitions for lean4-mode -*- lexical-binding: t -*- +;;; lean4-syntax.el --- Lean4-Mode Syntax Definitions -*- lexical-binding: t; -*- ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. -;; Released under Apache 2.0 license as described in the file LICENSE. -;; -;; Author: Leonardo de Moura -;; Soonho Kong -;; SPDX-License-Identifier: Apache-2.0 -;;; License: +;; 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: +;; 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. +;; 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: diff --git a/lean4-util.el b/lean4-util.el index 77d2ebd..273a530 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -1,24 +1,20 @@ -;;; lean4-util.el --- Utilities for lean4-mode -*- lexical-binding: t -*- +;;; lean4-util.el --- Lean4-Mode Utilities -*- lexical-binding: t; -*- ;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. -;; Released under Apache 2.0 license as described in the file LICENSE. -;; -;; Author: Soonho Kong -;; SPDX-License-Identifier: Apache-2.0 -;;; License: +;; 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: +;; 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. +;; 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: @@ -26,6 +22,7 @@ ;;; Code: +(require 'compat) (require 'lean4-settings) (defun lean4-setup-rootdir () @@ -56,8 +53,7 @@ First try to find an executable named `lean4-executable-name' in (defun lean4-get-executable (exe-name) "Return fullpath of lean executable EXE-NAME." - (let ((default-directory (lean4-get-rootdir))) - (expand-file-name exe-name (expand-file-name "bin")))) + (file-name-concat (lean4-get-rootdir) "bin" exe-name)) (defun lean4-whitespace-cleanup () "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t."