From 0294c65e36ea0f7fc622a3dc2d92d032864455a9 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sun, 17 Nov 2024 22:50:46 +0100 Subject: [PATCH 01/15] New CHANGELOG.org --- CHANGELOG.org | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 CHANGELOG.org diff --git a/CHANGELOG.org b/CHANGELOG.org new file mode 100644 index 0000000..adec67c --- /dev/null +++ b/CHANGELOG.org @@ -0,0 +1,8 @@ +#+title: Lean4-Mode - Changelog +#+language: en + +* Development + +* Version 1.0 + +- Specify "Version" in Emacs-Lisp library header. From 204ce97786eb7ad0d44e145e58cb097daef67435 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sat, 16 Nov 2024 01:43:39 +0100 Subject: [PATCH 02/15] Release version 1.0.0 Fixes issue #78 "Specification of lean4-mode version". --- lean4-mode.el | 1 + 1 file changed, 1 insertion(+) diff --git a/lean4-mode.el b/lean4-mode.el index 6224911..4220e3d 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -13,6 +13,7 @@ ;; 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 ;; SPDX-License-Identifier: Apache-2.0 +;; Version: 1.0.0 ;;; License: From 307d93e3ddbc4e9325930ea4c6c90ccce4a204e8 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sat, 16 Nov 2024 01:54:40 +0100 Subject: [PATCH 03/15] Upgrade Python in Github workflow Melpazoid Fixes issue #79 "Repair 'Melpazoid' workflow". --- .github/workflows/melpazoid.yml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/workflows/melpazoid.yml b/.github/workflows/melpazoid.yml index a19380b..4e0d05b 100644 --- a/.github/workflows/melpazoid.yml +++ b/.github/workflows/melpazoid.yml @@ -10,10 +10,11 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - name: Set up Python 3.9 - uses: actions/setup-python@v1 - with: { python-version: 3.9 } + - uses: actions/checkout@v3 + - name: Set up Python 3.10 + uses: actions/setup-python@v4 + with: + python-version: '3.10' - name: Install run: | python -m pip install --upgrade pip From f2d4bcdaee6799255f6b91c3d24fe0610b09ae39 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sat, 16 Nov 2024 01:38:55 +0100 Subject: [PATCH 04/15] Specify Yury as current maintainer Fixes issue #74 "Correct specification of current maintainer". --- lean4-mode.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-mode.el b/lean4-mode.el index 4220e3d..80b8066 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -7,7 +7,7 @@ ;; Soonho Kong ;; Gabriel Ebner ;; Sebastian Ullrich -;; Maintainer: Sebastian Ullrich +;; 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")) From 12d1ba86240ae883e1bbc3fbeae11f0e2ac121fd Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sun, 17 Nov 2024 00:18:09 +0100 Subject: [PATCH 05/15] README: Rename from .md to .org --- README.md => README.org | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename README.md => README.org (100%) diff --git a/README.md b/README.org similarity index 100% rename from README.md rename to README.org From f0e9cee3c865c8ad7ba43c2b32585766d94268d0 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sun, 17 Nov 2024 00:19:57 +0100 Subject: [PATCH 06/15] README: Translate from Markdown to Org --- README.org | 78 +++++++++++++++++++++++++++--------------------------- 1 file changed, 39 insertions(+), 39 deletions(-) diff --git a/README.org b/README.org index b67dcc6..9db3148 100644 --- a/README.org +++ b/README.org @@ -1,10 +1,11 @@ -Installation -============ +#+title: ~lean4-mode~ - An Emacs major-mode for the Lean language -Before using this major mode, you need to [install Lean 4](https://leanprover.github.io/lean4/doc/setup.html#basic-setup). +* Installation -To use `lean4-mode` in Emacs, add the following to your `init.el`: -``` +Before using this major mode, you need to [[https://leanprover.github.io/lean4/doc/setup.html#basic-setup][install Lean 4]]. + +To use ~lean4-mode~ in Emacs, add the following to your =init.el=: +#+begin_src elisp ;; You need to modify the following line (setq load-path (cons "/path/to/lean4-mode" load-path)) @@ -22,10 +23,11 @@ To use `lean4-mode` in Emacs, add the following to your `init.el`: (package-install p)))) (require 'lean4-mode) -``` -Alternatively if you are a fan of `use-package` and `straight.el` you +#+end_src + +Alternatively if you are a fan of ~use-package~ and =straight.el= you can use: -``` +#+begin_src elisp (use-package lean4-mode :straight (lean4-mode :type git @@ -34,51 +36,49 @@ can use: :files ("*.el" "data")) ;; to defer loading the package until required :commands (lean4-mode)) -``` -If you are a doom-emacs user, adding the following to `packages.el` should work: -``` +#+end_src + +If you are a doom-emacs user, adding the following to =packages.el= should work: +#+begin_src elisp (package! lean4-mode :recipe (:host github :repo "leanprover/lean4-mode" :files ("*.el" "data"))) -``` +#+end_src -Trying It Out -============= +* Trying It Out -If things are working correctly, you should see the word ``Lean 4`` in the -Emacs mode line when you open a file with extension `.lean`. Emacs will ask you +If things are working correctly, you should see the word "Lean 4" in the +Emacs mode line when you open a file with extension =.lean=. Emacs will ask you to identify the "project" this file belongs to. If you then type -```lean +#+begin_src lean #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 +#+end_src +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. -To view the proof state, run `lean4-toggle-info` (`C-c` `C-i`). This will show the `*Lean Goals*` buffer (like the `Lean infoview` pane in VSCode) in a separate window. +To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This will show the =*Lean Goals*= buffer (like the =Lean infoview= pane in VSCode) in a separate window. -Settings -======== +* Settings -Set these with e.g. `M-x customize-variable`. +Set these with e.g. =M-x customize-variable=. -* `lsp-headerline-breadcrumb-enable`: show a "breadcrumb bar" of namespaces and sections surrounding the current location (default: off) +- ~lsp-headerline-breadcrumb-enable~: show a "breadcrumb bar" of namespaces and sections surrounding the current location (default: off) -Key Bindings and Commands -========================= +* Key Bindings and Commands -| Key | Function | -|--------------------|---------------------------------------------------------------------------------| -| C-c C-k | show the keystroke needed to input the symbol under the cursor | -| C-c C-d | recompile & reload imports (`lean4-refresh-file-dependencies`) | -| C-c C-x | 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 showing goals and errors at point (`lean4-toggle-info-buffer`) | -| C-c ! n | flycheck: go to next error | -| C-c ! p | flycheck: go to previous error | +| Key | Function | +|---------------+---------------------------------------------------------------------------------| +| =C-c C-k= | show the keystroke needed to input the symbol under the cursor | +| =C-c C-d= | recompile & reload imports (~lean4-refresh-file-dependencies~) | +| =C-c C-x= | 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 showing goals and errors at point (~lean4-toggle-info-buffer~) | +| =C-c ! n= | flycheck: go to next error | +| =C-c ! p= | flycheck: go to previous error | -For `lsp-mode` bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently). +For ~lsp-mode~ bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently). -In the default configuration, the Flycheck annotation `FlyC:n/n` indicates the -number of errors / responses from Lean; clicking on `FlyC` opens the Flycheck menu. +In the default configuration, the Flycheck annotation =FlyC:n/n= indicates the +number of errors / responses from Lean; clicking on =FlyC= opens the Flycheck menu. From 84552033c56bb20b687791a84b89906620814b2b Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sun, 17 Nov 2024 00:21:29 +0100 Subject: [PATCH 07/15] README: Re-fill text paragraphs --- README.org | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/README.org b/README.org index 9db3148..2a8858c 100644 --- a/README.org +++ b/README.org @@ -38,7 +38,8 @@ can use: :commands (lean4-mode)) #+end_src -If you are a doom-emacs user, adding the following to =packages.el= should work: +If you are a doom-emacs user, adding the following to =packages.el= +should work: #+begin_src elisp (package! lean4-mode :recipe (:host github @@ -48,23 +49,28 @@ If you are a doom-emacs user, adding the following to =packages.el= should work: * Trying It Out -If things are working correctly, you should see the word "Lean 4" in the -Emacs mode line when you open a file with extension =.lean=. Emacs will ask you -to identify the "project" this file belongs to. If you then type +If things are working correctly, you should see the word "Lean 4" in +the Emacs mode line when you open a file with extension =.lean=. +Emacs will ask you to identify the "project" this file belongs to. If +you then type #+begin_src lean #check id #+end_src 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 +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. -To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This will show the =*Lean Goals*= buffer (like the =Lean infoview= pane in VSCode) in a separate window. +To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This +will show the =*Lean Goals*= buffer (like the =Lean infoview= pane in +VSCode) in a separate window. * Settings Set these with e.g. =M-x customize-variable=. -- ~lsp-headerline-breadcrumb-enable~: show a "breadcrumb bar" of namespaces and sections surrounding the current location (default: off) +- ~lsp-headerline-breadcrumb-enable~: Show a "breadcrumb bar" of + namespaces and sections surrounding the current location (default: + off) * Key Bindings and Commands @@ -78,7 +84,10 @@ Set these with e.g. =M-x customize-variable=. | =C-c ! n= | flycheck: go to next error | | =C-c ! p= | flycheck: go to previous error | -For ~lsp-mode~ bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all capabilities are supported currently). +For ~lsp-mode~ bindings, see +https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all +capabilities are supported currently). -In the default configuration, the Flycheck annotation =FlyC:n/n= indicates the -number of errors / responses from Lean; clicking on =FlyC= opens the Flycheck menu. +In the default configuration, the Flycheck annotation =FlyC:n/n= +indicates the number of errors / responses from Lean; clicking on +=FlyC= opens the Flycheck menu. From 7083b46238660ab96ac18493b2a9bf2c505d9d2d Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Sun, 17 Nov 2024 01:34:22 +0100 Subject: [PATCH 08/15] README: Add preamble. Rework Installation section. --- README.org | 153 ++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 111 insertions(+), 42 deletions(-) diff --git a/README.org b/README.org index 2a8858c..f3b4cf1 100644 --- a/README.org +++ b/README.org @@ -1,45 +1,105 @@ #+title: ~lean4-mode~ - An Emacs major-mode for the 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. + +For version 3 of Lean, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (formerly known as /Lean-Mode/). + * Installation -Before using this major mode, you need to [[https://leanprover.github.io/lean4/doc/setup.html#basic-setup][install Lean 4]]. +** Brief and Generic Instructions -To use ~lean4-mode~ in Emacs, add the following to your =init.el=: -#+begin_src elisp -;; You need to modify the following line -(setq load-path (cons "/path/to/lean4-mode" load-path)) +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]], [[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 the Melpa package-archive) + +Install Lean4-Mode: +- 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)=. -(setq lean4-mode-required-packages '(dash flycheck lsp-mode magit-section)) +** Detailed and Concrete Instructions +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 +(e.g. =~/.emacs.d/init.el=): + +#+begin_src elisp (require 'package) -(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/")) +(add-to-list 'package-archives + '("melpa" . "https://melpa.org/packages/")) (package-initialize) (let ((need-to-refresh t)) - (dolist (p lean4-mode-required-packages) - (when (not (package-installed-p p)) + (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 p)))) + (package-install package)))) +#+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 +#+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: +#+begin_src elisp +(add-to-list 'load-path "/path/to/lean4-mode") (require 'lean4-mode) #+end_src -Alternatively if you are a fan of ~use-package~ and =straight.el= you -can use: +** Instructions for Source-Based Use-Package + +If you use a source-based package-manager (e.g. =package-vc.el=, +Straight or Elpaca), then make sure to list the ="data"= directory in +your Lean4-Mode package recipe. + +If you use the ~use-package~ macro and intent to defer loading of +packages in order to improve your Emacs startup time, then make sure +to specify ~lean4-mode~ as a =:command=. + +Following subsections show concrete examples. + +*** Native =:vc= (Emacs 30 or later) + +GNU Emacs comes with =use-package.el= built-in since version 29. And +since version 30, it also comes with a built-in =:vc= keyword for the +~use-package~ macro that utilizes =package-vc.el= to install Emacs +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 - :straight (lean4-mode - :type git - :host github - :repo "leanprover/lean4-mode" - :files ("*.el" "data")) - ;; to defer loading the package until required - :commands (lean4-mode)) + :commands lean4-mode + :vc (:url "https://github.com/leanprover-community/lean4-mode.git" + :rev :newest)) #+end_src -If you are a doom-emacs user, adding the following to =packages.el= -should work: +*** Doom-Emacs + +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 @@ -47,42 +107,51 @@ should work: :files ("*.el" "data"))) #+end_src +*** Straight + +If you use the Straight package manager through Use-Package, then +place the following code in your Emacs initialization file: + +#+begin_src elisp +(use-package lean4-mode + :commands lean4-mode + :straight (lean4-mode :type git :host github + :repo "leanprover/lean4-mode" + :files ("*.el" "data"))) +#+end_src + * Trying It Out If things are working correctly, you should see the word "Lean 4" in -the Emacs mode line when you open a file with extension =.lean=. -Emacs will ask you to identify the "project" this file belongs to. If -you then type -#+begin_src lean -#check id -#+end_src -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. +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. To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This -will show the =*Lean Goals*= buffer (like the =Lean infoview= pane in -VSCode) in a separate window. +will display the =*Lean Goals*= buffer (like the =Lean infoview= pane +in VS-Code) in a separate window. * Settings Set these with e.g. =M-x customize-variable=. - - ~lsp-headerline-breadcrumb-enable~: Show a "breadcrumb bar" of - namespaces and sections surrounding the current location (default: - off) + namespaces and sections surrounding the current location. Defaults + to /off/. * Key Bindings and Commands | Key | Function | |---------------+---------------------------------------------------------------------------------| -| =C-c C-k= | show the keystroke needed to input the symbol under the cursor | -| =C-c C-d= | recompile & reload imports (~lean4-refresh-file-dependencies~) | -| =C-c C-x= | 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 showing goals and errors at point (~lean4-toggle-info-buffer~) | -| =C-c ! n= | flycheck: go to next error | -| =C-c ! p= | flycheck: go to previous error | +| =C-c C-k= | Show the keystroke needed to input the symbol under the cursor | +| =C-c C-d= | Recompile & reload imports (~lean4-refresh-file-dependencies~) | +| =C-c C-x= | 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 showing goals and errors at point (~lean4-toggle-info-buffer~) | +| =C-c ! n= | Flycheck: go to next error | +| =C-c ! p= | Flycheck: go to previous error | For ~lsp-mode~ bindings, see https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all From 429e7e5b3d00550f7d8de42e014bc37fa12c808f Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Mon, 18 Nov 2024 22:38:56 +0100 Subject: [PATCH 09/15] README: Keybindings: Separate "command" column; rewordings --- README.org | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/README.org b/README.org index f3b4cf1..363d8b1 100644 --- a/README.org +++ b/README.org @@ -143,20 +143,20 @@ Set these with e.g. =M-x customize-variable=. * Key Bindings and Commands -| Key | Function | -|---------------+---------------------------------------------------------------------------------| -| =C-c C-k= | Show the keystroke needed to input the symbol under the cursor | -| =C-c C-d= | Recompile & reload imports (~lean4-refresh-file-dependencies~) | -| =C-c C-x= | 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 showing goals and errors at point (~lean4-toggle-info-buffer~) | -| =C-c ! n= | Flycheck: go to next error | -| =C-c ! p= | Flycheck: go to previous error | - -For ~lsp-mode~ bindings, see -https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all -capabilities are supported currently). - -In the default configuration, the Flycheck annotation =FlyC:n/n= -indicates the number of errors / responses from Lean; clicking on -=FlyC= opens the Flycheck menu. +| Key | Description | Command | +|------------------------+--------------------------------------------------------+-----------------------------------| +| =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | +| =C-c C-d= | Recompile and reload imports | ~lean4-refresh-file-dependencies~ | +| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-std-exe~ | +| =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | +| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | +|------------------------+--------------------------------------------------------+-----------------------------------| +| =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 +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. From dba9dd1d180243cc65b7bd97f95a3c65996bbfd5 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Thu, 21 Nov 2024 22:21:35 +0100 Subject: [PATCH 10/15] README: Mention Zulip channel --- README.org | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.org b/README.org index 363d8b1..147375b 100644 --- a/README.org +++ b/README.org @@ -4,7 +4,12 @@ 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. -For version 3 of Lean, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (formerly known as /Lean-Mode/). +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]] (formerly +known as /Lean-Mode/). * Installation From a69330ff5e6fac1c0abf375e24b72a642ee1d31f Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Thu, 21 Nov 2024 22:22:12 +0100 Subject: [PATCH 11/15] README: Rename section "Trying it out" to "Usage"; other minor edits --- README.org | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/README.org b/README.org index 147375b..1a193a4 100644 --- a/README.org +++ b/README.org @@ -125,7 +125,7 @@ place the following code in your Emacs initialization file: :files ("*.el" "data"))) #+end_src -* Trying It Out +* Usage 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 @@ -136,15 +136,12 @@ show =FlyC:0/1=, indicating that there are no errors and one piece of information displayed. To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This -will display the =*Lean Goals*= buffer (like the =Lean infoview= pane +will display the =*Lean Goals*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. -* Settings - -Set these with e.g. =M-x customize-variable=. -- ~lsp-headerline-breadcrumb-enable~: Show a "breadcrumb bar" of - namespaces and sections surrounding the current location. Defaults - to /off/. +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 From 0a5fc604d80bbb5b184e1f2b5af6e479119c8fb6 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Thu, 21 Nov 2024 22:39:22 +0100 Subject: [PATCH 12/15] Makefile to translate README.org into .texi and .info manuals --- Makefile | 10 ++ README.org | 7 +- lean4-mode.info | 264 ++++++++++++++++++++++++++++++++++++++++++++++++ lean4-mode.texi | 260 +++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 540 insertions(+), 1 deletion(-) create mode 100644 Makefile create mode 100644 lean4-mode.info create mode 100644 lean4-mode.texi diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..89e8f6c --- /dev/null +++ b/Makefile @@ -0,0 +1,10 @@ +# GNU- and NonGNU-Elpa accept Org files as package documentation but +# Melpa does not. As long as Lean4-Mode is not distributed on GNU- or +# NonGNU-Elpa, it should ship with .texi and .info manuals. This +# depends on: GNU Emacs, Make and GNU Texinfo. + +lean4-mode.info lean4-mode.texi: README.org + emacs --batch \ + "--eval=(require 'ox-texinfo)" \ + '--eval=(find-file "$<")' \ + '--eval=(org-texinfo-export-to-info)' diff --git a/README.org b/README.org index 1a193a4..6ff7055 100644 --- a/README.org +++ b/README.org @@ -1,4 +1,9 @@ -#+title: ~lean4-mode~ - An Emacs major-mode for the 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 This package extends GNU Emacs by providing a major-mode for editing code written in version 4 of the programming language and theorem diff --git a/lean4-mode.info b/lean4-mode.info new file mode 100644 index 0000000..e2437e3 --- /dev/null +++ b/lean4-mode.info @@ -0,0 +1,264 @@ +This is lean4-mode.info, produced by makeinfo version 7.1 from +lean4-mode.texi. + +INFO-DIR-SECTION Emacs misc features +START-INFO-DIR-ENTRY +* 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 +*********************************************** + +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. + + 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) (formerly known as +_Lean-Mode_). + +* Menu: + +* Installation:: +* Usage:: +* Key Bindings and Commands:: + +-- The Detailed Node Listing -- + +Installation + +* Brief and Generic Instructions:: +* Detailed and Concrete Instructions:: +* Instructions for Source-Based Use-Package:: + +Instructions for Source-Based Use-Package + +* Native vc (Emacs 30 or later):: +* Doom-Emacs:: +* Straight:: + + + +File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top + +1 Installation +************** + +* Menu: + +* Brief and Generic Instructions:: +* Detailed and Concrete Instructions:: +* Instructions for Source-Based Use-Package:: + + +File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed and Concrete Instructions, Up: Installation + +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), Flycheck + (https://www.flycheck.org), 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 the Melpa package-archive) + + Install Lean4-Mode: + • 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)’. + + +File: lean4-mode.info, Node: Detailed and Concrete Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief and Generic Instructions, Up: Installation + +1.2 Detailed and Concrete Instructions +====================================== + +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 +(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)))) + + Clone the Git repository of 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") + (require 'lean4-mode) + + +File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed and Concrete Instructions, Up: Installation + +1.3 Instructions for Source-Based Use-Package +============================================= + +If you use a source-based package-manager (e.g. ‘package-vc.el’, +Straight or Elpaca), then make sure to list the ‘"data"’ directory in +your Lean4-Mode package recipe. + + If you use the ‘use-package’ macro and intent to defer loading of +packages in order to improve your Emacs startup time, then make sure to +specify ‘lean4-mode’ as a ‘:command’. + + Following subsections show concrete examples. + +* Menu: + +* Native vc (Emacs 30 or later):: +* Doom-Emacs:: +* Straight:: + + +File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom-Emacs, Up: Instructions for Source-Based Use-Package + +1.3.1 Native ‘:vc’ (Emacs 30 or later) +-------------------------------------- + +GNU Emacs comes with ‘use-package.el’ built-in since version 29. And +since version 30, it also comes with a built-in ‘:vc’ keyword for the +‘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)) + + +File: lean4-mode.info, Node: Doom-Emacs, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package + +1.3.2 Doom-Emacs +---------------- + +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"))) + + +File: lean4-mode.info, Node: Straight, Prev: Doom-Emacs, Up: Instructions for Source-Based Use-Package + +1.3.3 Straight +-------------- + +If you use the Straight package manager through Use-Package, then 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" + :files ("*.el" "data"))) + + +File: lean4-mode.info, Node: Usage, Next: Key Bindings and Commands, Prev: Installation, Up: Top + +2 Usage +******* + +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. + + 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’ +‘C-c C-d’ Recompile and reload imports ‘lean4-refresh-file-dependencies’ +‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-std-exe’ +‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ +‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’ +‘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 +(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. + + + +Tag Table: +Node: Top223 +Node: Installation1324 +Node: Brief and Generic Instructions1567 +Node: Detailed and Concrete Instructions2574 +Node: Instructions for Source-Based Use-Package4128 +Node: Native vc (Emacs 30 or later)4849 +Node: Doom-Emacs5702 +Node: Straight6102 +Node: Usage6592 +Node: Key Bindings and Commands7512 + +End Tag Table + + +Local Variables: +coding: utf-8 +End: diff --git a/lean4-mode.texi b/lean4-mode.texi new file mode 100644 index 0000000..6ecaa27 --- /dev/null +++ b/lean4-mode.texi @@ -0,0 +1,260 @@ +\input texinfo @c -*- texinfo -*- +@c %**start of header +@setfilename lean4-mode.info +@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. +@end direntry + +@finalout +@titlepage +@title Lean4-Mode - Emacs major-mode for Lean language +@end titlepage + +@contents + +@ifnottex +@node Top +@top 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. + +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} (formerly +known as @emph{Lean-Mode}). + +@end ifnottex + +@menu +* Installation:: +* Usage:: +* Key Bindings and Commands:: + +@detailmenu +--- The Detailed Node Listing --- + +Installation + +* Brief and Generic Instructions:: +* Detailed and Concrete Instructions:: +* Instructions for Source-Based Use-Package:: + +Instructions for Source-Based Use-Package + +* Native @samp{vc} (Emacs 30 or later):: +* Doom-Emacs:: +* Straight:: + +@end detailmenu +@end menu + +@node Installation +@chapter Installation + +@menu +* Brief and Generic Instructions:: +* Detailed and Concrete Instructions:: +* Instructions for Source-Based Use-Package:: +@end menu + +@node Brief and Generic Instructions +@section Brief and Generic Instructions + +Install dependencies: +@itemize +@item +@uref{https://lean-lang.org/lean4/doc/setup.html, Lean version 4} +@item +Emacs version 27 or later +@item +Emacs packages @uref{https://github.com/magnars/dash.el, Dash}, @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 the Melpa package-archive) +@end itemize + +Install Lean4-Mode: +@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)}. +@end itemize + +@node Detailed and Concrete Instructions +@section Detailed and Concrete Instructions + +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 +(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)))) +@end lisp + +Clone the Git repository of Lean4-Mode: + +@example +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: +@lisp +(add-to-list 'load-path "/path/to/lean4-mode") +(require 'lean4-mode) +@end lisp + +@node Instructions for Source-Based Use-Package +@section Instructions for Source-Based Use-Package + +If you use a source-based package-manager (e.g. @samp{package-vc.el}, +Straight or Elpaca), then make sure to list the @samp{"data"} directory in +your Lean4-Mode package recipe. + +If you use the @code{use-package} macro and intent to defer loading of +packages in order to improve your Emacs startup time, then make sure +to specify @code{lean4-mode} as a @samp{:command}. + +Following subsections show concrete examples. + +@menu +* Native @samp{vc} (Emacs 30 or later):: +* Doom-Emacs:: +* Straight:: +@end menu + +@node Native @samp{vc} (Emacs 30 or later) +@subsection Native @samp{:vc} (Emacs 30 or later) + +GNU Emacs comes with @samp{use-package.el} built-in since version 29. And +since version 30, it also comes with a built-in @samp{:vc} keyword for the +@code{use-package} macro that utilizes @samp{package-vc.el} to install Emacs +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)) +@end lisp + +@node Doom-Emacs +@subsection Doom-Emacs + +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"))) +@end lisp + +@node Straight +@subsection Straight + +If you use the Straight package manager through Use-Package, then +place the following code in your Emacs initialization file: + +@lisp +(use-package lean4-mode + :commands lean4-mode + :straight (lean4-mode :type git :host github + :repo "leanprover/lean4-mode" + :files ("*.el" "data"))) +@end lisp + +@node Usage +@chapter Usage + +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. + +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 +@tab Command +@item @samp{C-c C-k} +@tab Echo the keystroke needed to input the symbol at point +@tab @code{quail-show-key} +@item @samp{C-c C-d} +@tab Recompile and reload imports +@tab @code{lean4-refresh-file-dependencies} +@item @samp{C-c C-x} or @samp{C-c C-l} +@tab Execute Lean in stand-alone mode +@tab @code{lean4-std-exe} +@item @samp{C-c C-p C-l} +@tab Builds package with lake +@tab @code{lean4-lake-build} +@item @samp{C-c C-i} +@tab Toggle Info-View which shows goals and errors at point +@tab @code{lean4-toggle-info-buffer} +@item @samp{C-c ! n} +@tab Flycheck: Go to next error +@tab @code{flycheck-next-error} +@item @samp{C-c ! p} +@tab Flycheck: 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. + +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. + +@bye From 653aa65edd10231ab65ec130d6a4dff0bd8812fe Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Thu, 21 Nov 2024 23:23:53 +0100 Subject: [PATCH 13/15] README: Make clear that Dash is distributed on GNU-Elpa --- README.org | 5 +++-- lean4-mode.info | 19 ++++++++++--------- lean4-mode.texi | 5 +++-- 3 files changed, 16 insertions(+), 13 deletions(-) diff --git a/README.org b/README.org index 6ff7055..8a7acdd 100644 --- a/README.org +++ b/README.org @@ -23,8 +23,9 @@ known as /Lean-Mode/). 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]], [[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 the Melpa package-archive) +- 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) Install Lean4-Mode: - Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]]. diff --git a/lean4-mode.info b/lean4-mode.info index e2437e3..6966f13 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -69,11 +69,12 @@ File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed an 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), Flycheck + • 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 (https://github.com/magit/magit/blob/main/lisp/magit-section.el) - (which are available on the Melpa package-archive) + (which are available on Melpa package-archive) Install Lean4-Mode: • Clone the Git repository of Lean4-Mode @@ -248,13 +249,13 @@ Tag Table: Node: Top223 Node: Installation1324 Node: Brief and Generic Instructions1567 -Node: Detailed and Concrete Instructions2574 -Node: Instructions for Source-Based Use-Package4128 -Node: Native vc (Emacs 30 or later)4849 -Node: Doom-Emacs5702 -Node: Straight6102 -Node: Usage6592 -Node: Key Bindings and Commands7512 +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  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 6ecaa27..9b5cd44 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -77,8 +77,9 @@ Install dependencies: @item Emacs version 27 or later @item -Emacs packages @uref{https://github.com/magnars/dash.el, Dash}, @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 the Melpa package-archive) +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) @end itemize Install Lean4-Mode: From 294f74af4c6bdd95e93903a52db5e04bea293d97 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Thu, 21 Nov 2024 23:31:37 +0100 Subject: [PATCH 14/15] Release version 1.0.1 --- CHANGELOG.org | 6 ++++++ lean4-mode.el | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.org b/CHANGELOG.org index adec67c..60ec926 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -3,6 +3,12 @@ * Development +* 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-mode.el b/lean4-mode.el index 80b8066..fb52fa5 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -13,7 +13,7 @@ ;; 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 ;; SPDX-License-Identifier: Apache-2.0 -;; Version: 1.0.0 +;; Version: 1.0.1 ;;; License: From 4975c430d264b8b330987aa2b857616afa06f70a Mon Sep 17 00:00:00 2001 From: mekeor <60295641+mekeor@users.noreply.github.com> Date: Fri, 22 Nov 2024 20:48:46 +0100 Subject: [PATCH 15/15] README: Small English comma-grammar correction Co-authored-by: Yury G. Kudryashov --- README.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.org b/README.org index 8a7acdd..eff7672 100644 --- a/README.org +++ b/README.org @@ -24,7 +24,7 @@ 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 + 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) Install Lean4-Mode: