From 02f40c795296f55d9edf45a4c2752f44d9398c0b Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:35 +0200 Subject: [PATCH 01/50] [readme] Incorporate changelog --- CHANGELOG.org | 35 ------------- README.org | 41 ++++++++++++++++ lean4-mode.info | 128 ++++++++++++++++++++++++++++++++++++++++++------ lean4-mode.texi | 89 +++++++++++++++++++++++++++++++++ 4 files changed, 243 insertions(+), 50 deletions(-) delete mode 100644 CHANGELOG.org diff --git a/CHANGELOG.org b/CHANGELOG.org deleted file mode 100644 index 1ed62fe..0000000 --- a/CHANGELOG.org +++ /dev/null @@ -1,35 +0,0 @@ -#+title: Lean4-Mode - Changelog -#+language: en - -* Version 1.1.2 - -- Fix occasional errors like "The connected server(s) does not support - method =$/lean/plainGoal=" by not wrapping invocations of - ~lsp-protocol~ macro into ~eval-when-compile~ but rather into - ~eval-and-compile~. Thus, the methods should now work, no matter - whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by - loading compiled =.elc= or =.eln= files. ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]]) - -* Version 1.1.1 - -- Assign all customizable user-options to the Lean4-Mode specific - =lean4= group. To customize Lean4-Mode, you now need to type =M-x - customize-group RET lean4 RET=. - -* Version 1.1.0 - -- To =lean4= customization group, add link to local info manual and - use Lean4-Mode Github URL as website. -- Introduce new dependency on Elpa package =compat=. -- Remove dependency on Elpa package Flycheck. It is still supported - but not required. - -* Version 1.0.1 - -- Specify Yury G. Kudryashov as maintainer. -- Rework README. (Now in Org format). -- Provide README as Texi and Info manual too. - -* Version 1.0 - -- Specify "Version" in Emacs-Lisp library header. diff --git a/README.org b/README.org index ac66c63..dc95591 100644 --- a/README.org +++ b/README.org @@ -200,3 +200,44 @@ reasons. In principle, it is fine to have both Lean3-Mode and Lean4-Mode installed at the same time. But note that Lean3-Mode uses the prefix =lean-= for its symbols. E.g. you should not use =lean-=-prefixed commands in a buffer with Lean4-Mode as major mode. + +* Changelog + +** Upcoming Version + +Documentation: +- The changelog is now part of the readme (and thus of the Info + manual). + +** Version 1.1.2 from 2024-12-10 + +- Fix occasional errors like "The connected server(s) does not support + method =$/lean/plainGoal=" by not wrapping invocations of + ~lsp-protocol~ macro into ~eval-when-compile~ but rather into + ~eval-and-compile~. Thus, the methods should now work, no matter + whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by + loading compiled =.elc= or =.eln= files. ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]]) + +** Version 1.1.1 from 2024-12-02 + +- Assign all customizable user-options to the Lean4-Mode specific + =lean4= group. To customize Lean4-Mode, you now need to type =M-x + customize-group RET lean4 RET=. + +** Version 1.1.0 from 2024-12-01 + +- To =lean4= customization group, add link to local info manual and + use Lean4-Mode Github URL as website. +- Introduce new dependency on Elpa package =compat=. +- Remove dependency on Elpa package Flycheck. It is still supported + but not required. + +** Version 1.0.1 from 2024-11-21 + +- Specify Yury G. Kudryashov as maintainer. +- Rework README. (Now in Org format). +- Provide README as Texi and Info manual too. + +** Version 1.0 from 2024-11-16 + +- Specify "Version" in Emacs-Lisp library header. diff --git a/lean4-mode.info b/lean4-mode.info index 41a8f4c..d7a3ea7 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -32,6 +32,7 @@ Lean's Zulip chat. * Usage:: * Configuration:: * Common Pitfalls:: +* Changelog:: -- The Detailed Node Listing -- @@ -57,6 +58,15 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Changelog + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. +  File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top @@ -300,7 +310,7 @@ installed, then customize the ‘lsp-diagnostics-provider’ user option accordingly.  -File: lean4-mode.info, Node: Common Pitfalls, Prev: Configuration, Up: Top +File: lean4-mode.info, Node: Common Pitfalls, Next: Changelog, Prev: Configuration, Up: Top 4 Common Pitfalls ***************** @@ -313,24 +323,112 @@ note that Lean3-Mode uses the prefix ‘lean-’ for its symbols. E.g. you should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as major mode. + +File: lean4-mode.info, Node: Changelog, Prev: Common Pitfalls, Up: Top + +5 Changelog +*********** + +* Menu: + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. + + +File: lean4-mode.info, Node: Upcoming Version, Next: Version 112 from 2024-12-10, Up: Changelog + +5.1 Upcoming Version +==================== + +Documentation: + • The changelog is now part of the readme (and thus of the Info + manual). + + +File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog + +5.2 Version 1.1.2 from 2024-12-10 +================================= + + • Fix occasional errors like "The connected server(s) does not + support method ‘$/lean/plainGoal’" by not wrapping invocations of + ‘lsp-protocol’ macro into ‘eval-when-compile’ but rather into + ‘eval-and-compile’. Thus, the methods should now work, no matter + whether Lean4-Mode was loaded by interpreting ‘.el’ Elisp code or + by loading compiled ‘.elc’ or ‘.eln’ files. (Bug#54 + (https://github.com/leanprover-community/lean4-mode/issues/54), + Zulip discussion + (https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table)) + + +File: lean4-mode.info, Node: Version 111 from 2024-12-02, Next: Version 110 from 2024-12-01, Prev: Version 112 from 2024-12-10, Up: Changelog + +5.3 Version 1.1.1 from 2024-12-02 +================================= + + • Assign all customizable user-options to the Lean4-Mode specific + ‘lean4’ group. To customize Lean4-Mode, you now need to type ‘M-x + customize-group RET lean4 RET’. + + +File: lean4-mode.info, Node: Version 110 from 2024-12-01, Next: Version 101 from 2024-11-21, Prev: Version 111 from 2024-12-02, Up: Changelog + +5.4 Version 1.1.0 from 2024-12-01 +================================= + + • To ‘lean4’ customization group, add link to local info manual and + use Lean4-Mode Github URL as website. + • Introduce new dependency on Elpa package ‘compat’. + • Remove dependency on Elpa package Flycheck. It is still supported + but not required. + + +File: lean4-mode.info, Node: Version 101 from 2024-11-21, Next: Version 10 from 2024-11-16, Prev: Version 110 from 2024-12-01, Up: Changelog + +5.5 Version 1.0.1 from 2024-11-21 +================================= + + • Specify Yury G. Kudryashov as maintainer. + • Rework README. (Now in Org format). + • Provide README as Texi and Info manual too. + + +File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 from 2024-11-21, Up: Changelog + +5.6 Version 1.0 from 2024-11-16 +=============================== + + • Specify "Version" in Emacs-Lisp library header. +  Tag Table: Node: Top223 -Node: Installation1492 -Node: Brief and Generic Instructions1735 -Node: Detailed and Concrete Instructions2684 -Node: Instructions for Source-Based Use-Package4341 -Node: Native vc (Emacs 30 or later)5062 -Node: Doom-Emacs5970 -Node: Straight6396 -Node: Usage6896 -Node: lsp-mode8342 -Node: Flycheck8627 -Node: Configuration9237 -Node: lsp-mode (1)9427 -Node: Flycheck (1)9696 -Node: Common Pitfalls10181 +Node: Installation1846 +Node: Brief and Generic Instructions2089 +Node: Detailed and Concrete Instructions3038 +Node: Instructions for Source-Based Use-Package4695 +Node: Native vc (Emacs 30 or later)5416 +Node: Doom-Emacs6324 +Node: Straight6750 +Node: Usage7250 +Node: lsp-mode8696 +Node: Flycheck8981 +Node: Configuration9591 +Node: lsp-mode (1)9781 +Node: Flycheck (1)10050 +Node: Common Pitfalls10535 +Node: Changelog11127 +Node: Upcoming Version11567 +Node: Version 112 from 2024-12-1011811 +Node: Version 111 from 2024-12-0212676 +Node: Version 110 from 2024-12-0113083 +Node: Version 101 from 2024-11-2113581 +Node: Version 10 from 2024-11-1613944  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index fd205bf..909ff60 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -40,6 +40,7 @@ as @emph{Lean-Mode}). * Usage:: * Configuration:: * Common Pitfalls:: +* Changelog:: @detailmenu --- The Detailed Node Listing --- @@ -66,6 +67,15 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Changelog + +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. + @end detailmenu @end menu @@ -317,4 +327,83 @@ Lean4-Mode installed at the same time. But note that Lean3-Mode uses the prefix @samp{lean-} for its symbols. E.g. you should not use @samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode. +@node Changelog +@chapter Changelog + +@menu +* Upcoming Version:: +* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. +* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. +* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. +* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. +* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. +@end menu + +@node Upcoming Version +@section Upcoming Version + +Documentation: +@itemize +@item +The changelog is now part of the readme (and thus of the Info +manual). +@end itemize + +@node Version 112 from 2024-12-10 +@section Version 1.1.2 from 2024-12-10 + +@itemize +@item +Fix occasional errors like "The connected server(s) does not support +method @samp{$/lean/plainGoal}" by not wrapping invocations of +@code{lsp-protocol} macro into @code{eval-when-compile} but rather into +@code{eval-and-compile}. Thus, the methods should now work, no matter +whether Lean4-Mode was loaded by interpreting @samp{.el} Elisp code or by +loading compiled @samp{.elc} or @samp{.eln} files. (@uref{https://github.com/leanprover-community/lean4-mode/issues/54, Bug#54}, @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table, Zulip discussion}) +@end itemize + +@node Version 111 from 2024-12-02 +@section Version 1.1.1 from 2024-12-02 + +@itemize +@item +Assign all customizable user-options to the Lean4-Mode specific +@samp{lean4} group. To customize Lean4-Mode, you now need to type @samp{M-x + customize-group RET lean4 RET}. +@end itemize + +@node Version 110 from 2024-12-01 +@section Version 1.1.0 from 2024-12-01 + +@itemize +@item +To @samp{lean4} customization group, add link to local info manual and +use Lean4-Mode Github URL as website. +@item +Introduce new dependency on Elpa package @samp{compat}. +@item +Remove dependency on Elpa package Flycheck. It is still supported +but not required. +@end itemize + +@node Version 101 from 2024-11-21 +@section Version 1.0.1 from 2024-11-21 + +@itemize +@item +Specify Yury G@. Kudryashov as maintainer. +@item +Rework README@. (Now in Org format). +@item +Provide README as Texi and Info manual too. +@end itemize + +@node Version 10 from 2024-11-16 +@section Version 1.0 from 2024-11-16 + +@itemize +@item +Specify "Version" in Emacs-Lisp library header. +@end itemize + @bye From 4429417a5520bc7334fffabd4df8c87125da3362 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:38 +0200 Subject: [PATCH 02/50] [makefile] Add goal "clean" --- Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Makefile b/Makefile index 89e8f6c..a848d37 100644 --- a/Makefile +++ b/Makefile @@ -8,3 +8,6 @@ lean4-mode.info lean4-mode.texi: README.org "--eval=(require 'ox-texinfo)" \ '--eval=(find-file "$<")' \ '--eval=(org-texinfo-export-to-info)' + +clean: + rm lean4-mode.info lean4-mode.texi From d88e86ad7fcd3703defc5065677e24aefc69d9d7 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:41 +0200 Subject: [PATCH 03/50] [mode] Delete empty abbrev-table --- lean4-mode.el | 5 ----- 1 file changed, 5 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index 3994c99..596cb32 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -147,9 +147,6 @@ file, recompiling, and reloading all imports." ;; (local-set-key (kbd "") #'lean4-right-click-show-menu) ) -(define-abbrev-table 'lean4-abbrev-table - '()) - (defvar lean4-mode-map (make-sparse-keymap) "Keymap used in Lean mode.") @@ -216,7 +213,6 @@ of the parent project." \\{lean4-mode-map}" :syntax-table lean4-syntax-table - :abbrev-table lean4-abbrev-table :group 'lean4 (set (make-local-variable 'comment-start) "--") (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*") @@ -234,7 +230,6 @@ of the parent project." (lean4-set-keys) (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1)) - ;; (abbrev-mode 1) (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist) (add-hook hook fn nil 'local)) (lean4-mode-setup)) From aea6d96c0bd1f2c8435204d1b17e3f71f1b9887e Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:45 +0200 Subject: [PATCH 04/50] [mode] Delete Flycheck entry in tool-bar menu --- README.org | 5 +++++ lean4-mode.el | 5 ----- lean4-mode.info | 16 +++++++++++----- lean4-mode.texi | 8 ++++++++ 4 files changed, 24 insertions(+), 10 deletions(-) diff --git a/README.org b/README.org index dc95591..f8807c0 100644 --- a/README.org +++ b/README.org @@ -209,6 +209,11 @@ Documentation: - The changelog is now part of the readme (and thus of the Info manual). +User interface: +- The tool-bar menu of Lean4-Mode does not list the + ~flycheck-list-errors~ anymore. Please use the “Show all errors” + entry in Flycheck's menu instead. (Fixes [[https://github.com/leanprover-community/lean4-mode/issues/91][#91]].) + ** Version 1.1.2 from 2024-12-10 - Fix occasional errors like "The connected server(s) does not support diff --git a/lean4-mode.el b/lean4-mode.el index 596cb32..d312154 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -155,11 +155,6 @@ file, recompiling, and reloading all imports." `("Lean 4" ["Execute lean" lean4-execute t] ["Toggle info display" lean4-toggle-info t] - ;; TODO: Bug#91: We offers a Flycheck-based menu-item when - ;; Flycheck is in use. Users who use built-in Flymake should also - ;; be offered a working menu-item. Alternatively, the menu-item - ;; could also be dropped for both cases. - ["List of errors" flycheck-list-errors flycheck-mode] ["Restart lean process" lsp-workspace-restart t] ["Customize lean4-mode" (customize-group 'lean) t])) diff --git a/lean4-mode.info b/lean4-mode.info index d7a3ea7..da365ed 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -348,6 +348,12 @@ Documentation: • The changelog is now part of the readme (and thus of the Info manual). + User interface: + • The tool-bar menu of Lean4-Mode does not list the + ‘flycheck-list-errors’ anymore. Please use the “Show all errors” + entry in Flycheck's menu instead. (Fixes #91 + (https://github.com/leanprover-community/lean4-mode/issues/91).) +  File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog @@ -424,11 +430,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1011811 -Node: Version 111 from 2024-12-0212676 -Node: Version 110 from 2024-12-0113083 -Node: Version 101 from 2024-11-2113581 -Node: Version 10 from 2024-11-1613944 +Node: Version 112 from 2024-12-1012088 +Node: Version 111 from 2024-12-0212953 +Node: Version 110 from 2024-12-0113360 +Node: Version 101 from 2024-11-2113858 +Node: Version 10 from 2024-11-1614221  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 909ff60..b33a788 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -349,6 +349,14 @@ The changelog is now part of the readme (and thus of the Info manual). @end itemize +User interface: +@itemize +@item +The tool-bar menu of Lean4-Mode does not list the +@code{flycheck-list-errors} anymore. Please use the “Show all errors” +entry in Flycheck's menu instead. (Fixes @uref{https://github.com/leanprover-community/lean4-mode/issues/91, #91}.) +@end itemize + @node Version 112 from 2024-12-10 @section Version 1.1.2 from 2024-12-10 From a6a1009ca416fe5ff43bd40db6bd636d318aa563 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:48 +0200 Subject: [PATCH 05/50] [mode][settings][util] Delete feature of whitespace cleanup - Delete variable lean4-delete-trailing-whitespace. - Delete function lean4-whitespace-cleanup. The objective is to reduce the feature set of Lean4-Mode for sake of maintainability. This feature in particular is already provided in Emacs core and thus a redundant burden. --- README.org | 9 +++++++++ lean4-mode.el | 5 +---- lean4-mode.info | 19 ++++++++++++++----- lean4-mode.texi | 12 ++++++++++++ lean4-settings.el | 8 -------- lean4-util.el | 5 ----- 6 files changed, 36 insertions(+), 22 deletions(-) diff --git a/README.org b/README.org index f8807c0..6361e05 100644 --- a/README.org +++ b/README.org @@ -214,6 +214,15 @@ User interface: ~flycheck-list-errors~ anymore. Please use the “Show all errors” entry in Flycheck's menu instead. (Fixes [[https://github.com/leanprover-community/lean4-mode/issues/91][#91]].) +Features: +- The variable ~lean4-delete-trailing-whitespace~ has been removed + together with related code. Instead of reinventing the wheel, + Lean4-Mode demands users to use Emacs' built-in facilities for this + kind of use case. For example, you might want to define a function + that buffer-locally adds ~delete-trailing-whitespace~ to + ~before-save-hook~, and add that hereby defined function to + ~lean4-mode-hook~. + ** Version 1.1.2 from 2024-12-10 - Fix occasional errors like "The connected server(s) does not support diff --git a/lean4-mode.el b/lean4-mode.el index d312154..6ac71d6 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -159,10 +159,7 @@ file, recompiling, and reloading all imports." ["Customize lean4-mode" (customize-group 'lean) t])) (defconst lean4-hooks-alist - '( - ;; Handle events that may start automatic syntax checks - (before-save-hook . lean4-whitespace-cleanup) - ;; info view + '(;; info view ;; update errors immediately, but delay querying goal (flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay-debounced) (post-command-hook . lean4-info-buffer-redisplay-debounced) diff --git a/lean4-mode.info b/lean4-mode.info index da365ed..7283fe8 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -354,6 +354,15 @@ Documentation: entry in Flycheck's menu instead. (Fixes #91 (https://github.com/leanprover-community/lean4-mode/issues/91).) + Features: + • The variable ‘lean4-delete-trailing-whitespace’ has been removed + together with related code. Instead of reinventing the wheel, + Lean4-Mode demands users to use Emacs' built-in facilities for this + kind of use case. For example, you might want to define a function + that buffer-locally adds ‘delete-trailing-whitespace’ to + ‘before-save-hook’, and add that hereby defined function to + ‘lean4-mode-hook’. +  File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog @@ -430,11 +439,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1012088 -Node: Version 111 from 2024-12-0212953 -Node: Version 110 from 2024-12-0113360 -Node: Version 101 from 2024-11-2113858 -Node: Version 10 from 2024-11-1614221 +Node: Version 112 from 2024-12-1012555 +Node: Version 111 from 2024-12-0213420 +Node: Version 110 from 2024-12-0113827 +Node: Version 101 from 2024-11-2114325 +Node: Version 10 from 2024-11-1614688  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index b33a788..edec860 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -357,6 +357,18 @@ The tool-bar menu of Lean4-Mode does not list the entry in Flycheck's menu instead. (Fixes @uref{https://github.com/leanprover-community/lean4-mode/issues/91, #91}.) @end itemize +Features: +@itemize +@item +The variable @code{lean4-delete-trailing-whitespace} has been removed +together with related code. Instead of reinventing the wheel, +Lean4-Mode demands users to use Emacs' built-in facilities for this +kind of use case. For example, you might want to define a function +that buffer-locally adds @code{delete-trailing-whitespace} to +@code{before-save-hook}, and add that hereby defined function to +@code{lean4-mode-hook}. +@end itemize + @node Version 112 from 2024-12-10 @section Version 1.1.2 from 2024-12-10 diff --git a/lean4-settings.el b/lean4-settings.el index 910e533..df1a712 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -90,14 +90,6 @@ It is approximately the maximum number of memory allocations in thousands." :group 'lean4 :type '(list string)) -(defcustom lean4-delete-trailing-whitespace nil - "Automatically delete trailing shitespace. -Set this variable to true to automatically delete trailing -whitespace when a buffer is loaded from a file or when it is -written." - :group 'lean4 - :type 'boolean) - (defcustom lean4-highlight-inaccessible-names t "Use font to highlight inaccessible names. Set this variable to t to highlight inaccessible names in the info display diff --git a/lean4-util.el b/lean4-util.el index 273a530..2b8cdab 100644 --- a/lean4-util.el +++ b/lean4-util.el @@ -55,10 +55,5 @@ First try to find an executable named `lean4-executable-name' in "Return fullpath of lean executable EXE-NAME." (file-name-concat (lean4-get-rootdir) "bin" exe-name)) -(defun lean4-whitespace-cleanup () - "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t." - (when lean4-delete-trailing-whitespace - (delete-trailing-whitespace))) - (provide 'lean4-util) ;;; lean4-util.el ends here From 31ddb48cdac941877391fc4dc664f125c29bb2fc Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:51 +0200 Subject: [PATCH 06/50] [mode] Delete feature of automatic Lean version detection - Delete variable lean4-autodetect-lean3. - Delete command lean4-select-mode. This feature was removed in order to reduce the complexity of Lean4-Mode and improve maintainability. In particular, the removal of this feature was justified by Lean version 3 and Lean3-Mode both being officially legacy / obsolete. --- README.org | 5 +++++ lean4-mode.el | 13 ++----------- lean4-mode.info | 15 ++++++++++----- lean4-mode.texi | 6 ++++++ lean4-settings.el | 9 --------- 5 files changed, 23 insertions(+), 25 deletions(-) diff --git a/README.org b/README.org index 6361e05..5dd1879 100644 --- a/README.org +++ b/README.org @@ -222,6 +222,11 @@ Features: that buffer-locally adds ~delete-trailing-whitespace~ to ~before-save-hook~, and add that hereby defined function to ~lean4-mode-hook~. +- The variable ~lean4-autodetect-lean3~ has been removed along with + the command ~lean4-select-mode~ and related code. If you still use + legacy version 3 of Lean for some files or projects, you could + directory- or file-locally associate the =.lean= file extension with + Lean3-Mode in ~auto-mode-alist~. ** Version 1.1.2 from 2024-12-10 diff --git a/lean4-mode.el b/lean4-mode.el index 6ac71d6..eb7aafc 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -63,7 +63,6 @@ (defvar markdown-code-lang-modes) (declare-function flycheck-list-errors "ext:flycheck") (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") -(declare-function lean-mode "ext:lean-mode") (declare-function quail-show-key "quail") (defun lean4-compile-string (lake-name exe-name args file-name) @@ -239,23 +238,15 @@ of the parent project." (interactive) (message "Lean %s" (mapconcat #'number-to-string (lean4--version) "."))) -;;;###autoload -(defun lean4-select-mode () - "Automatically select mode (Lean 3 vs Lean 4)." - (if (and lean4-autodetect-lean3 - (eq 3 (car (lean4--version)))) - (lean-mode) - (lean4-mode))) - ;; Automatically use lean4-mode for .lean files. ;;;###autoload (add-to-list 'auto-mode-alist - '("\\.lean\\'" . lean4-select-mode)) + '("\\.lean\\'" . lean4-mode)) ;;;###autoload (with-eval-after-load 'markdown-mode (add-to-list 'markdown-code-lang-modes - '("lean" . lean4-select-mode))) + '("lean" . lean4-mode))) ;; Use utf-8 encoding ;;;### autoload diff --git a/lean4-mode.info b/lean4-mode.info index 7283fe8..219ac85 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -362,6 +362,11 @@ Documentation: that buffer-locally adds ‘delete-trailing-whitespace’ to ‘before-save-hook’, and add that hereby defined function to ‘lean4-mode-hook’. + • The variable ‘lean4-autodetect-lean3’ has been removed along with + the command ‘lean4-select-mode’ and related code. If you still use + legacy version 3 of Lean for some files or projects, you could + directory- or file-locally associate the ‘.lean’ file extension + with Lean3-Mode in ‘auto-mode-alist’.  File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog @@ -439,11 +444,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1012555 -Node: Version 111 from 2024-12-0213420 -Node: Version 110 from 2024-12-0113827 -Node: Version 101 from 2024-11-2114325 -Node: Version 10 from 2024-11-1614688 +Node: Version 112 from 2024-12-1012897 +Node: Version 111 from 2024-12-0213762 +Node: Version 110 from 2024-12-0114169 +Node: Version 101 from 2024-11-2114667 +Node: Version 10 from 2024-11-1615030  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index edec860..ca5a9f8 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -367,6 +367,12 @@ kind of use case. For example, you might want to define a function that buffer-locally adds @code{delete-trailing-whitespace} to @code{before-save-hook}, and add that hereby defined function to @code{lean4-mode-hook}. +@item +The variable @code{lean4-autodetect-lean3} has been removed along with +the command @code{lean4-select-mode} and related code. If you still use +legacy version 3 of Lean for some files or projects, you could +directory- or file-locally associate the @samp{.lean} file extension with +Lean3-Mode in @code{auto-mode-alist}. @end itemize @node Version 112 from 2024-12-10 diff --git a/lean4-settings.el b/lean4-settings.el index df1a712..0285d51 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -102,15 +102,6 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." :group 'lean4 :type 'boolean) - -(defcustom lean4-autodetect-lean3 nil - "Autodetect Lean version. -Use elan to check if current project uses Lean 3 or Lean 4 and initialize the -right mode when visiting a file. If elan has a default Lean version, Lean files -outside a project will default to that mode." - :group 'lean4 - :type 'boolean) - (defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x") "Main Keybinding for `lean4-std-exe'." :group 'lean4-keybinding :type 'key-sequence) From dfecaba4ff8405aa5a85893c0bc9b7e1f322e2fa Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:55 +0200 Subject: [PATCH 07/50] [input] Delete feature of Javascript format export - Delete function lean4-input-export-translations. - Delete function lean4-input-export-translations-to-stdout. --- README.org | 6 ++++++ lean4-input.el | 31 ------------------------------- lean4-mode.info | 16 +++++++++++----- lean4-mode.texi | 7 +++++++ 4 files changed, 24 insertions(+), 36 deletions(-) diff --git a/README.org b/README.org index 5dd1879..88a3bd1 100644 --- a/README.org +++ b/README.org @@ -227,6 +227,12 @@ Features: legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the =.lean= file extension with Lean3-Mode in ~auto-mode-alist~. +- The functions ~lean4-input-export-translations~ and + ~lean4-input-export-translations-to-stdout~ have been removed. We + expect that noone has been using it. If you do use it, let us know, + so we can reconsider our decision in case of a substantial amount of + users. Otherwise, please just define these functions in your Emacs + initialization file yourself. ** Version 1.1.2 from 2024-12-10 diff --git a/lean4-input.el b/lean4-input.el index fce884f..0051b4e 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -307,37 +307,6 @@ Suitable for use in the :set field of `defcustom'." (cl-eval-when (load eval) (lean4-input-setup)) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Export Translations - -(defun lean4-input-export-translations () - "Export the current translations in a javascript format. -Print (input, output) pairs in Javascript format to the buffer -*lean4-translations*. The output can be copy-pasted to -leanprover.github.io/tutorial/js/input-method.js" - (interactive) - (with-current-buffer - (get-buffer-create "*lean4-translations*") - (let ((exclude-list '("\\newline"))) - (insert "var corrections = {") - (--each - (--filter (not (member (car it) exclude-list)) - (lean4-input-get-translations "Lean")) - (let* ((input (substring (car it) 1)) - (outputs (cdr it))) - (insert (format "%s:\"" (prin1-to-string input))) - (cond ((vectorp outputs) - (insert (elt outputs 0))) - (t (insert-char outputs))) - (insert (format "\",\n")))) - (insert "};")))) - -(defun lean4-input-export-translations-to-stdout () - "Print current translations to stdout." - (lean4-input-export-translations) - (with-current-buffer "*lean4-translations*" - (princ (buffer-string)))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Administrative details diff --git a/lean4-mode.info b/lean4-mode.info index 219ac85..77e36b0 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -367,6 +367,12 @@ Documentation: legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the ‘.lean’ file extension with Lean3-Mode in ‘auto-mode-alist’. + • The functions ‘lean4-input-export-translations’ and + ‘lean4-input-export-translations-to-stdout’ have been removed. We + expect that noone has been using it. If you do use it, let us + know, so we can reconsider our decision in case of a substantial + amount of users. Otherwise, please just define these functions in + your Emacs initialization file yourself.  File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog @@ -444,11 +450,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1012897 -Node: Version 111 from 2024-12-0213762 -Node: Version 110 from 2024-12-0114169 -Node: Version 101 from 2024-11-2114667 -Node: Version 10 from 2024-11-1615030 +Node: Version 112 from 2024-12-1013292 +Node: Version 111 from 2024-12-0214157 +Node: Version 110 from 2024-12-0114564 +Node: Version 101 from 2024-11-2115062 +Node: Version 10 from 2024-11-1615425  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index ca5a9f8..3aecbee 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -373,6 +373,13 @@ the command @code{lean4-select-mode} and related code. If you still use legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the @samp{.lean} file extension with Lean3-Mode in @code{auto-mode-alist}. +@item +The functions @code{lean4-input-export-translations} and +@code{lean4-input-export-translations-to-stdout} have been removed. We +expect that noone has been using it. If you do use it, let us know, +so we can reconsider our decision in case of a substantial amount of +users. Otherwise, please just define these functions in your Emacs +initialization file yourself. @end itemize @node Version 112 from 2024-12-10 From 662af87d95ed2b6d139c63f5b37d96c97e354cca Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:58 +0200 Subject: [PATCH 08/50] [mode] Delete lean4-show-version command --- README.org | 3 +++ lean4-mode.el | 13 ------------- lean4-mode.info | 13 ++++++++----- lean4-mode.texi | 4 ++++ 4 files changed, 15 insertions(+), 18 deletions(-) diff --git a/README.org b/README.org index 88a3bd1..2230a0c 100644 --- a/README.org +++ b/README.org @@ -227,6 +227,9 @@ Features: legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the =.lean= file extension with Lean3-Mode in ~auto-mode-alist~. +- The command ~lean4-show-version~ has been removed. Lean4-Mode now + assumes Lean version 4. In order to determine the minor version, you + may type =M-! lean --version RET= or similar. - The functions ~lean4-input-export-translations~ and ~lean4-input-export-translations-to-stdout~ have been removed. We expect that noone has been using it. If you do use it, let us know, diff --git a/lean4-mode.el b/lean4-mode.el index eb7aafc..0cb864c 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -225,19 +225,6 @@ of the parent project." (add-hook hook fn nil 'local)) (lean4-mode-setup)) -(defun lean4--version () - "Return Lean version as a list `(MAJOR MINOR PATCH)'." - (with-temp-buffer - (call-process (lean4-get-executable "lean") nil (list t nil) nil "-v") - (goto-char (point-min)) - (re-search-forward (rx bol "Lean (version " (group (+ digit) (+ "." (+ digit))))) - (version-to-list (match-string 1)))) - -(defun lean4-show-version () - "Print Lean 4 version." - (interactive) - (message "Lean %s" (mapconcat #'number-to-string (lean4--version) "."))) - ;; Automatically use lean4-mode for .lean files. ;;;###autoload (add-to-list 'auto-mode-alist diff --git a/lean4-mode.info b/lean4-mode.info index 77e36b0..46400e7 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -367,6 +367,9 @@ Documentation: legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the ‘.lean’ file extension with Lean3-Mode in ‘auto-mode-alist’. + • The command ‘lean4-show-version’ has been removed. Lean4-Mode now + assumes Lean version 4. In order to determine the minor version, + you may type ‘M-! lean --version RET’ or similar. • The functions ‘lean4-input-export-translations’ and ‘lean4-input-export-translations-to-stdout’ have been removed. We expect that noone has been using it. If you do use it, let us @@ -450,11 +453,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1013292 -Node: Version 111 from 2024-12-0214157 -Node: Version 110 from 2024-12-0114564 -Node: Version 101 from 2024-11-2115062 -Node: Version 10 from 2024-11-1615425 +Node: Version 112 from 2024-12-1013500 +Node: Version 111 from 2024-12-0214365 +Node: Version 110 from 2024-12-0114772 +Node: Version 101 from 2024-11-2115270 +Node: Version 10 from 2024-11-1615633  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 3aecbee..51040b7 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -374,6 +374,10 @@ legacy version 3 of Lean for some files or projects, you could directory- or file-locally associate the @samp{.lean} file extension with Lean3-Mode in @code{auto-mode-alist}. @item +The command @code{lean4-show-version} has been removed. Lean4-Mode now +assumes Lean version 4. In order to determine the minor version, you +may type @samp{M-! lean --version RET} or similar. +@item The functions @code{lean4-input-export-translations} and @code{lean4-input-export-translations-to-stdout} have been removed. We expect that noone has been using it. If you do use it, let us know, From bb83235dea8194e7ac6bc6391a93ccd5c4977034 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:01 +0200 Subject: [PATCH 09/50] [mode] Delete lean4-std-exe in favor of equal lean4-execute --- README.org | 4 +++- lean4-mode.el | 11 +++-------- lean4-mode.info | 14 ++++++++------ lean4-mode.texi | 5 ++++- lean4-settings.el | 4 ++-- 5 files changed, 20 insertions(+), 18 deletions(-) diff --git a/README.org b/README.org index 2230a0c..580d652 100644 --- a/README.org +++ b/README.org @@ -154,7 +154,7 @@ in VS-Code) in a separate window. |------------------------+--------------------------------------------------------+-----------------------------------| | =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-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-execute~ | | =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | | =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | @@ -236,6 +236,8 @@ Features: so we can reconsider our decision in case of a substantial amount of users. Otherwise, please just define these functions in your Emacs initialization file yourself. +- The command ~lean4-std-exe~ has been removed. It was just the same + as ~lean4-execute~ which continues to exist. ** Version 1.1.2 from 2024-12-10 diff --git a/lean4-mode.el b/lean4-mode.el index 0cb864c..6992002 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -101,11 +101,6 @@ FILE-NAME." (setq compile-command cc) (setq default-directory dd))) -(defun lean4-std-exe () - "Execute Lean in the current buffer." - (interactive) - (lean4-execute)) - (defun lean4-refresh-file-dependencies () "Refresh the file dependencies. @@ -131,9 +126,9 @@ file, recompiling, and reloading all imports." (t (indent-for-tab-command)))) (defun lean4-set-keys () - "Setup Lean 4 keybindings." - (local-set-key lean4-keybinding-std-exe1 #'lean4-std-exe) - (local-set-key lean4-keybinding-std-exe2 #'lean4-std-exe) + "Setup Lean4 keybindings." + (local-set-key lean4-keybinding-std-exe1 #'lean4-execute) + (local-set-key lean4-keybinding-std-exe2 #'lean4-execute) (local-set-key lean4-keybinding-show-key #'quail-show-key) (local-set-key lean4-keybinding-tab-indent #'lean4-tab-indent) ;; (local-set-key lean4-keybinding-hole #'lean4-hole) diff --git a/lean4-mode.info b/lean4-mode.info index 46400e7..6c1cf8a 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -240,7 +240,7 @@ Key Description ---------------------------------------------------------------------------------------------------------------------- ‘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-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ ‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’ @@ -376,6 +376,8 @@ Documentation: know, so we can reconsider our decision in case of a substantial amount of users. Otherwise, please just define these functions in your Emacs initialization file yourself. + • The command ‘lean4-std-exe’ has been removed. It was just the same + as ‘lean4-execute’ which continues to exist.  File: lean4-mode.info, Node: Version 112 from 2024-12-10, Next: Version 111 from 2024-12-02, Prev: Upcoming Version, Up: Changelog @@ -453,11 +455,11 @@ Node: Flycheck (1)10050 Node: Common Pitfalls10535 Node: Changelog11127 Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1013500 -Node: Version 111 from 2024-12-0214365 -Node: Version 110 from 2024-12-0114772 -Node: Version 101 from 2024-11-2115270 -Node: Version 10 from 2024-11-1615633 +Node: Version 112 from 2024-12-1013633 +Node: Version 111 from 2024-12-0214498 +Node: Version 110 from 2024-12-0114905 +Node: Version 101 from 2024-11-2115403 +Node: Version 10 from 2024-11-1615766  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 51040b7..cfc6cee 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -252,7 +252,7 @@ in VS-Code) in a separate window. @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} +@tab @code{lean4-execute} @item @samp{C-c C-p C-l} @tab Builds package with lake @tab @code{lean4-lake-build} @@ -384,6 +384,9 @@ expect that noone has been using it. If you do use it, let us know, so we can reconsider our decision in case of a substantial amount of users. Otherwise, please just define these functions in your Emacs initialization file yourself. +@item +The command @code{lean4-std-exe} has been removed. It was just the same +as @code{lean4-execute} which continues to exist. @end itemize @node Version 112 from 2024-12-10 diff --git a/lean4-settings.el b/lean4-settings.el index 0285d51..24a4f2c 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -103,10 +103,10 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." :type 'boolean) (defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x") - "Main Keybinding for `lean4-std-exe'." + "Main Keybinding for `lean4-execute'." :group 'lean4-keybinding :type 'key-sequence) (defcustom lean4-keybinding-std-exe2 (kbd "C-c C-l") - "Alternative Keybinding for `lean4-std-exe'." + "Alternative Keybinding for `lean4-execute'." :group 'lean4-keybinding :type 'key-sequence) (defcustom lean4-keybinding-show-key (kbd "C-c C-k") "Lean Keybinding for `quail-show-key'." From ec12cee25ae412cbc2bd8377d9c26213189f7a58 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:05 +0200 Subject: [PATCH 10/50] [lake][util] Delete; minimalist approach in [mode]; shrink [settings] --- lean4-fringe.el | 1 - lean4-info.el | 1 - lean4-lake.el | 52 ------------------------------------ lean4-mode.el | 68 ++++++++++++++--------------------------------- lean4-settings.el | 47 -------------------------------- lean4-util.el | 59 ---------------------------------------- 6 files changed, 20 insertions(+), 208 deletions(-) delete mode 100644 lean4-lake.el delete mode 100644 lean4-util.el diff --git a/lean4-fringe.el b/lean4-fringe.el index e5ab9e0..24578f6 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -22,7 +22,6 @@ ;;; Code: -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) diff --git a/lean4-info.el b/lean4-info.el index 923cf56..12ae44d 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -24,7 +24,6 @@ (require 'dash) (require 'lean4-syntax) -(require 'lean4-settings) (require 'lsp-mode) (require 'lsp-protocol) (require 'magit-section) diff --git a/lean4-lake.el b/lean4-lake.el deleted file mode 100644 index 125aca1..0000000 --- a/lean4-lake.el +++ /dev/null @@ -1,52 +0,0 @@ -;;; lean4-lake.el --- Lean4-Mode Lake Integration -*- lexical-binding: t; -*- - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library provides integration with Lake, Lean 4 build system and package -;; manager. - -;;; Code: - -(require 'lean4-util) -(require 'lean4-settings) - -(defun lean4-root-dir-p (dir) - "Check if directory DIR contains \"lakefile.lean\" or \"lakefile.toml\"." - (or - (file-exists-p (expand-file-name "lakefile.lean" dir)) - (file-exists-p (expand-file-name "lakefile.toml" dir)))) - -(defun lean4-lake-find-dir () - "Find a parent directory of the current file with a Lake file. - - It looks for files named \"lakefile.lean\" or \"lakefile.toml\" file." - (and (buffer-file-name) - (locate-dominating-file (buffer-file-name) #'lean4-root-dir-p))) - -(defun lean4-lake-find-dir-safe () - "Call `lean4-lake-find-dir', error on failure." - (or (lean4-lake-find-dir) - (error "Cannot find lakefile in any directory above %s" (buffer-file-name)))) - -(defun lean4-lake-build () - "Call lake build." - (interactive) - (let ((default-directory (file-name-as-directory (lean4-lake-find-dir-safe)))) - (compile (concat (lean4-get-executable lean4-lake-name) " build")))) - -(provide 'lean4-lake) -;;; lean4-lake.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 6992002..f64c286 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -46,12 +46,9 @@ (require 'pcase) (require 'lsp-mode) (require 'lean4-eri) -(require 'lean4-util) -(require 'lean4-settings) (require 'lean4-syntax) (require 'lean4-info) (require 'lean4-fringe) -(require 'lean4-lake) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: @@ -65,41 +62,26 @@ (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") (declare-function quail-show-key "quail") -(defun lean4-compile-string (lake-name exe-name args file-name) - "Command to run EXE-NAME with extra ARGS and FILE-NAME. -If LAKE-NAME is nonempty, then prepend \"LAKE-NAME env\" to the command -\"EXE-NAME ARGS FILE-NAME\"." - (if lake-name - (format "%s env %s %s %s" lake-name exe-name args file-name) - (format "%s %s %s" exe-name args file-name))) - -(defun lean4-create-temp-in-system-tempdir (file-name prefix) - "Create a temp lean file and return its name. -The new file has prefix PREFIX (defaults to `flymake') and the same extension as -FILE-NAME." - (make-temp-file (or prefix "flymake") nil (file-name-extension file-name))) - -(defun lean4-execute (&optional arg) - "Execute Lean in the current buffer with an optional argument ARG." +(defcustom lean4-location-root nil + "Lean4 project root, used as `default-directory'." + :type 'directory + :group 'lean4) + +(defun lean4-execute () + "Execute Lean in the current buffer." + (interactive) + (let* ((default-directory + (or lean4-location-root default-directory))) + (compile (if-let* ((file (buffer-file-name))) + (concat "lean " file " ") + "lean ")))) + +(defun lean4-lake-build () + "Build Lean4 project with Lake." (interactive) - (when (called-interactively-p 'any) - (setq arg (read-string "arg: " arg))) - (let* ((cc compile-command) - (dd default-directory) - (use-lake (lean4-lake-find-dir)) - (default-directory (if use-lake (lean4-lake-find-dir) dd)) - (target-file-name - (or - (buffer-file-name) - (flymake-proc-init-create-temp-buffer-copy 'lean4-create-temp-in-system-tempdir)))) - (compile (lean4-compile-string - (if use-lake (shell-quote-argument (expand-file-name (lean4-get-executable lean4-lake-name))) nil) - (shell-quote-argument (expand-file-name (lean4-get-executable lean4-executable-name))) - (or arg "") - (shell-quote-argument (expand-file-name target-file-name)))) - ;; restore old value - (setq compile-command cc) - (setq default-directory dd))) + (let* ((default-directory + (or lean4-location-root default-directory))) + (compile "lake build "))) (defun lean4-refresh-file-dependencies () "Refresh the file dependencies. @@ -239,18 +221,8 @@ of the parent project." (add-to-list 'lsp-language-id-configuration '(lean4-mode . "lean")) -(defun lean4--server-cmd () - "Return Lean server command. -If found lake version at least 3.1.0, then return '/path/to/lake serve', -otherwise return '/path/to/lean --server'." - (condition-case nil - (if (string-version-lessp (car (process-lines (lean4-get-executable "lake") "--version")) "3.1.0") - `(,(lean4-get-executable lean4-executable-name) "--server") - `(,(lean4-get-executable "lake") "serve")) - (error `(,(lean4-get-executable lean4-executable-name) "--server")))) - (lsp-register-client - (make-lsp-client :new-connection (lsp-stdio-connection #'lean4--server-cmd) + (make-lsp-client :new-connection (lsp-stdio-connection '("lake" "serve")) :major-modes '(lean4-mode) :server-id 'lean4-lsp :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) diff --git a/lean4-settings.el b/lean4-settings.el index 24a4f2c..c9bc12c 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -22,9 +22,6 @@ ;;; Code: -(require 'cl-lib) -(require 'lsp-mode) - (defgroup lean4 nil "Major mode for Lean4 programming language and theorem prover." :group 'languages @@ -40,56 +37,12 @@ :prefix "lean4-" :group 'lean4) -(defconst lean4-default-executable-name - (cl-case system-type - (windows-nt "lean.exe") - (t "lean")) - "Default executable name of Lean.") - -(defconst lean4-default-lake-name - (cl-case system-type - (windows-nt "lake.exe") - (t "lake")) - "Default executable name of Lake.") - (defcustom lean4-mode-hook (list #'lsp) "Hook run after entering `lean4-mode'." :options '(flycheck-mode lsp) :type 'hook :group 'lean4) -(defcustom lean4-rootdir nil - "Full pathname of lean root directory. It should be defined by user." - :group 'lean4 - :type 'string) - -(defcustom lean4-executable-name lean4-default-executable-name - "Name of lean executable." - :group 'lean4 - :type 'string) - -(defcustom lean4-lake-name lean4-default-lake-name - "Name of lake executable." - :group 'lake - :type 'string) - -(defcustom lean4-memory-limit 1024 - "Memory limit for lean process in megabytes." - :group 'lean4 - :type 'number) - -(defcustom lean4-timeout-limit 100000 - "Deterministic timeout limit. - -It is approximately the maximum number of memory allocations in thousands." - :group 'lean4 - :type 'number) - -(defcustom lean4-extra-arguments nil - "Extra command-line arguments to the lean process." - :group 'lean4 - :type '(list string)) - (defcustom lean4-highlight-inaccessible-names t "Use font to highlight inaccessible names. Set this variable to t to highlight inaccessible names in the info display diff --git a/lean4-util.el b/lean4-util.el deleted file mode 100644 index 2b8cdab..0000000 --- a/lean4-util.el +++ /dev/null @@ -1,59 +0,0 @@ -;;; lean4-util.el --- Lean4-Mode Utilities -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library provides utilities for `lean4-mode'. - -;;; Code: - -(require 'compat) -(require 'lean4-settings) - -(defun lean4-setup-rootdir () - "Search for lean executable in variable `exec-path'. -Try to find an executable named `lean4-executable-name' in variable `exec-path'. -On succsess, return path to the directory with this executable." - (let ((root (executable-find lean4-executable-name))) - (when root - (setq lean4-rootdir (file-name-directory - (directory-file-name - (file-name-directory root))))) - lean4-rootdir)) - -(defun lean4-get-rootdir () - "Search for lean executable in `lean4-rootdir' and variable `exec-path'. -First try to find an executable named `lean4-executable-name' in -`lean4-rootdir'. On failure, search in variable `exec-path'." - (if lean4-rootdir - (let ((lean4-path (expand-file-name lean4-executable-name (expand-file-name "bin" lean4-rootdir)))) - (unless (file-exists-p lean4-path) - (error "Incorrect `lean4-rootdir' value, path '%s' does not exist" lean4-path)) - lean4-rootdir) - (or - (lean4-setup-rootdir) - (error - (concat "Lean was not found in the `exec-path' and `lean4-rootdir' is not defined. " - "Please set it via M-x customize-variable RET lean4-rootdir RET."))))) - -(defun lean4-get-executable (exe-name) - "Return fullpath of lean executable EXE-NAME." - (file-name-concat (lean4-get-rootdir) "bin" exe-name)) - -(provide 'lean4-util) -;;; lean4-util.el ends here From 3f8922b670afb46c9116887c0ba3511560a30dc1 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:08 +0200 Subject: [PATCH 11/50] [mode][settings] Refactor keybindings --- lean4-mode.el | 28 +++++++++------------------- lean4-settings.el | 33 --------------------------------- 2 files changed, 9 insertions(+), 52 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index f64c286..7cb2c3d 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -107,24 +107,15 @@ file, recompiling, and reloading all imports." (lean4-eri-indent)) (t (indent-for-tab-command)))) -(defun lean4-set-keys () - "Setup Lean4 keybindings." - (local-set-key lean4-keybinding-std-exe1 #'lean4-execute) - (local-set-key lean4-keybinding-std-exe2 #'lean4-execute) - (local-set-key lean4-keybinding-show-key #'quail-show-key) - (local-set-key lean4-keybinding-tab-indent #'lean4-tab-indent) - ;; (local-set-key lean4-keybinding-hole #'lean4-hole) - (local-set-key lean4-keybinding-lean4-toggle-info #'lean4-toggle-info) - ;; (local-set-key lean4-keybinding-lean4-message-boxes-toggle #'lean4-message-boxes-toggle) - (local-set-key lean4-keybinding-lake-build #'lean4-lake-build) - (local-set-key lean4-keybinding-refresh-file-dependencies #'lean4-refresh-file-dependencies) - ;; This only works as a mouse binding due to the event, so it is not abstracted - ;; to avoid user confusion. - ;; (local-set-key (kbd "") #'lean4-right-click-show-menu) - ) - -(defvar lean4-mode-map (make-sparse-keymap) - "Keymap used in Lean mode.") +(defvar-keymap lean4-mode-map + :doc "Keymap for `lean4-mode'." + "C-c C-x" #'lean4-execute + "C-c C-l" #'lean4-execute + "C-c C-k" #'quail-show-key + "TAB" #'lean4-tab-indent + "C-c C-i" #'lean4-toggle-info + "C-c C-p C-l" #'lean4-lake-build + "C-c C-d" #'lean4-refresh-file-dependencies) (easy-menu-define lean4-mode-menu lean4-mode-map "Menu for the Lean major mode." @@ -195,7 +186,6 @@ of the parent project." (set-input-method "Lean") (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function) - (lean4-set-keys) (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1)) (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist) diff --git a/lean4-settings.el b/lean4-settings.el index c9bc12c..a151d2c 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -32,11 +32,6 @@ :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") :prefix "lean4-") -(defgroup lean4-keybinding nil - "Keybindings for lean4-mode." - :prefix "lean4-" - :group 'lean4) - (defcustom lean4-mode-hook (list #'lsp) "Hook run after entering `lean4-mode'." :options '(flycheck-mode lsp) @@ -55,33 +50,5 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." :group 'lean4 :type 'boolean) -(defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x") - "Main Keybinding for `lean4-execute'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-std-exe2 (kbd "C-c C-l") - "Alternative Keybinding for `lean4-execute'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-show-key (kbd "C-c C-k") - "Lean Keybinding for `quail-show-key'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-server-restart (kbd "C-c C-r") - "Lean Keybinding for server-restart." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-tab-indent (kbd "TAB") - "Lean Keybinding for `lean4-tab-indent'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-auto-complete (kbd "S-SPC") - "Lean Keybinding for auto completion." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-lean4-toggle-info (kbd "C-c C-i") - "Lean Keybinding for `lean4-toggle-info'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-lake-build (kbd "C-c C-p C-l") - "Lean Keybinding for `lean4-lake-build'." - :group 'lean4-keybinding :type 'key-sequence) -(defcustom lean4-keybinding-refresh-file-dependencies (kbd "C-c C-d") - "Lean Keybinding for `lean4-refresh-file-dependencies'." - :group 'lean4-keybinding :type 'key-sequence) - (provide 'lean4-settings) ;;; lean4-settings.el ends here From 4d33141c8c1fcdf379bfc1121883e2cc37b008fe Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:11 +0200 Subject: [PATCH 12/50] [settings] Move lean4-show-file-progress to [fringe] --- lean4-fringe.el | 5 +++++ lean4-settings.el | 5 ----- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lean4-fringe.el b/lean4-fringe.el index 24578f6..e942a0a 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -25,6 +25,11 @@ (require 'lsp-mode) (require 'lsp-protocol) +(defcustom lean4-show-file-progress t + "Highlight file progress in the current buffer." + :group 'lean4 + :type 'boolean) + (eval-and-compile (lsp-interface (lean:LeanFileProgressProcessingInfo (:range :kind) nil) diff --git a/lean4-settings.el b/lean4-settings.el index a151d2c..9573756 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -45,10 +45,5 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." :group 'lean4 :type 'boolean) -(defcustom lean4-show-file-progress t - "Highlight file progress in the current buffer." - :group 'lean4 - :type 'boolean) - (provide 'lean4-settings) ;;; lean4-settings.el ends here From 05906e8b6980ac3e87105f6c6a5ca918223e91ad Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:15 +0200 Subject: [PATCH 13/50] [settings] Move lean4-highlight-inaccessible-names to [info] --- lean4-info.el | 7 +++++++ lean4-settings.el | 7 ------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 12ae44d..c180e07 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -32,6 +32,13 @@ "Lean4-Mode Info." :group 'lean4) +(defcustom lean4-highlight-inaccessible-names t + "Use font to highlight inaccessible names. +Set this variable to t to highlight inaccessible names in the info display +using `font-lock-comment-face' instead of the `✝` suffix used by Lean." + :group 'lean4-info + :type 'boolean) + ;; Lean Info Mode (for "*lean4-info*" buffer) ;; Automode List ;;;###autoload diff --git a/lean4-settings.el b/lean4-settings.el index 9573756..7b9dd79 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -38,12 +38,5 @@ :type 'hook :group 'lean4) -(defcustom lean4-highlight-inaccessible-names t - "Use font to highlight inaccessible names. -Set this variable to t to highlight inaccessible names in the info display -using `font-lock-comment-face' instead of the `✝` suffix used by Lean." - :group 'lean4 - :type 'boolean) - (provide 'lean4-settings) ;;; lean4-settings.el ends here From f74e958ee4f54746a88851c2b6de7c5551e2aa41 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:18 +0200 Subject: [PATCH 14/50] [settings] Move customization group and mode hook to [mode] --- lean4-mode.el | 16 ++++++++++++++++ lean4-settings.el | 16 ---------------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index 7cb2c3d..69df11b 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -62,6 +62,22 @@ (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") (declare-function quail-show-key "quail") +(defgroup lean4 nil + "Major mode for Lean4 programming language and theorem prover." + :group 'languages + :link '(info-link :tag "Info Manual" "(lean4-mode)") + :link '(url-link + :tag "Website" + "https://github.com/leanprover-community/lean4-mode") + :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") + :prefix "lean4-") + +(defcustom lean4-mode-hook (list #'lsp) + "Hook run after entering `lean4-mode'." + :options '(flycheck-mode lsp) + :type 'hook + :group 'lean4) + (defcustom lean4-location-root nil "Lean4 project root, used as `default-directory'." :type 'directory diff --git a/lean4-settings.el b/lean4-settings.el index 7b9dd79..e411250 100644 --- a/lean4-settings.el +++ b/lean4-settings.el @@ -22,21 +22,5 @@ ;;; Code: -(defgroup lean4 nil - "Major mode for Lean4 programming language and theorem prover." - :group 'languages - :link '(info-link :tag "Info Manual" "(lean4-mode)") - :link '(url-link - :tag "Website" - "https://github.com/leanprover-community/lean4-mode") - :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") - :prefix "lean4-") - -(defcustom lean4-mode-hook (list #'lsp) - "Hook run after entering `lean4-mode'." - :options '(flycheck-mode lsp) - :type 'hook - :group 'lean4) - (provide 'lean4-settings) ;;; lean4-settings.el ends here From 88d59983d6ca0278d44a5c7fab1e150d66ae20da Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:22 +0200 Subject: [PATCH 15/50] [settings] Delete --- lean4-settings.el | 26 -------------------------- 1 file changed, 26 deletions(-) delete mode 100644 lean4-settings.el diff --git a/lean4-settings.el b/lean4-settings.el deleted file mode 100644 index e411250..0000000 --- a/lean4-settings.el +++ /dev/null @@ -1,26 +0,0 @@ -;;; lean4-settings.el --- Lean4-Mode User-Options -*- lexical-binding: t; -*- - -;; Copyright (c) 2014 Microsoft Corporation. All rights reserved. - -;; This file is not part of GNU Emacs. - -;; Licensed under the Apache License, Version 2.0 (the "License"); you -;; may not use this file except in compliance with the License. You -;; may obtain a copy of the License at -;; -;; http://www.apache.org/licenses/LICENSE-2.0 -;; -;; Unless required by applicable law or agreed to in writing, software -;; distributed under the License is distributed on an "AS IS" BASIS, -;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or -;; implied. See the License for the specific language governing -;; permissions and limitations under the License. - -;;; Commentary: - -;; This library defines custom variables for `lean4-mode'. - -;;; Code: - -(provide 'lean4-settings) -;;; lean4-settings.el ends here From 77b844cfb17263485b8e8b6897c7e13d9d210589 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:25 +0200 Subject: [PATCH 16/50] [mode] Move lean4-tab-indent to [eri] --- lean4-eri.el | 7 +++++++ lean4-mode.el | 7 ------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lean4-eri.el b/lean4-eri.el index a85b474..2826307 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -223,5 +223,12 @@ are calculated." (interactive) (lean4-eri-indent t)) +(defun lean4-tab-indent () + "Lean 4 function for TAB indent." + (interactive) + (cond ((looking-back (rx line-start (* white)) nil) + (lean4-eri-indent)) + (t (indent-for-tab-command)))) + (provide 'lean4-eri) ;;; lean4-eri.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 69df11b..369e1f5 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -116,13 +116,6 @@ file, recompiling, and reloading all imports." :version lsp--cur-version :text (lsp--buffer-content))))) -(defun lean4-tab-indent () - "Lean 4 function for TAB indent." - (interactive) - (cond ((looking-back (rx line-start (* white)) nil) - (lean4-eri-indent)) - (t (indent-for-tab-command)))) - (defvar-keymap lean4-mode-map :doc "Keymap for `lean4-mode'." "C-c C-x" #'lean4-execute From 884ef653d136c9b9f001f24ea9befbd7877845f4 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:28 +0200 Subject: [PATCH 17/50] [mode] Move code to new command lean4-input-set in [input] --- lean4-input.el | 5 +++++ lean4-mode.el | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/lean4-input.el b/lean4-input.el index 0051b4e..6760add 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -310,5 +310,10 @@ Suitable for use in the :set field of `defcustom'." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Administrative details +(defun lean4-input-set () + (interactive) + "Select and activate the `Lean' input method." + (set-input-method "Lean")) + (provide 'lean4-input) ;;; lean4-input.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 369e1f5..47a715b 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -49,6 +49,7 @@ (require 'lean4-syntax) (require 'lean4-info) (require 'lean4-fringe) +(require 'lean4-input) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: @@ -191,8 +192,7 @@ of the parent project." (set (make-local-variable 'font-lock-defaults) lean4-font-lock-defaults) (set (make-local-variable 'indent-tabs-mode) nil) (set 'compilation-mode-font-lock-keywords '()) - (require 'lean4-input) - (set-input-method "Lean") + (lean4-input-set) (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function) (if (fboundp 'electric-indent-local-mode) From 1f15b9296a2fb58f93a378adbf0009221022893d Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:32 +0200 Subject: [PATCH 18/50] [mode] Move addition to markdown-code-lang-modes to [markdown] --- lean4-markdown.el | 31 +++++++++++++++++++++++++++++++ lean4-mode.el | 7 +------ 2 files changed, 32 insertions(+), 6 deletions(-) create mode 100644 lean4-markdown.el diff --git a/lean4-markdown.el b/lean4-markdown.el new file mode 100644 index 0000000..df2ef9d --- /dev/null +++ b/lean4-markdown.el @@ -0,0 +1,31 @@ +;;; lean4-markdown.el --- Lean4 Markdown Integration -*- lexical-binding: t; -*- + +;; Copyright (c) 2025 Mekeor Melire + +;; This file is NOT part of GNU Emacs. + +;; Licensed under the Apache License, Version 2.0 (the "License"); you +;; may not use this file except in compliance with the License. You +;; may obtain a copy of the License at +;; +;; http://www.apache.org/licenses/LICENSE-2.0 +;; +;; Unless required by applicable law or agreed to in writing, software +;; distributed under the License is distributed on an "AS IS" BASIS, +;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +;; implied. See the License for the specific language governing +;; permissions and limitations under the License. + +;;; Commentary: + +;; This file connects `lean4-mode' and `markdown-mode' packages. + +;;; Code: + +(require 'markdown-mode) + +(add-to-list 'markdown-code-lang-modes + '("lean" . lean4-mode)) + +(provide 'lean4-markdown) +;;; lean4-markdown.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 47a715b..0a04ad1 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -50,6 +50,7 @@ (require 'lean4-info) (require 'lean4-fringe) (require 'lean4-input) +(require 'lean4-markdown) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: @@ -58,7 +59,6 @@ (defvar flycheck-disabled-checkers) (defvar flycheck-mode) (defvar lsp--cur-version) -(defvar markdown-code-lang-modes) (declare-function flycheck-list-errors "ext:flycheck") (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") (declare-function quail-show-key "quail") @@ -206,11 +206,6 @@ of the parent project." (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) -;;;###autoload -(with-eval-after-load 'markdown-mode - (add-to-list 'markdown-code-lang-modes - '("lean" . lean4-mode))) - ;; Use utf-8 encoding ;;;### autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) From fc3fc91b6741978912709864b399c93b6b80a7ea Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:35 +0200 Subject: [PATCH 19/50] [mode] Move lsp-mode related definitions to [lsp] --- lean4-lsp.el | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++ lean4-mode.el | 49 +-------------------------------- 2 files changed, 76 insertions(+), 48 deletions(-) create mode 100644 lean4-lsp.el diff --git a/lean4-lsp.el b/lean4-lsp.el new file mode 100644 index 0000000..09664e5 --- /dev/null +++ b/lean4-lsp.el @@ -0,0 +1,75 @@ +;;; lean4-lsp.el --- Lean4 lsp-mode -*- lexical-binding: t; -*- + +;; Copyright (c) 2025 Mekeor Melire + +;; This file is NOT part of GNU Emacs. + +;; Licensed under the Apache License, Version 2.0 (the "License"); you +;; may not use this file except in compliance with the License. You +;; may obtain a copy of the License at +;; +;; http://www.apache.org/licenses/LICENSE-2.0 +;; +;; Unless required by applicable law or agreed to in writing, software +;; distributed under the License is distributed on an "AS IS" BASIS, +;; WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or +;; implied. See the License for the specific language governing +;; permissions and limitations under the License. + +;;; Commentary: + +;; This file connects `lean4-mode' and `lsp-mode' packages. + +;;; Code: + +(require 'lsp-mode) + +(defun lean4-refresh-file-dependencies () + "Refresh the file dependencies. + +This function restarts the server subprocess for the current +file, recompiling, and reloading all imports." + (interactive) + (lsp-notify + "textDocument/didClose" + `(:textDocument ,(lsp--text-document-identifier))) + (lsp-notify + "textDocument/didOpen" + (list :textDocument + (list :uri (lsp--buffer-uri) + :languageId (lsp-buffer-language) + :version lsp--cur-version + :text (lsp--buffer-content))))) + +(defun lean4-create-lsp-workspace () + "Create an LSP workspace. + +Starting from `(buffer-file-name)`, repeatedly look up the +directory hierarchy for a directory containing a file +\"lean-toolchain\", and use the last such directory found, if any. +This allows us to edit files in child packages using the settings +of the parent project." + (let (root) + (when-let ((file-name (buffer-file-name))) + (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) + ;; We found a toolchain file, but maybe it belongs to a package. + ;; Continue looking until there are no more toolchain files. + (setq root dir + file-name (file-name-directory (directory-file-name dir))))) + (when root + (lsp-workspace-folders-add root)))) + +;;;; Registration + +(add-to-list 'lsp-language-id-configuration + '(lean4-mode . "lean")) + +(lsp-register-client + (make-lsp-client :new-connection (lsp-stdio-connection '("lake" "serve")) + :major-modes '(lean4-mode) + :server-id 'lean4-lsp + :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) + :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) + +(provide 'lean4-lsp) +;;; lean4-lsp.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 0a04ad1..7088fd0 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -51,6 +51,7 @@ (require 'lean4-fringe) (require 'lean4-input) (require 'lean4-markdown) +(require 'lean4-lsp) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: @@ -58,7 +59,6 @@ (defvar flycheck-after-syntax-check-hook) (defvar flycheck-disabled-checkers) (defvar flycheck-mode) -(defvar lsp--cur-version) (declare-function flycheck-list-errors "ext:flycheck") (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") (declare-function quail-show-key "quail") @@ -100,23 +100,6 @@ (or lean4-location-root default-directory))) (compile "lake build "))) -(defun lean4-refresh-file-dependencies () - "Refresh the file dependencies. - -This function restarts the server subprocess for the current -file, recompiling, and reloading all imports." - (interactive) - (lsp-notify - "textDocument/didClose" - `(:textDocument ,(lsp--text-document-identifier))) - (lsp-notify - "textDocument/didOpen" - (list :textDocument - (list :uri (lsp--buffer-uri) - :languageId (lsp-buffer-language) - :version lsp--cur-version - :text (lsp--buffer-content))))) - (defvar-keymap lean4-mode-map :doc "Keymap for `lean4-mode'." "C-c C-x" #'lean4-execute @@ -158,24 +141,6 @@ enabled and disabled respectively.") (setq-local lsp-semantic-tokens-enable t) (lean4-create-lsp-workspace)) -(defun lean4-create-lsp-workspace () - "Create an LSP workspace. - -Starting from `(buffer-file-name)`, repeatedly look up the -directory hierarchy for a directory containing a file -\"lean-toolchain\", and use the last such directory found, if any. -This allows us to edit files in child packages using the settings -of the parent project." - (let (root) - (when-let ((file-name (buffer-file-name))) - (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) - ;; We found a toolchain file, but maybe it belongs to a package. - ;; Continue looking until there are no more toolchain files. - (setq root dir - file-name (file-name-directory (directory-file-name dir))))) - (when root - (lsp-workspace-folders-add root)))) - ;;;###autoload (define-derived-mode lean4-mode prog-mode "Lean 4" "Major mode for Lean language. @@ -210,17 +175,5 @@ of the parent project." ;;;### autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) -;; LSP init -;; Ref: https://emacs-lsp.github.io/lsp-mode/page/adding-new-language/ -(add-to-list 'lsp-language-id-configuration - '(lean4-mode . "lean")) - -(lsp-register-client - (make-lsp-client :new-connection (lsp-stdio-connection '("lake" "serve")) - :major-modes '(lean4-mode) - :server-id 'lean4-lsp - :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) - :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) - (provide 'lean4-mode) ;;; lean4-mode.el ends here From abf66c41a81ffe06cac5599cfbd853df537a3330 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:11:38 +0200 Subject: [PATCH 20/50] [fringe] For lean4-fringe- prefix, rename lean4-show-file-progress --- lean4-fringe.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-fringe.el b/lean4-fringe.el index e942a0a..3ab6807 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -25,7 +25,7 @@ (require 'lsp-mode) (require 'lsp-protocol) -(defcustom lean4-show-file-progress t +(defcustom lean4-fringe-show-file-progress t "Highlight file progress in the current buffer." :group 'lean4 :type 'boolean) @@ -79,7 +79,7 @@ (dolist (ov (flatten-tree (overlay-lists))) (when (eq (overlay-get ov 'face) 'lean4-fringe-face) (delete-overlay ov))) - (when lean4-show-file-progress + (when lean4-fringe-show-file-progress (seq-doseq (item lean4-fringe-data) (let* ((reg (lean4-fringe-region item)) (ov (make-overlay (car reg) (cdr reg)))) From cdb5f31855a39b729ece8ddac004fe859f99248b Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:12:23 +0200 Subject: [PATCH 21/50] [lsp] For lean4-lsp- prefix, rename definitions --- README.org | 14 +++++++------- lean4-lsp.el | 4 ++-- lean4-mode.el | 4 ++-- lean4-mode.info | 30 +++++++++++++++--------------- lean4-mode.texi | 4 ++-- 5 files changed, 28 insertions(+), 28 deletions(-) diff --git a/README.org b/README.org index 580d652..babe973 100644 --- a/README.org +++ b/README.org @@ -150,13 +150,13 @@ 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. -| 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-execute~ | -| =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | -| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | +| Key | Description | Command | +|------------------------+--------------------------------------------------------+-----------------------------| +| =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | +| =C-c C-d= | Recompile and reload imports | ~lean4-lsp-document-reopen~ | +| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-execute~ | +| =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | +| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | ** lsp-mode diff --git a/lean4-lsp.el b/lean4-lsp.el index 09664e5..df24742 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -24,7 +24,7 @@ (require 'lsp-mode) -(defun lean4-refresh-file-dependencies () +(defun lean4-lsp-document-reopen () "Refresh the file dependencies. This function restarts the server subprocess for the current @@ -41,7 +41,7 @@ file, recompiling, and reloading all imports." :version lsp--cur-version :text (lsp--buffer-content))))) -(defun lean4-create-lsp-workspace () +(defun lean4-lsp-workspace-add () "Create an LSP workspace. Starting from `(buffer-file-name)`, repeatedly look up the diff --git a/lean4-mode.el b/lean4-mode.el index 7088fd0..47648b2 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -108,7 +108,7 @@ "TAB" #'lean4-tab-indent "C-c C-i" #'lean4-toggle-info "C-c C-p C-l" #'lean4-lake-build - "C-c C-d" #'lean4-refresh-file-dependencies) + "C-c C-d" #'lean4-lsp-document-reopen) (easy-menu-define lean4-mode-menu lean4-mode-map "Menu for the Lean major mode." @@ -139,7 +139,7 @@ enabled and disabled respectively.") (setq-local flycheck-disabled-checkers '()) ;; Lean massively benefits from semantic tokens, so change default to enabled (setq-local lsp-semantic-tokens-enable t) - (lean4-create-lsp-workspace)) + (lean4-lsp-workspace-add)) ;;;###autoload (define-derived-mode lean4-mode prog-mode "Lean 4" diff --git a/lean4-mode.info b/lean4-mode.info index 6c1cf8a..12638ca 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -237,9 +237,9 @@ will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. Key Description Command ----------------------------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------------- ‘C-c C-k’ Echo the keystroke needed to input the symbol at point ‘quail-show-key’ -‘C-c C-d’ Recompile and reload imports ‘lean4-refresh-file-dependencies’ +‘C-c C-d’ Recompile and reload imports ‘lean4-lsp-document-reopen’ ‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ ‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’ @@ -447,19 +447,19 @@ Node: Native vc (Emacs 30 or later)5416 Node: Doom-Emacs6324 Node: Straight6750 Node: Usage7250 -Node: lsp-mode8696 -Node: Flycheck8981 -Node: Configuration9591 -Node: lsp-mode (1)9781 -Node: Flycheck (1)10050 -Node: Common Pitfalls10535 -Node: Changelog11127 -Node: Upcoming Version11567 -Node: Version 112 from 2024-12-1013633 -Node: Version 111 from 2024-12-0214498 -Node: Version 110 from 2024-12-0114905 -Node: Version 101 from 2024-11-2115403 -Node: Version 10 from 2024-11-1615766 +Node: lsp-mode8684 +Node: Flycheck8969 +Node: Configuration9579 +Node: lsp-mode (1)9769 +Node: Flycheck (1)10038 +Node: Common Pitfalls10523 +Node: Changelog11115 +Node: Upcoming Version11555 +Node: Version 112 from 2024-12-1013621 +Node: Version 111 from 2024-12-0214486 +Node: Version 110 from 2024-12-0114893 +Node: Version 101 from 2024-11-2115391 +Node: Version 10 from 2024-11-1615754  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index cfc6cee..4c524fb 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -240,7 +240,7 @@ 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. -@multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} +@multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaa} @headitem Key @tab Description @tab Command @@ -249,7 +249,7 @@ in VS-Code) in a separate window. @tab @code{quail-show-key} @item @samp{C-c C-d} @tab Recompile and reload imports -@tab @code{lean4-refresh-file-dependencies} +@tab @code{lean4-lsp-document-reopen} @item @samp{C-c C-x} or @samp{C-c C-l} @tab Execute Lean in stand-alone mode @tab @code{lean4-execute} From cb2e7112cfde19608e26def398dccdbaacdc80ab Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:12:27 +0200 Subject: [PATCH 22/50] [eri] For lean4-eri- prefix, rename lean4-tab-indent --- lean4-eri.el | 2 +- lean4-mode.el | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-eri.el b/lean4-eri.el index 2826307..d1f1c1d 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -223,7 +223,7 @@ are calculated." (interactive) (lean4-eri-indent t)) -(defun lean4-tab-indent () +(defun lean4-eri-tab () "Lean 4 function for TAB indent." (interactive) (cond ((looking-back (rx line-start (* white)) nil) diff --git a/lean4-mode.el b/lean4-mode.el index 47648b2..96d9e47 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -105,7 +105,7 @@ "C-c C-x" #'lean4-execute "C-c C-l" #'lean4-execute "C-c C-k" #'quail-show-key - "TAB" #'lean4-tab-indent + "TAB" #'lean4-eri-tab "C-c C-i" #'lean4-toggle-info "C-c C-p C-l" #'lean4-lake-build "C-c C-d" #'lean4-lsp-document-reopen) From 2ee1c5ba20532f474bee25a51a1a40f70ac0f654 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:12:30 +0200 Subject: [PATCH 23/50] [info] For lean4-info- prefix, rename definitions --- README.org | 4 ++-- lean4-info.el | 32 ++++++++++++++++---------------- lean4-mode.el | 4 ++-- lean4-mode.info | 4 ++-- lean4-mode.texi | 4 ++-- 5 files changed, 24 insertions(+), 24 deletions(-) diff --git a/README.org b/README.org index babe973..711d2fd 100644 --- a/README.org +++ b/README.org @@ -146,7 +146,7 @@ will ask you to identify the /project/ this file belongs to. If you then type =#check id=, the word =#check= will be underlined, and hovering over it will show you the type of ~id~. -To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=). This +To view the proof state, run ~lean4-info-toggle~ (=C-c C-i=). This will display the =*Lean Goals*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. @@ -156,7 +156,7 @@ in VS-Code) in a separate window. | =C-c C-d= | Recompile and reload imports | ~lean4-lsp-document-reopen~ | | =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-execute~ | | =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | -| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~ | +| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-info-toggle-buffer~ | ** lsp-mode diff --git a/lean4-info.el b/lean4-info.el index c180e07..4af37ea 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -32,7 +32,7 @@ "Lean4-Mode Info." :group 'lean4) -(defcustom lean4-highlight-inaccessible-names t +(defcustom lean4-info-highlight-inaccessibles t "Use font to highlight inaccessible names. Set this variable to t to highlight inaccessible names in the info display using `font-lock-comment-face' instead of the `✝` suffix used by Lean." @@ -52,7 +52,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function)) -(defun lean4-ensure-info-buffer (buffer) +(defun lean4-info-ensure-buffer (buffer) "Create BUFFER if it does not exist. Also choose settings used for the *Lean Goal* buffer." (unless (get-buffer buffer) @@ -62,12 +62,12 @@ Also choose settings used for the *Lean Goal* buffer." (set-syntax-table lean4-syntax-table) (setq buffer-read-only t)))) -(defun lean4-toggle-info-buffer (buffer) +(defun lean4-info-toggle-buffer (buffer) "Create or delete BUFFER. The buffer is supposed to be the *Lean Goal* buffer." (-if-let (window (get-buffer-window buffer)) (quit-window nil window) - (lean4-ensure-info-buffer buffer) + (lean4-info-ensure-buffer buffer) (display-buffer buffer))) (defun lean4-info-buffer-active (buffer) @@ -88,8 +88,8 @@ The buffer is supposed to be the *Lean Goal* buffer." (defconst lean4-info-buffer-name "*Lean Goal*") -(defvar lean4-goals nil) -(defvar lean4-term-goal nil) +(defvar lean4-info-goals nil) +(defvar lean4-info-term-goal nil) (lsp-defun lean4-diagnostic-full-start-line ((&lean:Diagnostic :full-range (&Range :start (&Position :line)))) line) @@ -109,7 +109,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (defun lean4-info--insert-highlight-inaccessible-names (&rest text) (let ((begin (point))) (apply #'insert text) - (when lean4-highlight-inaccessible-names + (when lean4-info-highlight-inaccessibles (let ((end (point-marker))) (goto-char begin) (while (re-search-forward "\\(\\sw+\\)✝\\([¹²³⁴-⁹⁰]*\\)" end t) @@ -120,7 +120,7 @@ The buffer is supposed to be the *Lean Goal* buffer." 'fixedcase 'literal)) (goto-char end))))) -(defun lean4--insert-goal-text (text delimiter) +(defun lean4-info--insert-goal-text (text delimiter) (lean4-info--insert-highlight-inaccessible-names (lsp--fontlock-with-mode text 'lean4-info-mode) delimiter)) @@ -158,20 +158,20 @@ The buffer is supposed to be the *Lean Goal* buffer." (progn (erase-buffer) (magit-insert-section (magit-section 'root) - (when-let ((goals lean4-goals)) ;; capture for deferred rendering + (when-let ((goals lean4-info-goals)) ;; capture for deferred rendering (magit-insert-section (magit-section 'goals) (magit-insert-heading "Goals:") (magit-insert-section-body (if (> (length goals) 0) (seq-doseq (g goals) (magit-insert-section (magit-section) - (lean4--insert-goal-text g "\n\n"))) + (lean4-info--insert-goal-text g "\n\n"))) (insert "goals accomplished\n\n"))))) - (when-let ((term-goal lean4-term-goal)) ;; capture for deferred rendering + (when-let ((term-goal lean4-info-term-goal)) ;; capture for deferred rendering (magit-insert-section (magit-section 'term-goal) (magit-insert-heading "Expected type:") (magit-insert-section-body - (lean4--insert-goal-text term-goal "\n")))) + (lean4-info--insert-goal-text term-goal "\n")))) (lean4-info--mk-message-section 'errors-here "Messages here:" errors-here buffer) (lean4-info--mk-message-section 'errors-below "Messages below:" errors-below buffer) (lean4-info--mk-message-section 'errors-above "Messages above:" errors-above buffer))))))) @@ -298,7 +298,7 @@ sections." "$/lean/plainGoal" (lsp--text-document-position-params) (-lambda ((ignored &as &lean:PlainGoal? :goals)) - (setq lean4-goals goals) + (setq lean4-info-goals goals) (lean4-info-buffer-redisplay-debounced)) :error-handler #'ignore :mode 'tick @@ -307,7 +307,7 @@ sections." "$/lean/plainTermGoal" (lsp--text-document-position-params) (-lambda ((ignored &as &lean:PlainTermGoal? :goal)) - (setq lean4-term-goal goal) + (setq lean4-info-term-goal goal) (lean4-info-buffer-redisplay-debounced)) :error-handler #'ignore :mode 'tick @@ -316,10 +316,10 @@ sections." ;(lean4-info-buffer-redisplay) )) -(defun lean4-toggle-info () +(defun lean4-info-toggle () "Show infos at the current point." (interactive) - (lean4-toggle-info-buffer lean4-info-buffer-name) + (lean4-info-toggle-buffer lean4-info-buffer-name) (lean4-info-buffer-refresh)) (provide 'lean4-info) diff --git a/lean4-mode.el b/lean4-mode.el index 96d9e47..08baa8e 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -106,7 +106,7 @@ "C-c C-l" #'lean4-execute "C-c C-k" #'quail-show-key "TAB" #'lean4-eri-tab - "C-c C-i" #'lean4-toggle-info + "C-c C-i" #'lean4-info-toggle "C-c C-p C-l" #'lean4-lake-build "C-c C-d" #'lean4-lsp-document-reopen) @@ -114,7 +114,7 @@ "Menu for the Lean major mode." `("Lean 4" ["Execute lean" lean4-execute t] - ["Toggle info display" lean4-toggle-info t] + ["Toggle info display" lean4-info-toggle t] ["Restart lean process" lsp-workspace-restart t] ["Customize lean4-mode" (customize-group 'lean) t])) diff --git a/lean4-mode.info b/lean4-mode.info index 12638ca..c3c9e97 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -232,7 +232,7 @@ ask you to identify the _project_ this file belongs to. If you then type ‘#check id’, the word ‘#check’ will be underlined, and hovering over it will show you the type of ‘id’. - To view the proof state, run ‘lean4-toggle-info’ (‘C-c C-i’). This + To view the proof state, run ‘lean4-info-toggle’ (‘C-c C-i’). This will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. @@ -242,7 +242,7 @@ Key Description ‘C-c C-d’ Recompile and reload imports ‘lean4-lsp-document-reopen’ ‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ -‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-toggle-info-buffer’ +‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-info-toggle-buffer’ * Menu: diff --git a/lean4-mode.texi b/lean4-mode.texi index 4c524fb..c2fcf36 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -236,7 +236,7 @@ will ask you to identify the @emph{project} this file belongs to. If you then type @samp{#check id}, the word @samp{#check} will be underlined, and hovering over it will show you the type of @code{id}. -To view the proof state, run @code{lean4-toggle-info} (@samp{C-c C-i}). This +To view the proof state, run @code{lean4-info-toggle} (@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. @@ -258,7 +258,7 @@ in VS-Code) in a separate window. @tab @code{lean4-lake-build} @item @samp{C-c C-i} @tab Toggle Info-View which shows goals and errors at point -@tab @code{lean4-toggle-info-buffer} +@tab @code{lean4-info-toggle-buffer} @end multitable @menu From 092fdd7889cf783847c6c4090d5d7a472ffc272f Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:12:34 +0200 Subject: [PATCH 24/50] [info] Rename lean4-info-mode and correct docstring and comments --- lean4-info.el | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 4af37ea..8809e56 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -39,11 +39,9 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." :group 'lean4-info :type 'boolean) -;; Lean Info Mode (for "*lean4-info*" buffer) -;; Automode List ;;;###autoload -(define-derived-mode lean4-info-mode prog-mode "Lean-Info" - "Major mode for Lean4-Mode Info Buffer." +(define-derived-mode lean4-info-mockup-mode prog-mode "Lean-Info" + "Major mode used internally to syntax highlight Lean4." :syntax-table lean4-syntax-table :group 'lean4 (set (make-local-variable 'font-lock-defaults) lean4-info-font-lock-defaults) @@ -122,7 +120,7 @@ The buffer is supposed to be the *Lean Goal* buffer." (defun lean4-info--insert-goal-text (text delimiter) (lean4-info--insert-highlight-inaccessible-names - (lsp--fontlock-with-mode text 'lean4-info-mode) + (lsp--fontlock-with-mode text 'lean4-info-mockup-mode) delimiter)) (defun lean4-info--mk-message-section (value caption messages buffer) From b9205d76ed00185ab85e24360041c426cf6ff6b9 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:12:56 +0200 Subject: [PATCH 25/50] [info] Define minor mode lean4-info-mode - Delete lean4-info-toggle. - In lean4-mode-map, bind C-c C-i to lean4-info-mode instead. - Adapt readme and manuals. - Move lean4-hooks-alist from lean4-mode.el to lean4-info-hookings and deal with it in lean4-info-mode. --- README.org | 4 ++-- lean4-info.el | 48 +++++++++++++++++++++++++++++++++++------------- lean4-mode.el | 23 ++--------------------- lean4-mode.info | 30 +++++++++++++++--------------- lean4-mode.texi | 4 ++-- 5 files changed, 56 insertions(+), 53 deletions(-) diff --git a/README.org b/README.org index 711d2fd..7abb675 100644 --- a/README.org +++ b/README.org @@ -146,7 +146,7 @@ will ask you to identify the /project/ this file belongs to. If you then type =#check id=, the word =#check= will be underlined, and hovering over it will show you the type of ~id~. -To view the proof state, run ~lean4-info-toggle~ (=C-c C-i=). This +To view the proof state, run ~lean4-info-mode~ (=C-c C-i=). This will display the =*Lean Goals*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. @@ -156,7 +156,7 @@ in VS-Code) in a separate window. | =C-c C-d= | Recompile and reload imports | ~lean4-lsp-document-reopen~ | | =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-execute~ | | =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | -| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-info-toggle-buffer~ | +| =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-info-mode~ | ** lsp-mode diff --git a/lean4-info.el b/lean4-info.el index 8809e56..0683dc0 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -60,14 +60,6 @@ Also choose settings used for the *Lean Goal* buffer." (set-syntax-table lean4-syntax-table) (setq buffer-read-only t)))) -(defun lean4-info-toggle-buffer (buffer) - "Create or delete BUFFER. -The buffer is supposed to be the *Lean Goal* buffer." - (-if-let (window (get-buffer-window buffer)) - (quit-window nil window) - (lean4-info-ensure-buffer buffer) - (display-buffer buffer))) - (defun lean4-info-buffer-active (buffer) "Check whether given info BUFFER should show info for current buffer." (and @@ -314,11 +306,41 @@ sections." ;(lean4-info-buffer-redisplay) )) -(defun lean4-info-toggle () - "Show infos at the current point." - (interactive) - (lean4-info-toggle-buffer lean4-info-buffer-name) - (lean4-info-buffer-refresh)) +(defcustom lean4-info-hookings + (list + (cons 'flycheck-after-syntax-check-hook + #'lean4-info-buffer-redisplay-debounced) + (cons 'post-command-hook + #'lean4-info-buffer-redisplay-debounced) + (cons 'lsp-on-idle-hook + #'lean4-info-buffer-refresh)) + "Pairs of hooks and functions to be toggled by `lean4-info-mode'. + +The value should be an alist associating hook variables with functions. +When `lean4-info-mode' is turned on, the function will be added +buffer-locally to the hook. When turned off, it'll be removed +buffer-locally." + :type '(repeat (cons variable function)) + :group 'lean4-info) + +(define-minor-mode lean4-info-mode + "Minor mode for `lean4-mode' to keep Lean4 Info buffer updated." + :lighter "ⓘ" + (if lean4-info-mode + (progn + (lean4-info-ensure-buffer lean4-info-buffer-name) + (display-buffer lean4-info-buffer-name) + (lean4-info-buffer-refresh) + (mapc (lambda (hooking) + (when (boundp (car hooking)) + (add-hook (car hooking) (cdr hooking) nil 'local))) + lean4-info-hookings)) + (when-let* ((window (get-buffer-window lean4-info-buffer-name))) + (quit-window nil window) + (mapc (lambda (hooking) + (when (boundp (car hooking)) + (remove-hook (car hooking) (cdr hooking) 'local))) + lean4-info-hookings)))) (provide 'lean4-info) ;;; lean4-info.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 08baa8e..048c52a 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -56,11 +56,6 @@ ;; 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) -(declare-function flycheck-list-errors "ext:flycheck") -(declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc") (declare-function quail-show-key "quail") (defgroup lean4 nil @@ -106,7 +101,7 @@ "C-c C-l" #'lean4-execute "C-c C-k" #'quail-show-key "TAB" #'lean4-eri-tab - "C-c C-i" #'lean4-info-toggle + "C-c C-i" #'lean4-info-mode "C-c C-p C-l" #'lean4-lake-build "C-c C-d" #'lean4-lsp-document-reopen) @@ -114,22 +109,10 @@ "Menu for the Lean major mode." `("Lean 4" ["Execute lean" lean4-execute t] - ["Toggle info display" lean4-info-toggle t] + ["Toggle info display" lean4-info-mode t] ["Restart lean process" lsp-workspace-restart t] ["Customize lean4-mode" (customize-group 'lean) t])) -(defconst lean4-hooks-alist - '(;; info view - ;; update errors immediately, but delay querying goal - (flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay-debounced) - (post-command-hook . lean4-info-buffer-redisplay-debounced) - (lsp-on-idle-hook . lean4-info-buffer-refresh)) - "Hooks which lean4-mode needs to hook in. - -The `car' of each pair is a hook variable, the `cdr' a function -to be added or removed from the hook variable if Flycheck mode is -enabled and disabled respectively.") - (defun lean4-mode-setup () "Default lean4-mode setup." ;; Right click menu sources @@ -162,8 +145,6 @@ enabled and disabled respectively.") 'common-lisp-indent-function) (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1)) - (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist) - (add-hook hook fn nil 'local)) (lean4-mode-setup)) ;; Automatically use lean4-mode for .lean files. diff --git a/lean4-mode.info b/lean4-mode.info index c3c9e97..1af75e4 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -232,7 +232,7 @@ ask you to identify the _project_ this file belongs to. If you then type ‘#check id’, the word ‘#check’ will be underlined, and hovering over it will show you the type of ‘id’. - To view the proof state, run ‘lean4-info-toggle’ (‘C-c C-i’). This + To view the proof state, run ‘lean4-info-mode’ (‘C-c C-i’). This will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. @@ -242,7 +242,7 @@ Key Description ‘C-c C-d’ Recompile and reload imports ‘lean4-lsp-document-reopen’ ‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ -‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-info-toggle-buffer’ +‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-info-mode’ * Menu: @@ -447,19 +447,19 @@ Node: Native vc (Emacs 30 or later)5416 Node: Doom-Emacs6324 Node: Straight6750 Node: Usage7250 -Node: lsp-mode8684 -Node: Flycheck8969 -Node: Configuration9579 -Node: lsp-mode (1)9769 -Node: Flycheck (1)10038 -Node: Common Pitfalls10523 -Node: Changelog11115 -Node: Upcoming Version11555 -Node: Version 112 from 2024-12-1013621 -Node: Version 111 from 2024-12-0214486 -Node: Version 110 from 2024-12-0114893 -Node: Version 101 from 2024-11-2115391 -Node: Version 10 from 2024-11-1615754 +Node: lsp-mode8673 +Node: Flycheck8958 +Node: Configuration9568 +Node: lsp-mode (1)9758 +Node: Flycheck (1)10027 +Node: Common Pitfalls10512 +Node: Changelog11104 +Node: Upcoming Version11544 +Node: Version 112 from 2024-12-1013610 +Node: Version 111 from 2024-12-0214475 +Node: Version 110 from 2024-12-0114882 +Node: Version 101 from 2024-11-2115380 +Node: Version 10 from 2024-11-1615743  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index c2fcf36..a7cd1a3 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -236,7 +236,7 @@ will ask you to identify the @emph{project} this file belongs to. If you then type @samp{#check id}, the word @samp{#check} will be underlined, and hovering over it will show you the type of @code{id}. -To view the proof state, run @code{lean4-info-toggle} (@samp{C-c C-i}). This +To view the proof state, run @code{lean4-info-mode} (@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. @@ -258,7 +258,7 @@ in VS-Code) in a separate window. @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-info-toggle-buffer} +@tab @code{lean4-info-mode} @end multitable @menu From 0f2be72e1edb4c8efd1fcef14e2810cc58fbaea8 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:00 +0200 Subject: [PATCH 26/50] [mode] Move lsp-mode specifics to new minor lean4-lsp-mode in [lsp] --- lean4-lsp.el | 24 ++++++++++++++++++++++++ lean4-mode.el | 14 ++++---------- 2 files changed, 28 insertions(+), 10 deletions(-) diff --git a/lean4-lsp.el b/lean4-lsp.el index df24742..62590ec 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -22,6 +22,8 @@ ;;; Code: +(require 'compat) ;; for `defvar-keymap' + (require 'lsp-mode) (defun lean4-lsp-document-reopen () @@ -59,6 +61,28 @@ of the parent project." (when root (lsp-workspace-folders-add root)))) +(defun lean4-lsp-semantic-tokens-enable () + "Buffer-locally set `lsp-semantic-tokens-enable' to t." + (interactive) + (setq-local lsp-semantic-tokens-enable t)) + +(defcustom lean4-lsp-mode-hook + (list #'lsp + #'lean4-lsp-semantic-tokens-enable + #'lean4-lsp-workspace-add) + "Hook run by `lean4-lsp-mode'." + :options '( lsp + lean4-lsp-semantic-tokens-enable + lean4-lsp-workspace-add) + :type 'hook + :group 'lean4-lsp) + +(defvar-keymap lean4-lsp-mode-map + "C-c C-d" #'lean4-lsp-document-reopen) + +(define-minor-mode lean4-lsp-mode + "Minor mode for `lean4-mode' for using `lsp-mode' as LSP client.") + ;;;; Registration (add-to-list 'lsp-language-id-configuration diff --git a/lean4-mode.el b/lean4-mode.el index 048c52a..885c072 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -44,7 +44,6 @@ (require 'cl-lib) (require 'dash) (require 'pcase) -(require 'lsp-mode) (require 'lean4-eri) (require 'lean4-syntax) (require 'lean4-info) @@ -68,9 +67,9 @@ :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") :prefix "lean4-") -(defcustom lean4-mode-hook (list #'lsp) +(defcustom lean4-mode-hook (list #'lean4-lsp-mode) "Hook run after entering `lean4-mode'." - :options '(flycheck-mode lsp) + :options '(flycheck-mode lean4-lsp-mode) :type 'hook :group 'lean4) @@ -102,15 +101,13 @@ "C-c C-k" #'quail-show-key "TAB" #'lean4-eri-tab "C-c C-i" #'lean4-info-mode - "C-c C-p C-l" #'lean4-lake-build - "C-c C-d" #'lean4-lsp-document-reopen) + "C-c C-p C-l" #'lean4-lake-build) (easy-menu-define lean4-mode-menu lean4-mode-map "Menu for the Lean major mode." `("Lean 4" ["Execute lean" lean4-execute t] ["Toggle info display" lean4-info-mode t] - ["Restart lean process" lsp-workspace-restart t] ["Customize lean4-mode" (customize-group 'lean) t])) (defun lean4-mode-setup () @@ -119,10 +116,7 @@ ;;(setq lean4-right-click-item-functions '(lean4-info-right-click-find-definition ;; lean4-hole-right-click)) ;; Flycheck - (setq-local flycheck-disabled-checkers '()) - ;; Lean massively benefits from semantic tokens, so change default to enabled - (setq-local lsp-semantic-tokens-enable t) - (lean4-lsp-workspace-add)) + (setq-local flycheck-disabled-checkers '())) ;;;###autoload (define-derived-mode lean4-mode prog-mode "Lean 4" From e5852dedbaae49fa8b60a6190ade45cd91b6c4a6 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:03 +0200 Subject: [PATCH 27/50] [mode] Delete lean4-mode-setup function The lean4-mode-setup function was almost empty. The only thing it was doing is to set flycheck-disabled-checkers to nil buffer-locally. But after testing, this setting is the default / initial value already and thus not needed. --- lean4-mode.el | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index 885c072..fa7a908 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -110,14 +110,6 @@ ["Toggle info display" lean4-info-mode t] ["Customize lean4-mode" (customize-group 'lean) t])) -(defun lean4-mode-setup () - "Default lean4-mode setup." - ;; Right click menu sources - ;;(setq lean4-right-click-item-functions '(lean4-info-right-click-find-definition - ;; lean4-hole-right-click)) - ;; Flycheck - (setq-local flycheck-disabled-checkers '())) - ;;;###autoload (define-derived-mode lean4-mode prog-mode "Lean 4" "Major mode for Lean language. @@ -138,8 +130,7 @@ (set (make-local-variable 'lisp-indent-function) 'common-lisp-indent-function) (if (fboundp 'electric-indent-local-mode) - (electric-indent-local-mode -1)) - (lean4-mode-setup)) + (electric-indent-local-mode -1))) ;; Automatically use lean4-mode for .lean files. ;;;###autoload From 0b5bb7ed4bffd70b743141cb64e1d5423658a381 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:06 +0200 Subject: [PATCH 28/50] [mode] Use setq-local --- lean4-mode.el | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index fa7a908..dfdba4b 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -117,18 +117,17 @@ \\{lean4-mode-map}" :syntax-table lean4-syntax-table :group 'lean4 - (set (make-local-variable 'comment-start) "--") - (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*") - (set (make-local-variable 'comment-end) "") - (set (make-local-variable 'comment-end-skip) "[ \t]*\\(-/\\|\\s>\\)") - (set (make-local-variable 'comment-padding) 1) - (set (make-local-variable 'comment-use-syntax) t) - (set (make-local-variable 'font-lock-defaults) lean4-font-lock-defaults) - (set (make-local-variable 'indent-tabs-mode) nil) - (set 'compilation-mode-font-lock-keywords '()) + (setq-local comment-end "") + (setq-local comment-end-skip "[ \t]*\\(-/\\|\\s>\\)") + (setq-local comment-padding 1) + (setq-local comment-start "--") + (setq-local comment-start-skip "[-/]-[ \t]*") + (setq-local comment-use-syntax t) + (setq-local font-lock-defaults lean4-font-lock-defaults) + (setq-local indent-tabs-mode nil) + (setq-local lisp-indent-function 'common-lisp-indent-function) + (set 'compilation-mode-font-lock-keywords nil) (lean4-input-set) - (set (make-local-variable 'lisp-indent-function) - 'common-lisp-indent-function) (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1))) From 54e0e2ae38761d51cb8b198ce6f95105910cb9c6 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:10 +0200 Subject: [PATCH 29/50] [mode] Don't set compilation-mode-font-lock-keywords to nil globally Even if compilation-mode-font-lock-keywords should be nil when `compile` is called from Lean4-Mode due to the way Lake's or Lean's build log looks, this doesn't justify globally setting compilation-mode-font-lock-keywords to nil because this screws up `compile` for the Emacs session permanently. --- lean4-mode.el | 1 - 1 file changed, 1 deletion(-) diff --git a/lean4-mode.el b/lean4-mode.el index dfdba4b..8df0f00 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -126,7 +126,6 @@ (setq-local font-lock-defaults lean4-font-lock-defaults) (setq-local indent-tabs-mode nil) (setq-local lisp-indent-function 'common-lisp-indent-function) - (set 'compilation-mode-font-lock-keywords nil) (lean4-input-set) (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1))) From cf7bb7664289f44ed26ce648c369f44f86c6e78d Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:13 +0200 Subject: [PATCH 30/50] [mode] Move lean4-input-set to lean4-mode-hook as default member --- lean4-mode.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lean4-mode.el b/lean4-mode.el index 8df0f00..285c3a4 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -67,9 +67,9 @@ :link '(emacs-library-link :tag "Library Source" "lean4-mode.el") :prefix "lean4-") -(defcustom lean4-mode-hook (list #'lean4-lsp-mode) +(defcustom lean4-mode-hook (list #'lean4-input-set #'lean4-lsp-mode) "Hook run after entering `lean4-mode'." - :options '(flycheck-mode lean4-lsp-mode) + :options '(flycheck-mode lean4-input-set lean4-lsp-mode) :type 'hook :group 'lean4) From 016bbc1be7b2bb798c935b74910d7b27ee6f42e1 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:16 +0200 Subject: [PATCH 31/50] [info] Remove local settings in lean4-info-mockup-mode --- lean4-info.el | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 0683dc0..e934b9a 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -44,11 +44,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." "Major mode used internally to syntax highlight Lean4." :syntax-table lean4-syntax-table :group 'lean4 - (set (make-local-variable 'font-lock-defaults) lean4-info-font-lock-defaults) - (set (make-local-variable 'indent-tabs-mode) nil) - (set 'compilation-mode-font-lock-keywords '()) - (set (make-local-variable 'lisp-indent-function) - 'common-lisp-indent-function)) + (setq-local font-lock-defaults lean4-info-font-lock-defaults)) (defun lean4-info-ensure-buffer (buffer) "Create BUFFER if it does not exist. From 70a06693415033d681e83aa95524365522f83836 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:20 +0200 Subject: [PATCH 32/50] [mode] Fix autoload cookie --- lean4-mode.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-mode.el b/lean4-mode.el index 285c3a4..9581d67 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -136,7 +136,7 @@ '("\\.lean\\'" . lean4-mode)) ;; Use utf-8 encoding -;;;### autoload +;;;###autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) (provide 'lean4-mode) From 34650996027d4eebf72a1cb79b6d3c11d67db842 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:23 +0200 Subject: [PATCH 33/50] Use same prop-line style everywhere --- lean4-eri.el | 2 +- lean4-fringe.el | 2 +- lean4-info.el | 2 +- lean4-input.el | 2 +- lean4-markdown.el | 2 +- lean4-mode.el | 2 +- lean4-syntax.el | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lean4-eri.el b/lean4-eri.el index d1f1c1d..b444092 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -1,4 +1,4 @@ -;;; lean4-eri.el --- Lean4-Mode Indentation -*- lexical-binding: t; -*- +;;; lean4-eri.el --- Lean4 indentation -*- lexical-binding: t; -*- ;; Copyright (c) 2005-2010 Ulf Norell, Nils Anders Danielsson, ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, diff --git a/lean4-fringe.el b/lean4-fringe.el index 3ab6807..35c61e3 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -1,4 +1,4 @@ -;;; lean4-fringe.el --- Lean4-Mode Processing Progress in Fringe -*- lexical-binding: t; -*- +;;; lean4-fringe.el --- Lean4 fringe progress -*- lexical-binding: t; -*- ;; Copyright (c) 2016 Microsoft Corporation. All rights reserved. diff --git a/lean4-info.el b/lean4-info.el index e934b9a..c3bc9e4 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -1,4 +1,4 @@ -;;; lean4-info.el --- Lean4-Mode Info View -*- lexical-binding: t; -*- +;;; lean4-info.el --- Lean4 info -*- lexical-binding: t; -*- ;; Copyright (c) 2016 Gabriel Ebner. All rights reserved. diff --git a/lean4-input.el b/lean4-input.el index 6760add..9877c64 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -1,4 +1,4 @@ -;;; lean4-input.el --- Lean4-Mode Input Method -*- lexical-binding: t; -*- +;;; lean4-input.el --- Lean4 input -*- lexical-binding: t; -*- ;; Copyright (c) 2005-2012 Ulf Norell, Nils Anders Danielsson, ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, diff --git a/lean4-markdown.el b/lean4-markdown.el index df2ef9d..534dacc 100644 --- a/lean4-markdown.el +++ b/lean4-markdown.el @@ -1,4 +1,4 @@ -;;; lean4-markdown.el --- Lean4 Markdown Integration -*- lexical-binding: t; -*- +;;; lean4-markdown.el --- Lean4 markdown -*- lexical-binding: t; -*- ;; Copyright (c) 2025 Mekeor Melire diff --git a/lean4-mode.el b/lean4-mode.el index 9581d67..5787b8a 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -1,4 +1,4 @@ -;;; lean4-mode.el --- Major mode for Lean language -*- lexical-binding: t; -*- +;;; lean4-mode.el --- Lean4 major mode -*- lexical-binding: t; -*- ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. ;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved. diff --git a/lean4-syntax.el b/lean4-syntax.el index 26b7fd1..e6dc1ca 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -1,4 +1,4 @@ -;;; lean4-syntax.el --- Lean4-Mode Syntax Definitions -*- lexical-binding: t; -*- +;;; lean4-syntax.el --- Lean4 syntax -*- lexical-binding: t; -*- ;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. From 4ce2b3a519964093ed946626caabed5b78d0b687 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:47 +0200 Subject: [PATCH 34/50] Use Lean4 naming everywhere --- README.org | 10 ++++----- lean4-eri.el | 2 +- lean4-fringe.el | 8 +++---- lean4-info.el | 12 +++++----- lean4-input.el | 23 +++++++++---------- lean4-lsp.el | 3 ++- lean4-markdown.el | 2 +- lean4-mode.el | 21 +++++++++--------- lean4-mode.info | 56 +++++++++++++++++++++++------------------------ lean4-mode.texi | 14 ++++++------ lean4-syntax.el | 14 +++++++----- 11 files changed, 84 insertions(+), 81 deletions(-) diff --git a/README.org b/README.org index 7abb675..fd8a57b 100644 --- a/README.org +++ b/README.org @@ -1,9 +1,9 @@ -#+title: Lean4-Mode - Emacs major mode for Lean language +#+title: Emacs Lean4-Mode #+language: en #+export_file_name: lean4-mode.texi #+texinfo_dir_category: Emacs misc features #+texinfo_dir_title: Lean4-Mode: (lean4-mode). -#+texinfo_dir_desc: Emacs major mode for Lean language +#+texinfo_dir_desc: Emacs major mode for Lean4 language This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing code written in version 4 of the programming language and theorem @@ -140,21 +140,21 @@ place the following code in your Emacs initialization file: * Usage -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with =.lean= extension. Emacs will ask you to identify the /project/ this file belongs to. If you then type =#check id=, the word =#check= will be underlined, and hovering over it will show you the type of ~id~. To view the proof state, run ~lean4-info-mode~ (=C-c C-i=). This -will display the =*Lean Goals*= buffer (like the Lean Info-View pane +will display the =*Lean4 Goals*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. | Key | Description | Command | |------------------------+--------------------------------------------------------+-----------------------------| | =C-c C-k= | Echo the keystroke needed to input the symbol at point | ~quail-show-key~ | | =C-c C-d= | Recompile and reload imports | ~lean4-lsp-document-reopen~ | -| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode | ~lean4-execute~ | +| =C-c C-x= or =C-c C-l= | Execute Lean4 in stand-alone mode | ~lean4-execute~ | | =C-c C-p C-l= | Builds package with lake | ~lean4-lake-build~ | | =C-c C-i= | Toggle Info-View which shows goals and errors at point | ~lean4-info-mode~ | diff --git a/lean4-eri.el b/lean4-eri.el index b444092..35dcff4 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -224,7 +224,7 @@ are calculated." (lean4-eri-indent t)) (defun lean4-eri-tab () - "Lean 4 function for TAB indent." + "Lean4 function for TAB indent." (interactive) (cond ((looking-back (rx line-start (* white)) nil) (lean4-eri-indent)) diff --git a/lean4-fringe.el b/lean4-fringe.el index 35c61e3..3a9fcb0 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -18,7 +18,7 @@ ;;; Commentary: -;; Show Lean processing progress in the editor fringe +;; Show Lean4 processing progress in the editor fringe ;;; Code: @@ -42,7 +42,7 @@ (defface lean4-fringe-face nil - "Face to highlight Lean file progress." + "Face to highlight Lean4 file progress." :group 'lean4) (if (fboundp 'define-fringe-bitmap) @@ -55,7 +55,7 @@ (((class color) (background dark)) :background "navajo white") (t :inverse-video t)) - "Face to highlight the fringe of Lean file processing progress." + "Face to highlight the fringe of Lean4 file processing progress." :group 'lean4) (defface lean4-fringe-fringe-fatal-error-face @@ -64,7 +64,7 @@ (((class color) (background dark)) :background "red") (t :inverse-video t)) - "Face to highlight the fringe of Lean file fatal errors." + "Face to highlight the fringe of Lean4 file fatal errors." :group 'lean4) (lsp-defun lean4-fringe-fringe-face ((&lean:LeanFileProgressProcessingInfo :kind)) diff --git a/lean4-info.el b/lean4-info.el index c3bc9e4..d92d583 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -35,12 +35,12 @@ (defcustom lean4-info-highlight-inaccessibles t "Use font to highlight inaccessible names. Set this variable to t to highlight inaccessible names in the info display -using `font-lock-comment-face' instead of the `✝` suffix used by Lean." +using `font-lock-comment-face' instead of the `✝` suffix used by Lean4." :group 'lean4-info :type 'boolean) ;;;###autoload -(define-derived-mode lean4-info-mockup-mode prog-mode "Lean-Info" +(define-derived-mode lean4-info-mockup-mode prog-mode "Lean4-Info" "Major mode used internally to syntax highlight Lean4." :syntax-table lean4-syntax-table :group 'lean4 @@ -48,7 +48,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean." (defun lean4-info-ensure-buffer (buffer) "Create BUFFER if it does not exist. -Also choose settings used for the *Lean Goal* buffer." +Also choose settings used for the *Lean4 Goal* buffer." (unless (get-buffer buffer) (with-current-buffer (get-buffer-create buffer) (buffer-disable-undo) @@ -72,7 +72,7 @@ Also choose settings used for the *Lean Goal* buffer." (:range :fullRange :message) (:code :relatedInformation :severity :source :tags)))) -(defconst lean4-info-buffer-name "*Lean Goal*") +(defconst lean4-info-buffer-name "*Lean4 Goal*") (defvar lean4-info-goals nil) (defvar lean4-info-term-goal nil) @@ -219,7 +219,7 @@ Also choose settings used for the *Lean Goal* buffer." (defcustom lean4-info-buffer-debounce-delay-sec 0.1 - "Duration of time we wait before writing to *Lean Goal*." + "Duration of time we wait before writing to *Lean4 Goal*." :group 'lean4-info :type 'number) @@ -278,7 +278,7 @@ sections." (defun lean4-info-buffer-refresh () - "Refresh the *Lean Goal* buffer." + "Refresh the *Lean4 Goal* buffer." (when (lean4-info-buffer-active lean4-info-buffer-name) (lsp-request-async "$/lean/plainGoal" diff --git a/lean4-input.el b/lean4-input.el index 9877c64..a0a3be8 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -22,7 +22,7 @@ ;; A highly customisable input method which can inherit from other ;; Quail input methods. By default the input method is geared towards -;; the input of mathematical and other symbols in Lean programs. +;; the input of mathematical and other symbols in Lean4 programs. ;; Use M-x customize-group lean4-input to customise this input method. ;; Note that the functions defined under "Functions used to tweak @@ -145,7 +145,7 @@ This suffix is dropped." ;; until lean4-input-setup is called at the end of this file. (defgroup lean4-input nil - "The Lean input method. + "The Lean4 input method. After tweaking these settings you may want to inspect the resulting translations using `lean4-input-show-translations'." :group 'lean4 @@ -162,7 +162,7 @@ translations using `lean4-input-show-translations'." (lean4-input-prefix "^")) (lean4-input-prefix "_")))))) "List of parent Quail input methods. -Translations from these methods will be inherited by the Lean +Translations from these methods will be inherited by the Lean4 input method (with the exception of translations corresponding to ASCII characters). @@ -189,7 +189,7 @@ order for the change to take effect." :type 'directory) (defcustom lean4-input-user-translations nil - "A list of translations specific to the Lean input method. + "A list of translations specific to the Lean4 input method. Each element is a pair (KEY-SEQUENCE-STRING . LIST-OF-TRANSLATION-STRINGS). All the translation strings are possible translations of the given key sequence; if there is more than one you can choose @@ -230,7 +230,7 @@ that contains all translations from QP Except for those corresponding to ASCII." (cons 'decode-map (lean4-input-get-translations qp))))))) (defun lean4-input-add-translations (trans) - "Add the given translations TRANS to the Lean input method. + "Add the given translations TRANS to the Lean4 input method. TRANS is a list of pairs (KEY-SEQUENCE . TRANSLATION). The translations are appended to the current translations." (with-temp-buffer @@ -244,7 +244,7 @@ translations are appended to the current translations." (defun lean4-input-inherit-package (qp &optional fun) "Inherit translations from the Quail package QP. Add all translations from the Quail package QP (except for those -corresponding to ASCII) to the list of Lean Quail rules. +corresponding to ASCII) to the list of Lean4 Quail rules. The optional function FUN can be used to modify the translations. It is given a pair (KEY-SEQUENCE . TRANSLATION) and should return @@ -261,14 +261,15 @@ a list of such pairs." (declare-function json-read "json") (defun lean4-input-setup () - "Set up the Lean input method. -Use customisable variables and parent input methods to setup Lean input method." + "Set up the Lean4 input method. +Use customisable variables and parent input methods to setup Lean4 input +method." ;; Create (or reset) the input method. (with-temp-buffer (quail-define-package "Lean" "UTF-8" "∏" t ; guidance - "Lean input method. -The purpose of this input method is to edit Lean programs, but + "Lean4 input method. +The purpose of this input method is to edit Lean4 programs, but since it is highly customisable it can be made useful for other tasks as well." nil nil nil nil nil nil t ; maximum-shortest @@ -296,7 +297,7 @@ tasks as well." (eval (cdr def))))) (defun lean4-input-incorporate-changed-setting (sym val) - "Update the Lean input method. + "Update the Lean4 input method. Set SYM default value to VAL, then call `lean4-input-setup'. Suitable for use in the :set field of `defcustom'." (set-default sym val) diff --git a/lean4-lsp.el b/lean4-lsp.el index 62590ec..1faa188 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -86,11 +86,12 @@ of the parent project." ;;;; Registration (add-to-list 'lsp-language-id-configuration - '(lean4-mode . "lean")) + '(lean4-mode . "lean4")) (lsp-register-client (make-lsp-client :new-connection (lsp-stdio-connection '("lake" "serve")) :major-modes '(lean4-mode) + :language-id "lean4" :server-id 'lean4-lsp :notification-handlers (ht ("$/lean/fileProgress" #'lean4-fringe-update)) :semantic-tokens-faces-overrides '(:types (("leanSorryLike" . font-lock-warning-face))))) diff --git a/lean4-markdown.el b/lean4-markdown.el index 534dacc..ca68daa 100644 --- a/lean4-markdown.el +++ b/lean4-markdown.el @@ -25,7 +25,7 @@ (require 'markdown-mode) (add-to-list 'markdown-code-lang-modes - '("lean" . lean4-mode)) + '("lean4" . lean4-mode)) (provide 'lean4-markdown) ;;; lean4-markdown.el ends here diff --git a/lean4-mode.el b/lean4-mode.el index 5787b8a..73896da 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -31,10 +31,10 @@ ;;; Commentary: -;; Provides a major mode for the Lean programming language. +;; Provides a major mode for the Lean4 programming language. ;; Provides highlighting, diagnostics, goal visualization, -;; and many other useful features for Lean users. +;; and many other useful features for Lean4 users. ;; See the README.md for more advanced features and the ;; associated keybindings. @@ -79,7 +79,7 @@ :group 'lean4) (defun lean4-execute () - "Execute Lean in the current buffer." + "Execute Lean4 in the current buffer." (interactive) (let* ((default-directory (or lean4-location-root default-directory))) @@ -104,15 +104,15 @@ "C-c C-p C-l" #'lean4-lake-build) (easy-menu-define lean4-mode-menu lean4-mode-map - "Menu for the Lean major mode." - `("Lean 4" - ["Execute lean" lean4-execute t] - ["Toggle info display" lean4-info-mode t] - ["Customize lean4-mode" (customize-group 'lean) t])) + "Menu for the Lean4 major mode." + `("Lean4" + ["Execute Lean4" lean4-execute t] + ["Toggle Info" lean4-info-mode t] + ["Customize" (customize-group 'lean) t])) ;;;###autoload -(define-derived-mode lean4-mode prog-mode "Lean 4" - "Major mode for Lean language. +(define-derived-mode lean4-mode prog-mode "Lean4" + "Major mode for Lean4 language. \\{lean4-mode-map}" :syntax-table lean4-syntax-table @@ -130,7 +130,6 @@ (if (fboundp 'electric-indent-local-mode) (electric-indent-local-mode -1))) -;; Automatically use lean4-mode for .lean files. ;;;###autoload (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) diff --git a/lean4-mode.info b/lean4-mode.info index 1af75e4..3188ae7 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -3,14 +3,14 @@ lean4-mode.texi. INFO-DIR-SECTION Emacs misc features START-INFO-DIR-ENTRY -* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language. +* Lean4-Mode: (lean4-mode). Emacs major mode for Lean4 language. END-INFO-DIR-ENTRY  File: lean4-mode.info, Node: Top, Next: Installation, Up: (dir) -Lean4-Mode - Emacs major mode for Lean language -*********************************************** +Emacs Lean4-Mode +**************** This package extends GNU Emacs (https://www.gnu.org/software/emacs/) by providing a major mode for editing code written in version 4 of the @@ -226,21 +226,21 @@ File: lean4-mode.info, Node: Usage, Next: Configuration, Prev: Installation, 2 Usage ******* -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with ‘.lean’ extension. Emacs will ask you to identify the _project_ this file belongs to. If you then type ‘#check id’, the word ‘#check’ will be underlined, and hovering over it will show you the type of ‘id’. To view the proof state, run ‘lean4-info-mode’ (‘C-c C-i’). This -will display the ‘*Lean Goals*’ buffer (like the Lean Info-View pane in +will display the ‘*Lean4 Goals*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. Key Description Command ---------------------------------------------------------------------------------------------------------------- ‘C-c C-k’ Echo the keystroke needed to input the symbol at point ‘quail-show-key’ ‘C-c C-d’ Recompile and reload imports ‘lean4-lsp-document-reopen’ -‘C-c C-x’ or ‘C-c C-l’ Execute Lean in stand-alone mode ‘lean4-execute’ +‘C-c C-x’ or ‘C-c C-l’ Execute Lean4 in stand-alone mode ‘lean4-execute’ ‘C-c C-p C-l’ Builds package with lake ‘lean4-lake-build’ ‘C-c C-i’ Toggle Info-View which shows goals and errors at point ‘lean4-info-mode’ @@ -438,28 +438,28 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: -Node: Top223 -Node: Installation1846 -Node: Brief and Generic Instructions2089 -Node: Detailed and Concrete Instructions3038 -Node: Instructions for Source-Based Use-Package4695 -Node: Native vc (Emacs 30 or later)5416 -Node: Doom-Emacs6324 -Node: Straight6750 -Node: Usage7250 -Node: lsp-mode8673 -Node: Flycheck8958 -Node: Configuration9568 -Node: lsp-mode (1)9758 -Node: Flycheck (1)10027 -Node: Common Pitfalls10512 -Node: Changelog11104 -Node: Upcoming Version11544 -Node: Version 112 from 2024-12-1013610 -Node: Version 111 from 2024-12-0214475 -Node: Version 110 from 2024-12-0114882 -Node: Version 101 from 2024-11-2115380 -Node: Version 10 from 2024-11-1615743 +Node: Top224 +Node: Installation1785 +Node: Brief and Generic Instructions2028 +Node: Detailed and Concrete Instructions2977 +Node: Instructions for Source-Based Use-Package4634 +Node: Native vc (Emacs 30 or later)5355 +Node: Doom-Emacs6263 +Node: Straight6689 +Node: Usage7189 +Node: lsp-mode8612 +Node: Flycheck8897 +Node: Configuration9507 +Node: lsp-mode (1)9697 +Node: Flycheck (1)9966 +Node: Common Pitfalls10451 +Node: Changelog11043 +Node: Upcoming Version11483 +Node: Version 112 from 2024-12-1013549 +Node: Version 111 from 2024-12-0214414 +Node: Version 110 from 2024-12-0114821 +Node: Version 101 from 2024-11-2115319 +Node: Version 10 from 2024-11-1615682  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index a7cd1a3..a45cdb6 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -1,26 +1,26 @@ \input texinfo @c -*- texinfo -*- @c %**start of header @setfilename lean4-mode.info -@settitle Lean4-Mode - Emacs major mode for Lean language +@settitle Emacs Lean4-Mode @documentencoding UTF-8 @documentlanguage en @c %**end of header @dircategory Emacs misc features @direntry -* Lean4-Mode: (lean4-mode). Emacs major mode for Lean language. +* Lean4-Mode: (lean4-mode). Emacs major mode for Lean4 language. @end direntry @finalout @titlepage -@title Lean4-Mode - Emacs major mode for Lean language +@title Emacs Lean4-Mode @end titlepage @contents @ifnottex @node Top -@top Lean4-Mode - Emacs major mode for Lean language +@top Emacs Lean4-Mode This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by providing a major mode for editing code written in version 4 of the programming language and theorem @@ -230,14 +230,14 @@ place the following code in your Emacs initialization file: @node Usage @chapter Usage -If things are working correctly, you should see the word "Lean 4" in +If things are working correctly, you should see the word "Lean4" in Emacs mode-line when you open a file with @samp{.lean} extension. Emacs will ask you to identify the @emph{project} this file belongs to. If you then type @samp{#check id}, the word @samp{#check} will be underlined, and hovering over it will show you the type of @code{id}. To view the proof state, run @code{lean4-info-mode} (@samp{C-c C-i}). This -will display the @samp{*Lean Goals*} buffer (like the Lean Info-View pane +will display the @samp{*Lean4 Goals*} buffer (like the Lean Info-View pane in VS-Code) in a separate window. @multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaa} @@ -251,7 +251,7 @@ in VS-Code) in a separate window. @tab Recompile and reload imports @tab @code{lean4-lsp-document-reopen} @item @samp{C-c C-x} or @samp{C-c C-l} -@tab Execute Lean in stand-alone mode +@tab Execute Lean4 in stand-alone mode @tab @code{lean4-execute} @item @samp{C-c C-p C-l} @tab Builds package with lake diff --git a/lean4-syntax.el b/lean4-syntax.el index e6dc1ca..06d7e23 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -39,7 +39,7 @@ "exists" "if" "then" "else" "from" "init_quot" "return" "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" "elab" "initialize" "builtin_initialize" "register_builtin_option" "induction" "cases" "generalizing" "unif_hint" "deriving") - "Lean keywords ending with `word' (not symbol).") + "Lean4 keywords ending with `word' (not symbol).") (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end))) (defconst lean4-constants @@ -50,17 +50,19 @@ "⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o" "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1" "^c" "≃c" "≅c" "×c" "×f" "×n" "+c" "+f" "+n" "ℕ₋₂") - "Lean constants.") + "Lean4 constants.") (defconst lean4-constants-regexp (regexp-opt lean4-constants)) (defconst lean4-numerals-regexp (eval `(rx word-start (one-or-more digit) (optional (and "." (zero-or-more digit))) word-end))) -(defconst lean4-warnings '("sorry") "Lean warnings.") +(defconst lean4-warnings '("sorry") "Lean4 warnings.") (defconst lean4-warnings-regexp (eval `(rx word-start (or ,@lean4-warnings) word-end))) -(defconst lean4-debugging '("unreachable!" "panic!" "assert!" "dbg_trace") "Lean debugging.") +(defconst lean4-debugging + '("unreachable!" "panic!" "assert!" "dbg_trace") + "Lean4 debugging.") (defconst lean4-debugging-regexp (eval `(rx word-start (or ,@lean4-debugging) word-end))) @@ -130,7 +132,7 @@ ?' ?_ ?! ??) (modify-syntax-entry it "w" st)) - ;; Lean operator chars + ;; Operator chars (--each (string-to-list "#$%&*+<=>@^|~:") (modify-syntax-entry it "." st)) @@ -197,7 +199,7 @@ (2 nil t) (3 font-lock-comment-face t))))) -;; Syntax Highlighting for Lean Info Mode +;; Syntax Highlighting for Lean4 Info (defconst lean4-info-font-lock-defaults (let ((new-entries `(;; Please add more after this: From 3c7aff7ccc57b383b32e49461a3fbc5ff0c8cdba Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:51 +0200 Subject: [PATCH 35/50] [input] Name input method "Lean4" --- lean4-input.el | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/lean4-input.el b/lean4-input.el index a0a3be8..902c18e 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -222,7 +222,7 @@ that contains all translations from QP Except for those corresponding to ASCII." "Display all translations used by the Quail package QP (a string). \(Except for those corresponding to ASCII)." (interactive (list (read-input-method-name - "Quail input method (default %s): " "Lean"))) + "Quail input method (default %s): " "Lean4"))) (let ((buf (concat "*" qp " input method translations*"))) (with-output-to-temp-buffer buf (with-current-buffer buf @@ -238,7 +238,7 @@ translations are appended to the current translations." (when key (quail-defrule (concat "\\" key) tr - "Lean" t))) + "Lean4" t))) trans))) (defun lean4-input-inherit-package (qp &optional fun) @@ -267,7 +267,7 @@ method." ;; Create (or reset) the input method. (with-temp-buffer - (quail-define-package "Lean" "UTF-8" "∏" t ; guidance + (quail-define-package "Lean4" "UTF-8" "∏" t ; guidance "Lean4 input method. The purpose of this input method is to edit Lean4 programs, but since it is highly customisable it can be made useful for other @@ -313,8 +313,8 @@ Suitable for use in the :set field of `defcustom'." (defun lean4-input-set () (interactive) - "Select and activate the `Lean' input method." - (set-input-method "Lean")) + "Select and activate the `Lean4' input method." + (set-input-method "Lean4")) (provide 'lean4-input) ;;; lean4-input.el ends here From ba32f827f75b13e14207db11ad45244620781327 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:54 +0200 Subject: [PATCH 36/50] [info] Name Info buffer "*Lean4 Info*" --- README.org | 2 +- lean4-info.el | 8 ++++---- lean4-mode.info | 28 ++++++++++++++-------------- lean4-mode.texi | 2 +- 4 files changed, 20 insertions(+), 20 deletions(-) diff --git a/README.org b/README.org index fd8a57b..7705929 100644 --- a/README.org +++ b/README.org @@ -147,7 +147,7 @@ then type =#check id=, the word =#check= will be underlined, and hovering over it will show you the type of ~id~. To view the proof state, run ~lean4-info-mode~ (=C-c C-i=). This -will display the =*Lean4 Goals*= buffer (like the Lean Info-View pane +will display the =*Lean4 Info*= buffer (like the Lean Info-View pane in VS-Code) in a separate window. | Key | Description | Command | diff --git a/lean4-info.el b/lean4-info.el index d92d583..e521604 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -48,7 +48,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean4." (defun lean4-info-ensure-buffer (buffer) "Create BUFFER if it does not exist. -Also choose settings used for the *Lean4 Goal* buffer." +Also choose settings used for the *Lean4 Info* buffer." (unless (get-buffer buffer) (with-current-buffer (get-buffer-create buffer) (buffer-disable-undo) @@ -72,7 +72,7 @@ Also choose settings used for the *Lean4 Goal* buffer." (:range :fullRange :message) (:code :relatedInformation :severity :source :tags)))) -(defconst lean4-info-buffer-name "*Lean4 Goal*") +(defconst lean4-info-buffer-name "*Lean4 Info*") (defvar lean4-info-goals nil) (defvar lean4-info-term-goal nil) @@ -219,7 +219,7 @@ Also choose settings used for the *Lean4 Goal* buffer." (defcustom lean4-info-buffer-debounce-delay-sec 0.1 - "Duration of time we wait before writing to *Lean4 Goal*." + "Duration of time we wait before writing to *Lean4 Info*." :group 'lean4-info :type 'number) @@ -278,7 +278,7 @@ sections." (defun lean4-info-buffer-refresh () - "Refresh the *Lean4 Goal* buffer." + "Refresh the *Lean4 Info* buffer." (when (lean4-info-buffer-active lean4-info-buffer-name) (lsp-request-async "$/lean/plainGoal" diff --git a/lean4-mode.info b/lean4-mode.info index 3188ae7..030493b 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -233,7 +233,7 @@ type ‘#check id’, the word ‘#check’ will be underlined, and hovering over it will show you the type of ‘id’. To view the proof state, run ‘lean4-info-mode’ (‘C-c C-i’). This -will display the ‘*Lean4 Goals*’ buffer (like the Lean Info-View pane in +will display the ‘*Lean4 Info*’ buffer (like the Lean Info-View pane in VS-Code) in a separate window. Key Description Command @@ -447,19 +447,19 @@ Node: Native vc (Emacs 30 or later)5355 Node: Doom-Emacs6263 Node: Straight6689 Node: Usage7189 -Node: lsp-mode8612 -Node: Flycheck8897 -Node: Configuration9507 -Node: lsp-mode (1)9697 -Node: Flycheck (1)9966 -Node: Common Pitfalls10451 -Node: Changelog11043 -Node: Upcoming Version11483 -Node: Version 112 from 2024-12-1013549 -Node: Version 111 from 2024-12-0214414 -Node: Version 110 from 2024-12-0114821 -Node: Version 101 from 2024-11-2115319 -Node: Version 10 from 2024-11-1615682 +Node: lsp-mode8611 +Node: Flycheck8896 +Node: Configuration9506 +Node: lsp-mode (1)9696 +Node: Flycheck (1)9965 +Node: Common Pitfalls10450 +Node: Changelog11042 +Node: Upcoming Version11482 +Node: Version 112 from 2024-12-1013548 +Node: Version 111 from 2024-12-0214413 +Node: Version 110 from 2024-12-0114820 +Node: Version 101 from 2024-11-2115318 +Node: Version 10 from 2024-11-1615681  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index a45cdb6..aea22e9 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -237,7 +237,7 @@ then type @samp{#check id}, the word @samp{#check} will be underlined, and hovering over it will show you the type of @code{id}. To view the proof state, run @code{lean4-info-mode} (@samp{C-c C-i}). This -will display the @samp{*Lean4 Goals*} buffer (like the Lean Info-View pane +will display the @samp{*Lean4 Info*} buffer (like the Lean Info-View pane in VS-Code) in a separate window. @multitable {aaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa} {aaaaaaaaaaaaaaaaaaaaaaaaaaa} From 16e51dc21d6837c9ad7d061b03b5be329bf2fc39 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:13:58 +0200 Subject: [PATCH 37/50] Use appropriate customization-groups everywhere --- lean4-fringe.el | 12 ++++++++---- lean4-info.el | 2 +- lean4-lsp.el | 4 ++++ 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/lean4-fringe.el b/lean4-fringe.el index 3a9fcb0..952ea56 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -25,9 +25,13 @@ (require 'lsp-mode) (require 'lsp-protocol) +(defgroup lean4-fringe nil + "Lean4 lsp-mode processing progress in fringes." + :group 'lean4) + (defcustom lean4-fringe-show-file-progress t "Highlight file progress in the current buffer." - :group 'lean4 + :group 'lean4-fringe :type 'boolean) (eval-and-compile @@ -43,7 +47,7 @@ (defface lean4-fringe-face nil "Face to highlight Lean4 file progress." - :group 'lean4) + :group 'lean4-fringe) (if (fboundp 'define-fringe-bitmap) (define-fringe-bitmap 'lean4-fringe-fringe-bitmap @@ -56,7 +60,7 @@ :background "navajo white") (t :inverse-video t)) "Face to highlight the fringe of Lean4 file processing progress." - :group 'lean4) + :group 'lean4-fringe) (defface lean4-fringe-fringe-fatal-error-face '((((class color) (background light)) @@ -65,7 +69,7 @@ :background "red") (t :inverse-video t)) "Face to highlight the fringe of Lean4 file fatal errors." - :group 'lean4) + :group 'lean4-fringe) (lsp-defun lean4-fringe-fringe-face ((&lean:LeanFileProgressProcessingInfo :kind)) (cond diff --git a/lean4-info.el b/lean4-info.el index e521604..1e4923d 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -43,7 +43,7 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean4." (define-derived-mode lean4-info-mockup-mode prog-mode "Lean4-Info" "Major mode used internally to syntax highlight Lean4." :syntax-table lean4-syntax-table - :group 'lean4 + :group 'lean4-info (setq-local font-lock-defaults lean4-info-font-lock-defaults)) (defun lean4-info-ensure-buffer (buffer) diff --git a/lean4-lsp.el b/lean4-lsp.el index 1faa188..789ab91 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -26,6 +26,10 @@ (require 'lsp-mode) +(defgroup lean4-lsp nil + "`lsp-mode' for Lean4." + :group 'lean4) + (defun lean4-lsp-document-reopen () "Refresh the file dependencies. From 4f4e621d3dae56907333b86bc1c237e8a292dce7 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:01 +0200 Subject: [PATCH 38/50] [info] Use same code citation style as elsewhere --- lean4-info.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-info.el b/lean4-info.el index 1e4923d..450e74c 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -244,7 +244,7 @@ the request." :group 'lean4-info :type 'number) -;; Debounce implementation modifed from lsp-lens +;; This is based on lsp-lens.el from lsp-mode: ;; https://github.com/emacs-lsp/lsp-mode/blob/2f0ea2e396ec9a570f2a2aeb097c304ddc61ebee/lsp-lens.el#L140 (defun lean4-info-buffer-redisplay-debounced () "Debounced version of `lean4-info-buffer-redisplay'. From 44aa4458225513a8305ea94e07be9b1ea18bdce8 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:04 +0200 Subject: [PATCH 39/50] Use same order of (require '...) forms everywhere 1. Built-ins 2. Third-party (any Elpa) 3. Local (lean4-*) --- lean4-info.el | 3 ++- lean4-input.el | 5 +++-- lean4-lsp.el | 1 - lean4-mode.el | 10 ++++++---- lean4-syntax.el | 3 ++- 5 files changed, 13 insertions(+), 9 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 450e74c..39d63d4 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -23,11 +23,12 @@ ;;; Code: (require 'dash) -(require 'lean4-syntax) (require 'lsp-mode) (require 'lsp-protocol) (require 'magit-section) +(require 'lean4-syntax) + (defgroup lean4-info nil "Lean4-Mode Info." :group 'lean4) diff --git a/lean4-input.el b/lean4-input.el index 902c18e..4a3122c 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -39,11 +39,12 @@ ;;; Code: -(require 'quail) (require 'cl-lib) +(require 'map) +(require 'quail) (require 'subr-x) + (require 'dash) -(require 'map) ;; Quail is quite stateful, so be careful when editing this code. Note ;; that with-temp-buffer is used below whenever buffer-local state is diff --git a/lean4-lsp.el b/lean4-lsp.el index 789ab91..bc43e8e 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -23,7 +23,6 @@ ;;; Code: (require 'compat) ;; for `defvar-keymap' - (require 'lsp-mode) (defgroup lean4-lsp nil diff --git a/lean4-mode.el b/lean4-mode.el index 73896da..eb7080c 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -42,15 +42,17 @@ ;;; Code: (require 'cl-lib) -(require 'dash) (require 'pcase) + +(require 'dash) + (require 'lean4-eri) -(require 'lean4-syntax) -(require 'lean4-info) (require 'lean4-fringe) +(require 'lean4-info) (require 'lean4-input) -(require 'lean4-markdown) (require 'lean4-lsp) +(require 'lean4-markdown) +(require 'lean4-syntax) ;; Declare symbols defined in external dependencies. This silences ;; byte-compiler warnings: diff --git a/lean4-syntax.el b/lean4-syntax.el index 06d7e23..bb3f0e4 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -22,9 +22,10 @@ ;;; Code: -(require 'dash) (require 'rx) +(require 'dash) + (defconst lean4-keywords1 '("import" "prelude" "protected" "private" "noncomputable" "unsafe" "partial" "renaming" "hiding" "begin" "constant" From 8ebf81762e134b9b31b9cd48e1acd4874fbd637f Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:08 +0200 Subject: [PATCH 40/50] Use same copyright statement style everywhere MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Citing Wikipedia : “The requirement to add the "all rights reserved" notice became essentially obsolete on August 23, 2000, when Nicaragua became the final member of the Buenos Aires Convention to also become a signatory to the Berne Convention. As of that date, every country that was a member of the Buenos Aires Convention (which is the only copyright treaty requiring this notice to be used) was also a member of Berne, which requires protection be granted without any formality of notice of copyright.” --- lean4-fringe.el | 2 +- lean4-info.el | 2 +- lean4-mode.el | 4 ++-- lean4-syntax.el | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lean4-fringe.el b/lean4-fringe.el index 952ea56..959ac79 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -1,6 +1,6 @@ ;;; lean4-fringe.el --- Lean4 fringe progress -*- lexical-binding: t; -*- -;; Copyright (c) 2016 Microsoft Corporation. All rights reserved. +;; Copyright (c) 2016 Microsoft Corporation ;; This file is not part of GNU Emacs. diff --git a/lean4-info.el b/lean4-info.el index 39d63d4..7b7b60d 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -1,6 +1,6 @@ ;;; lean4-info.el --- Lean4 info -*- lexical-binding: t; -*- -;; Copyright (c) 2016 Gabriel Ebner. All rights reserved. +;; Copyright (c) 2016 Gabriel Ebner ;; This file is not part of GNU Emacs. diff --git a/lean4-mode.el b/lean4-mode.el index eb7080c..2a9ead2 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -1,7 +1,7 @@ ;;; lean4-mode.el --- Lean4 major mode -*- lexical-binding: t; -*- -;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. -;; Copyright (c) 2014, 2015 Soonho Kong. All rights reserved. +;; Copyright (c) 2013, 2014 Microsoft Corporation +;; Copyright (c) 2014, 2015 Soonho Kong ;; Author: Leonardo de Moura ;; Soonho Kong diff --git a/lean4-syntax.el b/lean4-syntax.el index bb3f0e4..b25f5f2 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -1,6 +1,6 @@ ;;; lean4-syntax.el --- Lean4 syntax -*- lexical-binding: t; -*- -;; Copyright (c) 2013, 2014 Microsoft Corporation. All rights reserved. +;; Copyright (c) 2013, 2014 Microsoft Corporation ;; This file is not part of GNU Emacs. From 58359e947e85a087f1eb91b6d6002fb56b396253 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:11 +0200 Subject: [PATCH 41/50] Use same capitalization of "not part of gnu emacs" everywhere --- lean4-eri.el | 2 +- lean4-fringe.el | 2 +- lean4-info.el | 2 +- lean4-input.el | 2 +- lean4-mode.el | 2 +- lean4-syntax.el | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lean4-eri.el b/lean4-eri.el index 35dcff4..3295a1f 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -4,7 +4,7 @@ ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, ;; Marcin Benke, Darin Morrison. -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You diff --git a/lean4-fringe.el b/lean4-fringe.el index 959ac79..8da4fa6 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -2,7 +2,7 @@ ;; Copyright (c) 2016 Microsoft Corporation -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You diff --git a/lean4-info.el b/lean4-info.el index 7b7b60d..50ca11f 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -2,7 +2,7 @@ ;; Copyright (c) 2016 Gabriel Ebner -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You diff --git a/lean4-input.el b/lean4-input.el index 4a3122c..a207571 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -4,7 +4,7 @@ ;; Catarina Coquand, Makoto Takeyama, Andreas Abel, Karl Mehltretter, ;; Marcin Benke, Darin Morrison. -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You diff --git a/lean4-mode.el b/lean4-mode.el index 2a9ead2..36dae45 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -15,7 +15,7 @@ ;; SPDX-License-Identifier: Apache-2.0 ;; Version: 1.1.2 -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You diff --git a/lean4-syntax.el b/lean4-syntax.el index b25f5f2..ec774b6 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -2,7 +2,7 @@ ;; Copyright (c) 2013, 2014 Microsoft Corporation -;; This file is not part of GNU Emacs. +;; This file is NOT part of GNU Emacs. ;; Licensed under the Apache License, Version 2.0 (the "License"); you ;; may not use this file except in compliance with the License. You From 1950502cecbd2d5444561de1ff85eefd52f9e53a Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:14 +0200 Subject: [PATCH 42/50] Rephrase comments; use at most one consecutive blank line everywhere - Rephrase some comments - Reduce multiple consecutive blank lines to single blank lines - Avoid exceeding fill-column with comments - Use `;;;;* ` prefix for outline/heading comments (for code navigation) --- lean4-info.el | 18 ++++++------------ lean4-input.el | 47 ++++++++++++++++++++++++----------------------- lean4-lsp.el | 5 +++-- lean4-mode.el | 4 +--- lean4-syntax.el | 8 +++++++- 5 files changed, 41 insertions(+), 41 deletions(-) diff --git a/lean4-info.el b/lean4-info.el index 50ca11f..3913b63 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -218,17 +218,14 @@ Also choose settings used for the *Lean4 Info* buffer." ;; >longer than `debounce-upper-bound-sec'< ;; -------------------------r4.render(FORCED) - (defcustom lean4-info-buffer-debounce-delay-sec 0.1 "Duration of time we wait before writing to *Lean4 Info*." :group 'lean4-info :type 'number) - (defvar lean4-info-buffer-debounce-timer nil "Timer that is used to debounce Lean4 info view refresh.") - (defvar lean4-info-buffer-debounce-begin-time nil "Return the time we have begun debouncing. @@ -253,20 +250,20 @@ the request." This version ensures that info buffer is not repeatedly written to. This is to prevent lag, because magit is quite slow at building sections." - ;; if we have not begun debouncing, setup debouncing begin time. + ;; If we have not begun debouncing, setup debouncing begin time. (if (not lean4-info-buffer-debounce-begin-time) (setq lean4-info-buffer-debounce-begin-time (current-time))) - ;; if time since we began debouncing is too long... + ;; If time since we began debouncing is too long... (if (>= (time-to-seconds (time-subtract (current-time) lean4-info-buffer-debounce-begin-time)) lean4-info-buffer-debounce-upper-bound-sec) - ;; then redisplay immediately. + ;; then redisplay immediately. (progn - ;; We have stopped debouncing. + ;; We have stopped debouncing. (setq lean4-info-buffer-debounce-begin-time nil) (lean4-info-buffer-redisplay)) - ;; else cancel current timer, create new debounced timer. + ;; Else, cancel current timer and create new debounced timer. (-some-> lean4-info-buffer-debounce-timer cancel-timer) (setq lean4-info-buffer-debounce-timer ; set new timer (run-with-timer @@ -298,10 +295,7 @@ sections." (lean4-info-buffer-redisplay-debounced)) :error-handler #'ignore :mode 'tick - :cancel-token :plain-term-goal) - ;; may lead to flickering - ;(lean4-info-buffer-redisplay) - )) + :cancel-token :plain-term-goal))) (defcustom lean4-info-hookings (list diff --git a/lean4-input.el b/lean4-input.el index a207571..eca3f7a 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -46,12 +46,12 @@ (require 'dash) -;; Quail is quite stateful, so be careful when editing this code. Note -;; that with-temp-buffer is used below whenever buffer-local state is -;; modified. +;; Quail is quite stateful, so be careful when editing this code. +;; Note that `with-temp-buffer' is used below whenever buffer-local +;; state is modified. -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Utility functions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Utility functions (defun lean4-input-concat-map (f xs) "Concat (map F XS)." @@ -73,8 +73,8 @@ First remove all space and newline characters." (setq seq (cons (+ from i) seq))) (concat (nreverse seq)))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Functions used to tweak translation pairs +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Functions used to tweak translation pairs (defun lean4-input-compose (f g) "\\x -> concatMap F (G x)." @@ -135,15 +135,17 @@ This suffix is dropped." (lean4-input-drop-end (length suffix)) (lean4-input-suffix suffix))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Customization +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Customization -;; The :set keyword is set to 'lean4-input-incorporate-changed-setting -;; so that the input method gets updated immediately when users -;; customize it. However, the setup functions cannot be run before all -;; variables have been defined. Hence the :initialize keyword is set to -;; 'custom-initialize-default to ensure that the setup is not performed -;; until lean4-input-setup is called at the end of this file. +;; The `:set' keyword is set to +;; `lean4-input-incorporate-changed-setting' so that the input method +;; gets updated immediately when users customize it. However, the +;; setup functions cannot be run before all variables have been +;; defined. Hence the `:initialize' keyword is set to +;; `custom-initialize-default' to ensure that the setup is not +;; performed until `lean4-input-setup' is called at the end of this +;; file. (defgroup lean4-input nil "The Lean4 input method. @@ -212,7 +214,7 @@ from other input methods." Result is a list of pairs (KEY-SEQUENCE . TRANSLATION) that contains all translations from QP Except for those corresponding to ASCII." (with-temp-buffer - (activate-input-method qp) ; To make sure that the package is loaded. + (activate-input-method qp) ;; Ensure that package is loaded. (unless (quail-package qp) (error "%s is not a Quail package" qp)) (let ((decode-map (list 'decode-map))) @@ -255,8 +257,8 @@ a list of such pairs." (if fun (lean4-input-concat-map fun trans) trans)))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Setting up the input method +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Setting up the input method (defvar json-key-type) (declare-function json-read "json") @@ -265,7 +267,6 @@ a list of such pairs." "Set up the Lean4 input method. Use customisable variables and parent input methods to setup Lean4 input method." - ;; Create (or reset) the input method. (with-temp-buffer (quail-define-package "Lean4" "UTF-8" "∏" t ; guidance @@ -283,9 +284,10 @@ tasks as well." "abbreviations.json" lean4-input-data-directory)) (thread-last - (let ((json-key-type 'string)) ;; make sure json key is a string. - ;; Prefer emacs native support implemented in C (since 27.1). - ;; Back-up is still useful in case Emacs in not compiled `--with-json`. + (let ((json-key-type 'string)) ;; Make sure json key is string. + ;; Prefer Emacs native support implemented in C (since 27.1). + ;; Back-up is still useful in case Emacs in not compiled + ;; `--with-json'. (if (fboundp 'json-parse-buffer) (json-parse-buffer) (require 'json) @@ -305,7 +307,6 @@ Suitable for use in the :set field of `defcustom'." (lean4-input-setup)) ;; Set up the input method. - (cl-eval-when (load eval) (lean4-input-setup)) diff --git a/lean4-lsp.el b/lean4-lsp.el index bc43e8e..75bba4d 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -57,8 +57,9 @@ of the parent project." (let (root) (when-let ((file-name (buffer-file-name))) (while-let ((dir (locate-dominating-file file-name "lean-toolchain"))) - ;; We found a toolchain file, but maybe it belongs to a package. - ;; Continue looking until there are no more toolchain files. + ;; We found a toolchain file, but maybe it belongs to a + ;; package. Continue looking until there are no more + ;; toolchain files. (setq root dir file-name (file-name-directory (directory-file-name dir))))) (when root diff --git a/lean4-mode.el b/lean4-mode.el index 36dae45..3543f24 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -54,8 +54,7 @@ (require 'lean4-markdown) (require 'lean4-syntax) -;; Declare symbols defined in external dependencies. This silences -;; byte-compiler warnings: +;; Suppress byte-compiler warnings: (defvar compilation-mode-font-lock-keywords) (declare-function quail-show-key "quail") @@ -136,7 +135,6 @@ (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) -;; Use utf-8 encoding ;;;###autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) diff --git a/lean4-syntax.el b/lean4-syntax.el index ec774b6..6bfb41e 100644 --- a/lean4-syntax.el +++ b/lean4-syntax.el @@ -41,8 +41,10 @@ "mutual" "def" "run_cmd" "declare_syntax_cat" "syntax" "macro_rules" "macro" "scoped" "elab" "initialize" "builtin_initialize" "register_builtin_option" "induction" "cases" "generalizing" "unif_hint" "deriving") "Lean4 keywords ending with `word' (not symbol).") + (defconst lean4-keywords1-regexp (eval `(rx word-start (or ,@lean4-keywords1) word-end))) + (defconst lean4-constants '("#" "@" "!" "$" "->" "∼" "↔" "/" "==" "=" ":=" "<->" "/\\" "\\/" "∧" "∨" "≠" "<" ">" "≤" "≥" "¬" "<=" ">=" "⁻¹" "⬝" "▸" "+" "*" "-" "/" "λ" @@ -52,22 +54,26 @@ "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1" "^c" "≃c" "≅c" "×c" "×f" "×n" "+c" "+f" "+n" "ℕ₋₂") "Lean4 constants.") + (defconst lean4-constants-regexp (regexp-opt lean4-constants)) + (defconst lean4-numerals-regexp (eval `(rx word-start (one-or-more digit) (optional (and "." (zero-or-more digit))) word-end))) (defconst lean4-warnings '("sorry") "Lean4 warnings.") + (defconst lean4-warnings-regexp (eval `(rx word-start (or ,@lean4-warnings) word-end))) + (defconst lean4-debugging '("unreachable!" "panic!" "assert!" "dbg_trace") "Lean4 debugging.") + (defconst lean4-debugging-regexp (eval `(rx word-start (or ,@lean4-debugging) word-end))) - (defconst lean4-syntax-table (let ((st (make-syntax-table))) ;; Matching parens From 6de82510f336de444fe46e60047afd3ef6652f89 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:18 +0200 Subject: [PATCH 43/50] Rephrase commentaries --- lean4-eri.el | 4 ++ lean4-fringe.el | 6 ++- lean4-info.el | 122 +++++++++++++++++++++++++--------------------- lean4-input.el | 10 ++-- lean4-lsp.el | 3 +- lean4-markdown.el | 3 +- lean4-mode.el | 10 ++-- 7 files changed, 87 insertions(+), 71 deletions(-) diff --git a/lean4-eri.el b/lean4-eri.el index 3295a1f..745d507 100644 --- a/lean4-eri.el +++ b/lean4-eri.el @@ -20,6 +20,10 @@ ;;; Commentary: +;; This file eventually defines the `lean4-eri-tab' command that +;; context-sensitively indents the current line, as appropriate for +;; the Lean4 language. + ;; This file is based on eri.el which was part of Agda-Mode: ;; https://github.com/agda/agda/blob/b40c6fc2e0ced7b547553654f81e5898082d700c/src/data/emacs-mode/eri.el diff --git a/lean4-fringe.el b/lean4-fringe.el index 8da4fa6..b695de9 100644 --- a/lean4-fringe.el +++ b/lean4-fringe.el @@ -18,7 +18,11 @@ ;;; Commentary: -;; Show Lean4 processing progress in the editor fringe +;; In `lean4-mode', indicate the processing progress of `lsp-mode' in +;; Emacs window fringes. + +;; For documentation on Emacs fringes, see (info "(emacs) Fringes") or +;; equally: https://gnu.org/s/emacs/manual/html_node/emacs/Fringes ;;; Code: diff --git a/lean4-info.el b/lean4-info.el index 3913b63..a892e96 100644 --- a/lean4-info.el +++ b/lean4-info.el @@ -18,7 +18,72 @@ ;;; Commentary: -;; This library provides an advanced LSP feature for `lean4-mode'. +;; This file defines `lean4-info-mode', a minor mode for `lean4-mode' +;; that keeps a buffer updated with an appealing display of LSP backed +;; information relevant at point, such as proof goals, type signatures +;; and error messages. + +;;;; Details on Debouncing + +;; We want to update the Lean4 info buffer as seldom as possible, +;; since magit-section is slow at rendering. We wait a small duration +;; (`debounce-delay-sec') when we get a redisplay request, to see if +;; there is a redisplay request in the future that invalidates the +;; current request (debouncing). Pictorially: + +;; (a) One request: +;; --r1 +;; --r1.wait +;; ----------r1.render + +;; (b) Two requests in quick succession: +;; +;; --r1 +;; --r1.wait +;; --------r2(cancel r1.wait) +;; --------r2.wait +;; ---------------r2.render + +;; (c) Two requests, not in succession: +;; +;; --r1 +;; --r1.wait +;; ---------r1.render +;; ------------------r2 +;; ------------------r2.wait +;; -------------------------r2.render + +;; This delaying can lead to a pathological case where we continually +;; stagger, while not rendering anything: +;; +;; --r1 +;; --r1.wait +;; --------r2(cancel r1.wait) +;; --------r2.wait +;; --------------r3(cancel r2.wait) +;; ---------------r3.wait +;; ---------------------r4(cancel r3.wait) +;; ---------------------... + +;; We prevent this pathological case by keeping track of when when we +;; began debouncing in `lean4-info-buffer-debounce-begin-time'. If we +;; have been debouncing for longer than +;; `lean4-info-buffer-debounce-upper-bound-sec', then we immediately +;; write instead of debouncing; `max-debounces' times. Upon trying to +;; stagger the `max-debounces'th request, we immediately render: +;; +;; begin-time:nil----t0----------------nil------- +;; -------r1 | +;; -------r1.wait | +;; -------|-----r2(cancel r1.wait) +;; -------|-----r2.wait | +;; -------|-----------r3(cancel r2.wait) +;; -------|-----------r3.wait +;; -------|-----------------r4(cancel r3.wait) +;; -------|-----------------| +;; >-----------------< +;; >longer than `debounce-upper-bound-sec'< +;; -------------------------r4.render(FORCED) ;;; Code: @@ -163,61 +228,6 @@ Also choose settings used for the *Lean4 Info* buffer." (lean4-info--mk-message-section 'errors-below "Messages below:" errors-below buffer) (lean4-info--mk-message-section 'errors-above "Messages above:" errors-above buffer))))))) -;; Debouncing -;; ~~~~~~~~~~~ -;; We want to update the Lean4 info buffer as seldom as possible, -;; since magit-section is slow at rendering. We -;; wait a small duration (`debounce-delay-sec') when we get a -;; redisplay request, to see if there is a redisplay request in the -;; future that invalidates the current request (debouncing). -;; Pictorially, -;; (a) One request: -;; --r1 -;; --r1.wait -;; ----------r1.render -;; (b) Two requests in quick succession: -;; --r1 -;; --r1.wait -;; --------r2(cancel r1.wait) -;; --------r2.wait -;; ---------------r2.render -;; (c) Two requests, not in succession: -;; --r1 -;; --r1.wait -;; ---------r1.render -;; ------------------r2 -;; ------------------r2.wait -;; -------------------------r2.render -;; This delaying can lead to a pathological case where we continually -;; stagger, while not rendering anything: -;; --r1 -;; --r1.wait -;; --------r2(cancel r1.wait) -;; --------r2.wait -;; --------------r3(cancel r2.wait) -;; ---------------r3.wait -;; ---------------------r4(cancel r3.wait) -;; ---------------------... -;; We prevent this pathological case by keeping track of when -;; when we began debouncing in `lean4-info-buffer-debounce-begin-time'. -;; If we have been debouncing for longer than -;; `lean4-info-buffer-debounce-upper-bound-sec', then we -;; immediately write instead of debouncing; -;; `max-debounces' times. Upon trying to stagger the -;; `max-debounces'th request, we immediately render: -;; begin-time:nil----t0----------------nil------- -;; -------r1 | -;; -------r1.wait | -;; -------|-----r2(cancel r1.wait) -;; -------|-----r2.wait | -;; -------|-----------r3(cancel r2.wait) -;; -------|-----------r3.wait -;; -------|-----------------r4(cancel r3.wait) -;; -------|-----------------| -;; >-----------------< -;; >longer than `debounce-upper-bound-sec'< -;; -------------------------r4.render(FORCED) - (defcustom lean4-info-buffer-debounce-delay-sec 0.1 "Duration of time we wait before writing to *Lean4 Info*." :group 'lean4-info diff --git a/lean4-input.el b/lean4-input.el index eca3f7a..83d09f7 100644 --- a/lean4-input.el +++ b/lean4-input.el @@ -24,11 +24,11 @@ ;; Quail input methods. By default the input method is geared towards ;; the input of mathematical and other symbols in Lean4 programs. -;; Use M-x customize-group lean4-input to customise this input method. -;; Note that the functions defined under "Functions used to tweak -;; translation pairs" below can be used to tweak both the key -;; translations inherited from other input methods as well as the -;; ones added specifically for this one. +;; Use M-x customize-group lean4-input RET to customize this input +;; method. Note that the functions defined under "Functions used to +;; tweak translation pairs" below can be used to tweak both the key +;; translations inherited from other input methods as well as the ones +;; added specifically for this one. ;; Use lean4-input-show-translations to see all the characters which ;; can be typed using this input method (except for those diff --git a/lean4-lsp.el b/lean4-lsp.el index 75bba4d..6ffab8a 100644 --- a/lean4-lsp.el +++ b/lean4-lsp.el @@ -18,7 +18,8 @@ ;;; Commentary: -;; This file connects `lean4-mode' and `lsp-mode' packages. +;; This file defines the `lean4-lsp-mode', a minor mode for +;; `lean4-mode' that appropriately sets up `lsp-mode'. ;;; Code: diff --git a/lean4-markdown.el b/lean4-markdown.el index ca68daa..6fb5fc8 100644 --- a/lean4-markdown.el +++ b/lean4-markdown.el @@ -18,7 +18,8 @@ ;;; Commentary: -;; This file connects `lean4-mode' and `markdown-mode' packages. +;; This file mutates `markdown-code-lang-modes' so that +;; `markdown-mode' supports Lean4 code blocks. ;;; Code: diff --git a/lean4-mode.el b/lean4-mode.el index 3543f24..d156cd4 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -31,13 +31,9 @@ ;;; Commentary: -;; Provides a major mode for the Lean4 programming language. - -;; Provides highlighting, diagnostics, goal visualization, -;; and many other useful features for Lean4 users. - -;; See the README.md for more advanced features and the -;; associated keybindings. +;; Lean4-Mode is a package providing an equally named major mode for +;; Lean version 4, a programming language and theorem prover. Consult +;; the readme or equivalent manual for further information. ;;; Code: From 7a34f0413c266290a4475a12f89b1adde2dd8eab Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:33 +0200 Subject: [PATCH 44/50] [readme] Rephrase introduction --- README.org | 14 +++++------- lean4-mode.info | 60 +++++++++++++++++++++++-------------------------- lean4-mode.texi | 14 +++++------- 3 files changed, 38 insertions(+), 50 deletions(-) diff --git a/README.org b/README.org index 7705929..5a4f67b 100644 --- a/README.org +++ b/README.org @@ -5,16 +5,12 @@ #+texinfo_dir_title: Lean4-Mode: (lean4-mode). #+texinfo_dir_desc: Emacs major mode for Lean4 language -This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing -code written in version 4 of the programming language and theorem -prover [[https://lean-lang.org][Lean]]. +This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by a major mode for [[https://lean-lang.org][Lean]] version 4, a +programming language and theorem prover. -The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues -tracked there too. Further discussions and question-answering takes -place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat. - -For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known -as /Lean-Mode/). +Lean4-Mode is developed on [[https://github.com/leanprover-community/lean4-mode][Github]]. Bugs and feature requests are also +tracked there. Further discussions take place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs]] channel +on the Lean Zulip chat platform. * Installation diff --git a/lean4-mode.info b/lean4-mode.info index 030493b..5b9e580 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -13,18 +13,14 @@ Emacs Lean4-Mode **************** This package extends GNU Emacs (https://www.gnu.org/software/emacs/) by -providing a major mode for editing code written in version 4 of the -programming language and theorem prover Lean (https://lean-lang.org). +a major mode for Lean (https://lean-lang.org) version 4, a programming +language and theorem prover. - The Lean4-Mode source code is developed at Github -(https://github.com/leanprover-community/lean4-mode) and its issues -tracked there too. Further discussions and question-answering takes -place in the #Emacs channel -(https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs) of -Lean's Zulip chat. - - For legacy version 3 of Lean, use the archived Lean3-Mode -(https://github.com/leanprover/lean3-mode) (also known as _Lean-Mode_). + Lean4-Mode is developed on Github +(https://github.com/leanprover-community/lean4-mode). Bugs and feature +requests are also tracked there. Further discussions take place in the +#Emacs (https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs) +channel on the Lean Zulip chat platform. * Menu: @@ -439,27 +435,27 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: Node: Top224 -Node: Installation1785 -Node: Brief and Generic Instructions2028 -Node: Detailed and Concrete Instructions2977 -Node: Instructions for Source-Based Use-Package4634 -Node: Native vc (Emacs 30 or later)5355 -Node: Doom-Emacs6263 -Node: Straight6689 -Node: Usage7189 -Node: lsp-mode8611 -Node: Flycheck8896 -Node: Configuration9506 -Node: lsp-mode (1)9696 -Node: Flycheck (1)9965 -Node: Common Pitfalls10450 -Node: Changelog11042 -Node: Upcoming Version11482 -Node: Version 112 from 2024-12-1013548 -Node: Version 111 from 2024-12-0214413 -Node: Version 110 from 2024-12-0114820 -Node: Version 101 from 2024-11-2115318 -Node: Version 10 from 2024-11-1615681 +Node: Installation1602 +Node: Brief and Generic Instructions1845 +Node: Detailed and Concrete Instructions2794 +Node: Instructions for Source-Based Use-Package4451 +Node: Native vc (Emacs 30 or later)5172 +Node: Doom-Emacs6080 +Node: Straight6506 +Node: Usage7006 +Node: lsp-mode8428 +Node: Flycheck8713 +Node: Configuration9323 +Node: lsp-mode (1)9513 +Node: Flycheck (1)9782 +Node: Common Pitfalls10267 +Node: Changelog10859 +Node: Upcoming Version11299 +Node: Version 112 from 2024-12-1013365 +Node: Version 111 from 2024-12-0214230 +Node: Version 110 from 2024-12-0114637 +Node: Version 101 from 2024-11-2115135 +Node: Version 10 from 2024-11-1615498  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index aea22e9..4c6fea9 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -22,16 +22,12 @@ @node Top @top Emacs Lean4-Mode -This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by providing a major mode for editing -code written in version 4 of the programming language and theorem -prover @uref{https://lean-lang.org, Lean}. +This package extends @uref{https://www.gnu.org/software/emacs/, GNU Emacs} by a major mode for @uref{https://lean-lang.org, Lean} version 4, a +programming language and theorem prover. -The Lean4-Mode source code is developed at @uref{https://github.com/leanprover-community/lean4-mode, Github} and its issues -tracked there too. Further discussions and question-answering takes -place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs channel} of Lean's Zulip chat. - -For legacy version 3 of Lean, use the archived @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode} (also known -as @emph{Lean-Mode}). +Lean4-Mode is developed on @uref{https://github.com/leanprover-community/lean4-mode, Github}. Bugs and feature requests are also +tracked there. Further discussions take place in the @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs, #Emacs} channel +on the Lean Zulip chat platform. @end ifnottex From cb3d1c8cbff948f1d8c4b8c78cbec1ef100171fe Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:14:56 +0200 Subject: [PATCH 45/50] [readme] Reindent code; rephrase "Doom-Emacs" section headline --- README.org | 18 ++++++------- lean4-mode.info | 72 ++++++++++++++++++++++++------------------------- lean4-mode.texi | 24 ++++++++--------- 3 files changed, 57 insertions(+), 57 deletions(-) diff --git a/README.org b/README.org index 5a4f67b..2b03b22 100644 --- a/README.org +++ b/README.org @@ -102,23 +102,23 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) #+end_src -*** Doom-Emacs +*** Doom ~package!~ If you use Doom-Emacs, you can place the following code in your Doom initialization file: #+begin_src elisp (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) #+end_src *** Straight diff --git a/lean4-mode.info b/lean4-mode.info index 5b9e580..a768ddf 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -41,7 +41,7 @@ Installation Instructions for Source-Based Use-Package * Native vc (Emacs 30 or later):: -* Doom-Emacs:: +* Doom package!:: * Straight:: Usage @@ -160,11 +160,11 @@ specify ‘lean4-mode’ as a ‘:command’. * Menu: * Native vc (Emacs 30 or later):: -* Doom-Emacs:: +* Doom package!:: * Straight::  -File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom-Emacs, Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom package!, Up: Instructions for Source-Based Use-Package 1.3.1 Native ‘:vc’ (Emacs 30 or later) -------------------------------------- @@ -181,28 +181,28 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + ))  -File: lean4-mode.info, Node: Doom-Emacs, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Doom package!, Next: Straight, Prev: Native vc (Emacs 30 or later), Up: Instructions for Source-Based Use-Package -1.3.2 Doom-Emacs ----------------- +1.3.2 Doom ‘package!’ +--------------------- If you use Doom-Emacs, you can place the following code in your Doom initialization file: (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data")))  -File: lean4-mode.info, Node: Straight, Prev: Doom-Emacs, Up: Instructions for Source-Based Use-Package +File: lean4-mode.info, Node: Straight, Prev: Doom package!, Up: Instructions for Source-Based Use-Package 1.3.3 Straight -------------- @@ -435,27 +435,27 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: Node: Top224 -Node: Installation1602 -Node: Brief and Generic Instructions1845 -Node: Detailed and Concrete Instructions2794 -Node: Instructions for Source-Based Use-Package4451 -Node: Native vc (Emacs 30 or later)5172 -Node: Doom-Emacs6080 -Node: Straight6506 -Node: Usage7006 -Node: lsp-mode8428 -Node: Flycheck8713 -Node: Configuration9323 -Node: lsp-mode (1)9513 -Node: Flycheck (1)9782 -Node: Common Pitfalls10267 -Node: Changelog10859 -Node: Upcoming Version11299 -Node: Version 112 from 2024-12-1013365 -Node: Version 111 from 2024-12-0214230 -Node: Version 110 from 2024-12-0114637 -Node: Version 101 from 2024-11-2115135 -Node: Version 10 from 2024-11-1615498 +Node: Installation1605 +Node: Brief and Generic Instructions1848 +Node: Detailed and Concrete Instructions2797 +Node: Instructions for Source-Based Use-Package4454 +Node: Native vc (Emacs 30 or later)5178 +Node: Doom package!6094 +Node: Straight6564 +Node: Usage7067 +Node: lsp-mode8489 +Node: Flycheck8774 +Node: Configuration9384 +Node: lsp-mode (1)9574 +Node: Flycheck (1)9843 +Node: Common Pitfalls10328 +Node: Changelog10920 +Node: Upcoming Version11360 +Node: Version 112 from 2024-12-1013426 +Node: Version 111 from 2024-12-0214291 +Node: Version 110 from 2024-12-0114698 +Node: Version 101 from 2024-11-2115196 +Node: Version 10 from 2024-11-1615559  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 4c6fea9..34f62e0 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -50,7 +50,7 @@ Installation Instructions for Source-Based Use-Package * Native @samp{vc} (Emacs 30 or later):: -* Doom-Emacs:: +* Doom @code{package!}:: * Straight:: Usage @@ -169,7 +169,7 @@ Following subsections show concrete examples. @menu * Native @samp{vc} (Emacs 30 or later):: -* Doom-Emacs:: +* Doom @code{package!}:: * Straight:: @end menu @@ -189,24 +189,24 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode - :vc (:url "https://github.com/leanprover-community/lean4-mode.git" - :rev :last-release - ;; Or, if you prefer the bleeding edge version of Lean4-Mode: - ;; :rev :newest - )) + :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" + :rev :last-release + ;; Or, if you prefer the bleeding edge version of Lean4-Mode: + ;; :rev :newest + )) @end lisp -@node Doom-Emacs -@subsection Doom-Emacs +@node Doom @code{package!} +@subsection Doom @code{package!} If you use Doom-Emacs, you can place the following code in your Doom initialization file: @lisp (package! lean4-mode - :recipe (:host github - :repo "leanprover-community/lean4-mode" - :files ("*.el" "data"))) + :recipe ( :host github + :repo "leanprover-community/lean4-mode" + :files ("*.el" "data"))) @end lisp @node Straight From f4b44cf4341f93ecdadb9343132db670390a97ab Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:15:42 +0200 Subject: [PATCH 46/50] [readme] Load package before customizing hook variables (#101) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Fixes issue #101 “Document the pitfall of modifying lean4-mode-hook before Lean4-Mode has been loaded”. --- README.org | 55 ++++++++++++++++++++++++ lean4-mode.info | 110 +++++++++++++++++++++++++++++++++++++++--------- lean4-mode.texi | 67 +++++++++++++++++++++++++++++ 3 files changed, 211 insertions(+), 21 deletions(-) diff --git a/README.org b/README.org index 2b03b22..38eff46 100644 --- a/README.org +++ b/README.org @@ -73,6 +73,9 @@ Lean4-Mode should now already be enabled when you open a file with Lean4-Mode on Emacs startup, e.g. in order to customize variables: #+begin_src elisp (require 'lean4-mode) + +;; Optionally, customize variables, e.g. hooks: +;; (add-hook 'lean4-...-hook #'...) #+end_src ** Instructions for Source-Based Use-Package @@ -85,6 +88,15 @@ If you use the ~use-package~ macro and intent to defer loading of packages in order to improve your Emacs startup time, then make sure to specify ~lean4-mode~ as a =:command=. +When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like ~lean4-mode-hook~ have non-nil initialization +values. And since ~use-package~ applies the =:hook= specifications +before package loading, you should avoid it. Instead, put +=(add-hook 'lean4-...-hook #'...)= under the =:config= section. (See +/Common Pitfalls/ section below.) + Following subsections show concrete examples. *** Native =:vc= (Emacs 30 or later) @@ -190,6 +202,8 @@ option accordingly. * Common Pitfalls +** Lean(3)-Mode + Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical reasons. In principle, it is fine to have both Lean3-Mode and @@ -197,6 +211,47 @@ Lean4-Mode installed at the same time. But note that Lean3-Mode uses the prefix =lean-= for its symbols. E.g. you should not use =lean-=-prefixed commands in a buffer with Lean4-Mode as major mode. +** Partial value of ~lean4-mode-hook~ or other hook variables + +If you customize a hook variable like ~lean4-mode-hook~ e.g. with +~add-hook~ or Use-Package's =:hook= keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +~lean4-mode-hook~ may not contain the ~lsp~ command and as a +consequence ~lsp-mode~ won't start automatically together with +Lean4-Mode. + +There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your ~add-hook~ form before it loads +the definition of the hook from Lean4-Mode package. (3.) ~add-hook~ +effectively initializes the passed hook-variable to nil when the +symbol has no value cell. And (4.), Use-Package applies passed =:hook= +specifications before package loading. + +If you do not use Use-Package, the solution is to load Lean4-Mode +before calling ~add-hook~, e.g. with ~require~: +#+begin_src elisp +(require 'lean4-mode) +(add-hook 'lean4-...-hook #'...) +#+end_src + +Or with ~with-eval-after-load~: +#+begin_src elisp +(with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) +(with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) +#+end_src + +If you do Use-Package, you can solve the problem by calling ~add-hook~ +within the =:config= section: +#+begin_src elisp +(use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) +#+end_src + * Changelog ** Upcoming Version diff --git a/lean4-mode.info b/lean4-mode.info index a768ddf..f043d34 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -54,6 +54,11 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Common Pitfalls + +* Lean(3)-Mode:: +* Partial value of lean4-mode-hook or other hook variables:: + Changelog * Upcoming Version:: @@ -141,6 +146,9 @@ Lean4-Mode repository to the ‘load-path’ list: on Emacs startup, e.g. in order to customize variables: (require 'lean4-mode) + ;; Optionally, customize variables, e.g. hooks: + ;; (add-hook 'lean4-...-hook #'...) +  File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed and Concrete Instructions, Up: Installation @@ -155,6 +163,15 @@ your Lean4-Mode package recipe. packages in order to improve your Emacs startup time, then make sure to specify ‘lean4-mode’ as a ‘:command’. + When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like ‘lean4-mode-hook’ have non-nil initialization values. +And since ‘use-package’ applies the ‘:hook’ specifications before +package loading, you should avoid it. Instead, put ‘(add-hook +'lean4-...-hook #'...)’ under the ‘:config’ section. (See _Common +Pitfalls_ section below.) + Following subsections show concrete examples. * Menu: @@ -311,6 +328,17 @@ File: lean4-mode.info, Node: Common Pitfalls, Next: Changelog, Prev: Configur 4 Common Pitfalls ***************** +* Menu: + +* Lean(3)-Mode:: +* Partial value of lean4-mode-hook or other hook variables:: + + +File: lean4-mode.info, Node: Lean(3)-Mode, Next: Partial value of lean4-mode-hook or other hook variables, Up: Common Pitfalls + +4.1 Lean(3)-Mode +================ + Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, use Lean3-Mode (https://github.com/leanprover/lean3-mode), which is also known as Lean-Mode due to historical reasons. In principle, it is fine @@ -319,6 +347,44 @@ note that Lean3-Mode uses the prefix ‘lean-’ for its symbols. E.g. you should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as major mode. + +File: lean4-mode.info, Node: Partial value of lean4-mode-hook or other hook variables, Prev: Lean(3)-Mode, Up: Common Pitfalls + +4.2 Partial value of ‘lean4-mode-hook’ or other hook variables +============================================================== + +If you customize a hook variable like ‘lean4-mode-hook’ e.g. with +‘add-hook’ or Use-Package's ‘:hook’ keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +‘lean4-mode-hook’ may not contain the ‘lsp’ command and as a consequence +‘lsp-mode’ won't start automatically together with Lean4-Mode. + + There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your ‘add-hook’ form before it loads +the definition of the hook from Lean4-Mode package. (3.) ‘add-hook’ +effectively initializes the passed hook-variable to nil when the symbol +has no value cell. And (4.), Use-Package applies passed ‘:hook’ +specifications before package loading. + + If you do not use Use-Package, the solution is to load Lean4-Mode +before calling ‘add-hook’, e.g. with ‘require’: + (require 'lean4-mode) + (add-hook 'lean4-...-hook #'...) + + Or with ‘with-eval-after-load’: + (with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) + (with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) + + If you do Use-Package, you can solve the problem by calling +‘add-hook’ within the ‘:config’ section: + (use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) +  File: lean4-mode.info, Node: Changelog, Prev: Common Pitfalls, Up: Top @@ -435,27 +501,29 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: Node: Top224 -Node: Installation1605 -Node: Brief and Generic Instructions1848 -Node: Detailed and Concrete Instructions2797 -Node: Instructions for Source-Based Use-Package4454 -Node: Native vc (Emacs 30 or later)5178 -Node: Doom package!6094 -Node: Straight6564 -Node: Usage7067 -Node: lsp-mode8489 -Node: Flycheck8774 -Node: Configuration9384 -Node: lsp-mode (1)9574 -Node: Flycheck (1)9843 -Node: Common Pitfalls10328 -Node: Changelog10920 -Node: Upcoming Version11360 -Node: Version 112 from 2024-12-1013426 -Node: Version 111 from 2024-12-0214291 -Node: Version 110 from 2024-12-0114698 -Node: Version 101 from 2024-11-2115196 -Node: Version 10 from 2024-11-1615559 +Node: Installation1701 +Node: Brief and Generic Instructions1944 +Node: Detailed and Concrete Instructions2893 +Node: Instructions for Source-Based Use-Package4645 +Node: Native vc (Emacs 30 or later)5890 +Node: Doom package!6806 +Node: Straight7276 +Node: Usage7779 +Node: lsp-mode9201 +Node: Flycheck9486 +Node: Configuration10096 +Node: lsp-mode (1)10286 +Node: Flycheck (1)10555 +Node: Common Pitfalls11040 +Node: Lean(3)-Mode11264 +Node: Partial value of lean4-mode-hook or other hook variables11888 +Node: Changelog13594 +Node: Upcoming Version14034 +Node: Version 112 from 2024-12-1016100 +Node: Version 111 from 2024-12-0216965 +Node: Version 110 from 2024-12-0117372 +Node: Version 101 from 2024-11-2117870 +Node: Version 10 from 2024-11-1618233  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 34f62e0..6229e83 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -63,6 +63,11 @@ Configuration * lsp-mode: lsp-mode (1). * Flycheck: Flycheck (1). +Common Pitfalls + +* Lean(3)-Mode:: +* Partial value of @code{lean4-mode-hook} or other hook variables:: + Changelog * Upcoming Version:: @@ -152,6 +157,9 @@ Lean4-Mode should now already be enabled when you open a file with Lean4-Mode on Emacs startup, e.g. in order to customize variables: @lisp (require 'lean4-mode) + +;; Optionally, customize variables, e.g. hooks: +;; (add-hook 'lean4-...-hook #'...) @end lisp @node Instructions for Source-Based Use-Package @@ -165,6 +173,15 @@ If you use the @code{use-package} macro and intent to defer loading of packages in order to improve your Emacs startup time, then make sure to specify @code{lean4-mode} as a @samp{:command}. +When customizing Lean4-Mode variables, make sure the customization +takes place after loading the Lean4-Mode package so that the variables +are correctly initialized first. For example, many Lean4-Mode hook +variables like @code{lean4-mode-hook} have non-nil initialization +values. And since @code{use-package} applies the @samp{:hook} specifications +before package loading, you should avoid it. Instead, put +@samp{(add-hook 'lean4-...-hook #'...)} under the @samp{:config} section. (See +@emph{Common Pitfalls} section below.) + Following subsections show concrete examples. @menu @@ -316,6 +333,14 @@ option accordingly. @node Common Pitfalls @chapter Common Pitfalls +@menu +* Lean(3)-Mode:: +* Partial value of @code{lean4-mode-hook} or other hook variables:: +@end menu + +@node Lean(3)-Mode +@section Lean(3)-Mode + Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical reasons. In principle, it is fine to have both Lean3-Mode and @@ -323,6 +348,48 @@ Lean4-Mode installed at the same time. But note that Lean3-Mode uses the prefix @samp{lean-} for its symbols. E.g. you should not use @samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode. +@node Partial value of @code{lean4-mode-hook} or other hook variables +@section Partial value of @code{lean4-mode-hook} or other hook variables + +If you customize a hook variable like @code{lean4-mode-hook} e.g. with +@code{add-hook} or Use-Package's @samp{:hook} keyword, you may end up with a +partial / incomplete value of the hook variable. For example, +@code{lean4-mode-hook} may not contain the @code{lsp} command and as a +consequence @code{lsp-mode} won't start automatically together with +Lean4-Mode. + +There are several reasons that lead to this situation in conjunction: +(1.) Lean4-Mode has non-nil initialization values for many of its hook +variables. (2.) Emacs evaluates your @code{add-hook} form before it loads +the definition of the hook from Lean4-Mode package. (3.) @code{add-hook} +effectively initializes the passed hook-variable to nil when the +symbol has no value cell. And (4.), Use-Package applies passed @samp{:hook} +specifications before package loading. + +If you do not use Use-Package, the solution is to load Lean4-Mode +before calling @code{add-hook}, e.g. with @code{require}: +@lisp +(require 'lean4-mode) +(add-hook 'lean4-...-hook #'...) +@end lisp + +Or with @code{with-eval-after-load}: +@lisp +(with-eval-after-load 'lean4-mode + (add-hook 'lean4-mode-hook #'...)) +(with-eval-after-load 'lean4-lsp + (add-hook 'lean4-lsp-mode-hook #'...)) +@end lisp + +If you do Use-Package, you can solve the problem by calling @code{add-hook} +within the @samp{:config} section: +@lisp +(use-package lean4-mode + ;; ... + :config + (add-hook 'lean4-...-hook #'...)) +@end lisp + @node Changelog @chapter Changelog From 470692398a6abd7f5e5e5494ca46a14a73eecce3 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:15:46 +0200 Subject: [PATCH 47/50] [makefile] Add autoload target and add it to [gitignore] --- .gitignore | 1 + Makefile | 29 ++++++++++++++++++++++------- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/.gitignore b/.gitignore index 433da84..2998b25 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .cask *.elc +lean4-mode-autoloads.el \ No newline at end of file diff --git a/Makefile b/Makefile index a848d37..7f8c87e 100644 --- a/Makefile +++ b/Makefile @@ -1,13 +1,28 @@ # GNU- and NonGNU-Elpa accept Org files as package documentation but # Melpa does not. As long as Lean4-Mode is not distributed on GNU- or # NonGNU-Elpa, it should ship with .texi and .info manuals. This -# depends on: GNU Emacs, Make and GNU Texinfo. +# depends on: GNU Emacs, Make, GNU Texinfo and the “sponge” program +# bundled in the “Moreutils” collection that is maintained by Joey +# Hess. -lean4-mode.info lean4-mode.texi: README.org - emacs --batch \ - "--eval=(require 'ox-texinfo)" \ - '--eval=(find-file "$<")' \ - '--eval=(org-texinfo-export-to-info)' +.PHONY: all autoload clean info +all : autoload info clean: - rm lean4-mode.info lean4-mode.texi + rm -f lean4-mode.info lean4-mode.texi lean4-mode-autoloads.el + +autoload: lean4-mode-autoloads.el +lean4-mode-autoloads.el : $(wildcard *.el) + emacs --batch \ + --eval '(setq make-backup-files nil)' \ + --eval '(setq generated-autoload-file "./$@")' \ + --eval "(require 'autoload)" \ + -f batch-update-autoloads '.' + cat $@ | sponge | sed s/"This file is part of GNU Emacs"/"This file is NOT part of GNU Emacs"/ > $@ + +info: lean4-mode.info lean4-mode.texi +lean4-mode.info lean4-mode.texi : README.org + emacs --batch \ + --eval "(require 'ox-texinfo)" \ + --eval '(find-file "$<")' \ + --eval '(org-texinfo-export-to-info)' From 6853e62d5c577fd0ad06ed0eeb61cece59ce0191 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:16:12 +0200 Subject: [PATCH 48/50] [readme] Elaborate on autoloading (#103) --- README.org | 69 +++++++++++++++++++------- lean4-mode.info | 128 ++++++++++++++++++++++++++++++------------------ lean4-mode.texi | 84 ++++++++++++++++++++++--------- 3 files changed, 193 insertions(+), 88 deletions(-) diff --git a/README.org b/README.org index 38eff46..7e17824 100644 --- a/README.org +++ b/README.org @@ -14,22 +14,30 @@ on the Lean Zulip chat platform. * Installation -** Brief and Generic Instructions +** Brief, Generic Instructions First, install the dependencies of Lean4-Mode: - [[https://lean-lang.org/lean4/doc/setup.html][Lean]] (version 4) - Emacs (version 27 or later) - Emacs packages [[https://github.com/magnars/dash.el][Dash]] (available on GNU-Elpa), [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (available on Melpa) +Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: -- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]]. -- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to that local - repository to the ~load-path~ list. -# Note that (require 'lean4-mode) is not necessary when the user -# relies on autoloading and uses the default settings. +- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository]]. +- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to your local + repository to ~load-path~. -** Detailed and Concrete Instructions +Third, ensure Lean4-Mode is loaded by one of the following ways: +- Load it eagerly. +- Load it lazily by associating ~lean4-mode~ with the =.lean= file + extension and setting it up as autoloaded command. +- Load it lazily by generating an autoload file (with the Make target + called =autoload=) and loading that in your init file. Make sure to + regenerate the autoload file, whenever you change the Lean4-Mode + repository (e.g. =git pull=). + +** Detailed, Native Instructions Install Lean version 4. @@ -68,26 +76,39 @@ Lean4-Mode repository to the ~load-path~ list: (add-to-list 'load-path "~/path/to/lean4-mode") #+end_src -Lean4-Mode should now already be enabled when you open a file with -=.lean= extension. But you can optionally also already load -Lean4-Mode on Emacs startup, e.g. in order to customize variables: +Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + +If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: #+begin_src elisp (require 'lean4-mode) +#+end_src + +If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 source +file is opened the first time, put in your init file: +#+begin_src elisp +(autoload 'lean4-mode "lean4-mode" nil t) +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) +#+end_src -;; Optionally, customize variables, e.g. hooks: -;; (add-hook 'lean4-...-hook #'...) +If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your +Git repository changes (e.g. =git pull=), run =make autoload= +inside. And put this in your init file: +#+begin_src elisp +(require 'lean4-mode-autoloads) #+end_src ** Instructions for Source-Based Use-Package +This section instructs how to set up Lean4-Mode through the +~use-package~ macro that is built into Emacs since version 29. + If you use a source-based package-manager (e.g. =package-vc.el=, Straight or Elpaca), then make sure to list the ="data"= directory in your Lean4-Mode package recipe. -If you use the ~use-package~ macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure -to specify ~lean4-mode~ as a =:command=. - When customizing Lean4-Mode variables, make sure the customization takes place after loading the Lean4-Mode package so that the variables are correctly initialized first. For example, many Lean4-Mode hook @@ -97,12 +118,22 @@ before package loading, you should avoid it. Instead, put =(add-hook 'lean4-...-hook #'...)= under the =:config= section. (See /Common Pitfalls/ section below.) +Use-Package [[https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html][involves]] some complexity when it comes to deciding whether +to load a package eagerly (/demand/) or lazily (/defer/). For example, +it depends on your configuration (e.g. ~use-package-always-defer~, +~use-package-always-demand~). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via =:demand t=. Alternatively, +you can defer loading e.g. via =:defer t= together with +=:mode "\\.lean\\'"= (which associates Lean4-Mode with the =.lean= +file extension) and =:commands lean4-mode= (which will set up +autoloading). + Following subsections show concrete examples. *** Native =:vc= (Emacs 30 or later) -GNU Emacs comes with =use-package.el= built-in since version 29. And -since version 30, it also comes with a built-in =:vc= keyword for the +Since version 30, Emacs comes with a built-in =:vc= keyword for the ~use-package~ macro that utilizes =package-vc.el= to install Emacs packages from remote source repositories. @@ -114,6 +145,7 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" :rev :last-release ;; Or, if you prefer the bleeding edge version of Lean4-Mode: @@ -141,6 +173,7 @@ place the following code in your Emacs initialization file: #+begin_src elisp (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) diff --git a/lean4-mode.info b/lean4-mode.info index f043d34..23928b3 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -34,8 +34,8 @@ channel on the Lean Zulip chat platform. Installation -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: Instructions for Source-Based Use-Package @@ -77,15 +77,15 @@ File: lean4-mode.info, Node: Installation, Next: Usage, Prev: Top, Up: Top * Menu: -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package::  -File: lean4-mode.info, Node: Brief and Generic Instructions, Next: Detailed and Concrete Instructions, Up: Installation +File: lean4-mode.info, Node: Brief Generic Instructions, Next: Detailed Native Instructions, Up: Installation -1.1 Brief and Generic Instructions -================================== +1.1 Brief, Generic Instructions +=============================== First, install the dependencies of Lean4-Mode: • Lean (https://lean-lang.org/lean4/doc/setup.html) (version 4) @@ -95,19 +95,29 @@ First, install the dependencies of Lean4-Mode: Magit-Section (https://github.com/magit/magit/blob/main/lisp/magit-section.el) (available on Melpa) + Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: - • Clone the Git repository of Lean4-Mode + • Clone the Git repository (https://github.com/leanprover-community/lean4-mode). • In your Emacs initialization file (https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html), - add the path to that local repository to the ‘load-path’ list. + add the path to your local repository to ‘load-path’. + + Third, ensure Lean4-Mode is loaded by one of the following ways: + • Load it eagerly. + • Load it lazily by associating ‘lean4-mode’ with the ‘.lean’ file + extension and setting it up as autoloaded command. + • Load it lazily by generating an autoload file (with the Make target + called ‘autoload’) and loading that in your init file. Make sure + to regenerate the autoload file, whenever you change the Lean4-Mode + repository (e.g. ‘git pull’).  -File: lean4-mode.info, Node: Detailed and Concrete Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief and Generic Instructions, Up: Installation +File: lean4-mode.info, Node: Detailed Native Instructions, Next: Instructions for Source-Based Use-Package, Prev: Brief Generic Instructions, Up: Installation -1.2 Detailed and Concrete Instructions -====================================== +1.2 Detailed, Native Instructions +================================= Install Lean version 4. @@ -141,28 +151,37 @@ approach, add the following to your Emacs initialization file (e.g. Lean4-Mode repository to the ‘load-path’ list: (add-to-list 'load-path "~/path/to/lean4-mode") - Lean4-Mode should now already be enabled when you open a file with -‘.lean’ extension. But you can optionally also already load Lean4-Mode -on Emacs startup, e.g. in order to customize variables: + Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + + If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: (require 'lean4-mode) - ;; Optionally, customize variables, e.g. hooks: - ;; (add-hook 'lean4-...-hook #'...) + If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 +source file is opened the first time, put in your init file: + (autoload 'lean4-mode "lean4-mode" nil t) + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) + + If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your Git +repository changes (e.g. ‘git pull’), run ‘make autoload’ inside. And +put this in your init file: + (require 'lean4-mode-autoloads)  -File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed and Concrete Instructions, Up: Installation +File: lean4-mode.info, Node: Instructions for Source-Based Use-Package, Prev: Detailed Native Instructions, Up: Installation 1.3 Instructions for Source-Based Use-Package ============================================= -If you use a source-based package-manager (e.g. ‘package-vc.el’, +This section instructs how to set up Lean4-Mode through the +‘use-package’ macro that is built into Emacs since version 29. + + If you use a source-based package-manager (e.g. ‘package-vc.el’, Straight or Elpaca), then make sure to list the ‘"data"’ directory in your Lean4-Mode package recipe. - If you use the ‘use-package’ macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure to -specify ‘lean4-mode’ as a ‘:command’. - When customizing Lean4-Mode variables, make sure the customization takes place after loading the Lean4-Mode package so that the variables are correctly initialized first. For example, many Lean4-Mode hook @@ -172,6 +191,18 @@ package loading, you should avoid it. Instead, put ‘(add-hook 'lean4-...-hook #'...)’ under the ‘:config’ section. (See _Common Pitfalls_ section below.) + Use-Package involves +(https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html) +some complexity when it comes to deciding whether to load a package +eagerly (_demand_) or lazily (_defer_). For example, it depends on your +configuration (e.g. ‘use-package-always-defer’, +‘use-package-always-demand’). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via ‘:demand t’. Alternatively, +you can defer loading e.g. via ‘:defer t’ together with ‘:mode +"\\.lean\\'"’ (which associates Lean4-Mode with the ‘.lean’ file +extension) and ‘:commands lean4-mode’ (which will set up autoloading). + Following subsections show concrete examples. * Menu: @@ -186,8 +217,7 @@ File: lean4-mode.info, Node: Native vc (Emacs 30 or later), Next: Doom package 1.3.1 Native ‘:vc’ (Emacs 30 or later) -------------------------------------- -GNU Emacs comes with ‘use-package.el’ built-in since version 29. And -since version 30, it also comes with a built-in ‘:vc’ keyword for the +Since version 30, Emacs comes with a built-in ‘:vc’ keyword for the ‘use-package’ macro that utilizes ‘package-vc.el’ to install Emacs packages from remote source repositories. @@ -198,6 +228,7 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" :rev :last-release ;; Or, if you prefer the bleeding edge version of Lean4-Mode: @@ -229,6 +260,7 @@ the following code in your Emacs initialization file: (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) @@ -501,29 +533,29 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: Node: Top224 -Node: Installation1701 -Node: Brief and Generic Instructions1944 -Node: Detailed and Concrete Instructions2893 -Node: Instructions for Source-Based Use-Package4645 -Node: Native vc (Emacs 30 or later)5890 -Node: Doom package!6806 -Node: Straight7276 -Node: Usage7779 -Node: lsp-mode9201 -Node: Flycheck9486 -Node: Configuration10096 -Node: lsp-mode (1)10286 -Node: Flycheck (1)10555 -Node: Common Pitfalls11040 -Node: Lean(3)-Mode11264 -Node: Partial value of lean4-mode-hook or other hook variables11888 -Node: Changelog13594 -Node: Upcoming Version14034 -Node: Version 112 from 2024-12-1016100 -Node: Version 111 from 2024-12-0216965 -Node: Version 110 from 2024-12-0117372 -Node: Version 101 from 2024-11-2117870 -Node: Version 10 from 2024-11-1618233 +Node: Installation1749 +Node: Brief Generic Instructions2040 +Node: Detailed Native Instructions3496 +Node: Instructions for Source-Based Use-Package5646 +Node: Native vc (Emacs 30 or later)7562 +Node: Doom package!8428 +Node: Straight8898 +Node: Usage9427 +Node: lsp-mode10849 +Node: Flycheck11134 +Node: Configuration11744 +Node: lsp-mode (1)11934 +Node: Flycheck (1)12203 +Node: Common Pitfalls12688 +Node: Lean(3)-Mode12912 +Node: Partial value of lean4-mode-hook or other hook variables13536 +Node: Changelog15242 +Node: Upcoming Version15682 +Node: Version 112 from 2024-12-1017748 +Node: Version 111 from 2024-12-0218613 +Node: Version 110 from 2024-12-0119020 +Node: Version 101 from 2024-11-2119518 +Node: Version 10 from 2024-11-1619881  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 6229e83..80e8bee 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -43,8 +43,8 @@ on the Lean Zulip chat platform. Installation -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: Instructions for Source-Based Use-Package @@ -84,13 +84,13 @@ Changelog @chapter Installation @menu -* Brief and Generic Instructions:: -* Detailed and Concrete Instructions:: +* Brief, Generic Instructions: Brief Generic Instructions. +* Detailed, Native Instructions: Detailed Native Instructions. * Instructions for Source-Based Use-Package:: @end menu -@node Brief and Generic Instructions -@section Brief and Generic Instructions +@node Brief Generic Instructions +@section Brief, Generic Instructions First, install the dependencies of Lean4-Mode: @itemize @@ -102,18 +102,33 @@ Emacs (version 27 or later) Emacs packages @uref{https://github.com/magnars/dash.el, Dash} (available on GNU-Elpa), @uref{https://emacs-lsp.github.io/lsp-mode, lsp-mode}, and @uref{https://github.com/magit/magit/blob/main/lisp/magit-section.el, Magit-Section} (available on Melpa) @end itemize +Additionally, we'll assume you have Git installed. Second, install Lean4-Mode itself: @itemize @item -Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository of Lean4-Mode}. +Clone the @uref{https://github.com/leanprover-community/lean4-mode, Git repository}. @item -In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to that local -repository to the @code{load-path} list. +In your @uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html, Emacs initialization file}, add the path to your local +repository to @code{load-path}. @end itemize -@node Detailed and Concrete Instructions -@section Detailed and Concrete Instructions +Third, ensure Lean4-Mode is loaded by one of the following ways: +@itemize +@item +Load it eagerly. +@item +Load it lazily by associating @code{lean4-mode} with the @samp{.lean} file +extension and setting it up as autoloaded command. +@item +Load it lazily by generating an autoload file (with the Make target +called @samp{autoload}) and loading that in your init file. Make sure to +regenerate the autoload file, whenever you change the Lean4-Mode +repository (e.g. @samp{git pull}). +@end itemize + +@node Detailed Native Instructions +@section Detailed, Native Instructions Install Lean version 4. @@ -152,27 +167,40 @@ Lean4-Mode repository to the @code{load-path} list: (add-to-list 'load-path "~/path/to/lean4-mode") @end lisp -Lean4-Mode should now already be enabled when you open a file with -@samp{.lean} extension. But you can optionally also already load -Lean4-Mode on Emacs startup, e.g. in order to customize variables: +Now you can choose one of the following ways to determine how +Lean4-Mode is loaded: + +If you want Emacs to load Lean4-Mode eagerly whenever it is started, +put in your init file: @lisp (require 'lean4-mode) +@end lisp -;; Optionally, customize variables, e.g. hooks: -;; (add-hook 'lean4-...-hook #'...) +If you want Emacs to load Lean4-Mode lazily, i.e. when a Lean4 source +file is opened the first time, put in your init file: +@lisp +(autoload 'lean4-mode "lean4-mode" nil t) +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode)) +@end lisp + +If you want Emacs to load Lean4-Mode lazily, you can also generate an +autoload file and load it in your init file. That is, whenever your +Git repository changes (e.g. @samp{git pull}), run @samp{make autoload} +inside. And put this in your init file: +@lisp +(require 'lean4-mode-autoloads) @end lisp @node Instructions for Source-Based Use-Package @section Instructions for Source-Based Use-Package +This section instructs how to set up Lean4-Mode through the +@code{use-package} macro that is built into Emacs since version 29. + If you use a source-based package-manager (e.g. @samp{package-vc.el}, Straight or Elpaca), then make sure to list the @samp{"data"} directory in your Lean4-Mode package recipe. -If you use the @code{use-package} macro and intent to defer loading of -packages in order to improve your Emacs startup time, then make sure -to specify @code{lean4-mode} as a @samp{:command}. - When customizing Lean4-Mode variables, make sure the customization takes place after loading the Lean4-Mode package so that the variables are correctly initialized first. For example, many Lean4-Mode hook @@ -182,6 +210,17 @@ before package loading, you should avoid it. Instead, put @samp{(add-hook 'lean4-...-hook #'...)} under the @samp{:config} section. (See @emph{Common Pitfalls} section below.) +Use-Package @uref{https://www.gnu.org/software/emacs/manual/html_node/use-package/Deferring-loading.html, involves} some complexity when it comes to deciding whether +to load a package eagerly (@emph{demand}) or lazily (@emph{defer}). For example, +it depends on your configuration (e.g. @code{use-package-always-defer}, +@code{use-package-always-demand}). Assuming you want Lean4-Mode to be +invoked as major mode when opening a Lean source file, the simplest +solution would be eager loading, e.g. via @samp{:demand t}. Alternatively, +you can defer loading e.g. via @samp{:defer t} together with +@samp{:mode "\\.lean\\'"} (which associates Lean4-Mode with the @samp{.lean} +file extension) and @samp{:commands lean4-mode} (which will set up +autoloading). + Following subsections show concrete examples. @menu @@ -193,8 +232,7 @@ Following subsections show concrete examples. @node Native @samp{vc} (Emacs 30 or later) @subsection Native @samp{:vc} (Emacs 30 or later) -GNU Emacs comes with @samp{use-package.el} built-in since version 29. And -since version 30, it also comes with a built-in @samp{:vc} keyword for the +Since version 30, Emacs comes with a built-in @samp{:vc} keyword for the @code{use-package} macro that utilizes @samp{package-vc.el} to install Emacs packages from remote source repositories. @@ -206,6 +244,7 @@ packages from remote source repositories. (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :vc ( :url "https://github.com/leanprover-community/lean4-mode.git" :rev :last-release ;; Or, if you prefer the bleeding edge version of Lean4-Mode: @@ -235,6 +274,7 @@ place the following code in your Emacs initialization file: @lisp (use-package lean4-mode :commands lean4-mode + :mode "\\.lean\\'" :straight (lean4-mode :type git :host github :repo "leanprover-community/lean4-mode" :files ("*.el" "data"))) From c380c1c2179c548d16755740e07112eb7e16c3d7 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:16:41 +0200 Subject: [PATCH 49/50] [readme] Elaborate on coexistence with Lean3-Mode --- README.org | 45 +++++++++++++++++++---- lean4-mode.info | 97 +++++++++++++++++++++++++++++++------------------ lean4-mode.texi | 54 ++++++++++++++++++++++----- 3 files changed, 142 insertions(+), 54 deletions(-) diff --git a/README.org b/README.org index 7e17824..7ef04aa 100644 --- a/README.org +++ b/README.org @@ -235,14 +235,43 @@ option accordingly. * Common Pitfalls -** Lean(3)-Mode - -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix =lean-= for its symbols. E.g. you should not use -=lean-=-prefixed commands in a buffer with Lean4-Mode as major mode. +** Coexistence with Lean3-Mode + +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]]. It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + +- Lean3-Mode uses =lean-= as prefix (e.g. for commands) whereas + Lean4-Mode uses =lean4-= as prefix. When Lean4-Mode is active, + you must not use commands with prefix =lean-=. + +- Both packages associate the =.lean= file extension with their + respective commands. Even more confusingly, they use different + functions and regular expressions to do so. + + Lean3-Mode: + #+begin_src elisp + ;;;###autoload + (push '("\\.lean$" . lean-mode) auto-mode-alist) + #+end_src + + Lean4-Mode: + #+begin_src elisp + ;;;###autoload + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) + #+end_src + + Make sure that both packages are loaded, autoloaded and configured + in such a way ~auto-mode-alist~ ends up with your desired value. + +- In particular, if you want Emacs to automatically detect whether + Lean3- or Lean4-Mode should be used for a particular file or + project, you'll need to define your own Elisp function and associate + it with the Lean file extension. If desired, you can even do this + directory locally (via the special "variable" =eval= in + =.dir-locals.el=). ** Partial value of ~lean4-mode-hook~ or other hook variables diff --git a/lean4-mode.info b/lean4-mode.info index 23928b3..4a0597b 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -56,7 +56,7 @@ Configuration Common Pitfalls -* Lean(3)-Mode:: +* Coexistence with Lean3-Mode:: * Partial value of lean4-mode-hook or other hook variables:: Changelog @@ -362,25 +362,50 @@ File: lean4-mode.info, Node: Common Pitfalls, Next: Changelog, Prev: Configur * Menu: -* Lean(3)-Mode:: +* Coexistence with Lean3-Mode:: * Partial value of lean4-mode-hook or other hook variables::  -File: lean4-mode.info, Node: Lean(3)-Mode, Next: Partial value of lean4-mode-hook or other hook variables, Up: Common Pitfalls +File: lean4-mode.info, Node: Coexistence with Lean3-Mode, Next: Partial value of lean4-mode-hook or other hook variables, Up: Common Pitfalls -4.1 Lean(3)-Mode -================ +4.1 Coexistence with Lean3-Mode +=============================== + +Lean4-Mode only supports version 4 of Lean. For editing code written in +deprecated version 3, use Lean3-Mode +(https://github.com/leanprover/lean3-mode). It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + + • Lean3-Mode uses ‘lean-’ as prefix (e.g. for commands) whereas + Lean4-Mode uses ‘lean4-’ as prefix. When Lean4-Mode is active, you + must not use commands with prefix ‘lean-’. + + • Both packages associate the ‘.lean’ file extension with their + respective commands. Even more confusingly, they use different + functions and regular expressions to do so. + + Lean3-Mode: + ;;;###autoload + (push '("\\.lean$" . lean-mode) auto-mode-alist) + + Lean4-Mode: + ;;;###autoload + (add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) + + Make sure that both packages are loaded, autoloaded and configured + in such a way ‘auto-mode-alist’ ends up with your desired value. -Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, -use Lean3-Mode (https://github.com/leanprover/lean3-mode), which is also -known as Lean-Mode due to historical reasons. In principle, it is fine -to have both Lean3-Mode and Lean4-Mode installed at the same time. But -note that Lean3-Mode uses the prefix ‘lean-’ for its symbols. E.g. you -should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as -major mode. + • In particular, if you want Emacs to automatically detect whether + Lean3- or Lean4-Mode should be used for a particular file or + project, you'll need to define your own Elisp function and + associate it with the Lean file extension. If desired, you can + even do this directory locally (via the special "variable" ‘eval’ + in ‘.dir-locals.el’).  -File: lean4-mode.info, Node: Partial value of lean4-mode-hook or other hook variables, Prev: Lean(3)-Mode, Up: Common Pitfalls +File: lean4-mode.info, Node: Partial value of lean4-mode-hook or other hook variables, Prev: Coexistence with Lean3-Mode, Up: Common Pitfalls 4.2 Partial value of ‘lean4-mode-hook’ or other hook variables ============================================================== @@ -533,29 +558,29 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro  Tag Table: Node: Top224 -Node: Installation1749 -Node: Brief Generic Instructions2040 -Node: Detailed Native Instructions3496 -Node: Instructions for Source-Based Use-Package5646 -Node: Native vc (Emacs 30 or later)7562 -Node: Doom package!8428 -Node: Straight8898 -Node: Usage9427 -Node: lsp-mode10849 -Node: Flycheck11134 -Node: Configuration11744 -Node: lsp-mode (1)11934 -Node: Flycheck (1)12203 -Node: Common Pitfalls12688 -Node: Lean(3)-Mode12912 -Node: Partial value of lean4-mode-hook or other hook variables13536 -Node: Changelog15242 -Node: Upcoming Version15682 -Node: Version 112 from 2024-12-1017748 -Node: Version 111 from 2024-12-0218613 -Node: Version 110 from 2024-12-0119020 -Node: Version 101 from 2024-11-2119518 -Node: Version 10 from 2024-11-1619881 +Node: Installation1764 +Node: Brief Generic Instructions2055 +Node: Detailed Native Instructions3511 +Node: Instructions for Source-Based Use-Package5661 +Node: Native vc (Emacs 30 or later)7577 +Node: Doom package!8443 +Node: Straight8913 +Node: Usage9442 +Node: lsp-mode10864 +Node: Flycheck11149 +Node: Configuration11759 +Node: lsp-mode (1)11949 +Node: Flycheck (1)12218 +Node: Common Pitfalls12703 +Node: Coexistence with Lean3-Mode12942 +Node: Partial value of lean4-mode-hook or other hook variables14664 +Node: Changelog16385 +Node: Upcoming Version16825 +Node: Version 112 from 2024-12-1018891 +Node: Version 111 from 2024-12-0219756 +Node: Version 110 from 2024-12-0120163 +Node: Version 101 from 2024-11-2120661 +Node: Version 10 from 2024-11-1621024  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 80e8bee..cd17454 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -65,7 +65,7 @@ Configuration Common Pitfalls -* Lean(3)-Mode:: +* Coexistence with Lean3-Mode:: * Partial value of @code{lean4-mode-hook} or other hook variables:: Changelog @@ -374,19 +374,53 @@ option accordingly. @chapter Common Pitfalls @menu -* Lean(3)-Mode:: +* Coexistence with Lean3-Mode:: * Partial value of @code{lean4-mode-hook} or other hook variables:: @end menu -@node Lean(3)-Mode -@section Lean(3)-Mode +@node Coexistence with Lean3-Mode +@section Coexistence with Lean3-Mode -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix @samp{lean-} for its symbols. E.g. you should not use -@samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode. +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}. It is possible for both +packages to be installed in parallel and used independently. But as a +user, it's your responsibility to set this up correctly. You need to +take care of following issues in particular: + +@itemize +@item +Lean3-Mode uses @samp{lean-} as prefix (e.g. for commands) whereas +Lean4-Mode uses @samp{lean4-} as prefix. When Lean4-Mode is active, +you must not use commands with prefix @samp{lean-}. + +@item +Both packages associate the @samp{.lean} file extension with their +respective commands. Even more confusingly, they use different +functions and regular expressions to do so. + +Lean3-Mode: +@lisp +;;;###autoload +(push '("\\.lean$" . lean-mode) auto-mode-alist) +@end lisp + +Lean4-Mode: +@lisp +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-select-mode)) +@end lisp + +Make sure that both packages are loaded, autoloaded and configured +in such a way @code{auto-mode-alist} ends up with your desired value. + +@item +In particular, if you want Emacs to automatically detect whether +Lean3- or Lean4-Mode should be used for a particular file or +project, you'll need to define your own Elisp function and associate +it with the Lean file extension. If desired, you can even do this +directory locally (via the special "variable" @samp{eval} in +@samp{.dir-locals.el}). +@end itemize @node Partial value of @code{lean4-mode-hook} or other hook variables @section Partial value of @code{lean4-mode-hook} or other hook variables From cca95cb5ab39a059c9ffc0e52f8b3655722d3265 Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:17:38 +0200 Subject: [PATCH 50/50] [readme] Contributing chapter on copyright bug-reference-mode --- README.org | 10 ++++++++ lean4-mode.info | 64 ++++++++++++++++++++++++++++++------------------- lean4-mode.texi | 12 ++++++++++ 3 files changed, 62 insertions(+), 24 deletions(-) diff --git a/README.org b/README.org index 7ef04aa..af9afa5 100644 --- a/README.org +++ b/README.org @@ -384,3 +384,13 @@ Features: ** Version 1.0 from 2024-11-16 - Specify "Version" in Emacs-Lisp library header. + +* Contributing + +When you contribute to Lean4-Mode, add a personal copyright like +=;; Copyright (c) 2024 Firstname Lastname= to the header of respective +files. + +You can use Emacs' built-in ~bug-reference-mode~ and +~bug-reference-prog-mode~ in this repository to make mentions of +issues like =#123= clickable. diff --git a/lean4-mode.info b/lean4-mode.info index 4a0597b..f327c07 100644 --- a/lean4-mode.info +++ b/lean4-mode.info @@ -29,6 +29,7 @@ channel on the Lean Zulip chat platform. * Configuration:: * Common Pitfalls:: * Changelog:: +* Contributing:: -- The Detailed Node Listing -- @@ -443,7 +444,7 @@ before calling ‘add-hook’, e.g. with ‘require’: (add-hook 'lean4-...-hook #'...))  -File: lean4-mode.info, Node: Changelog, Prev: Common Pitfalls, Up: Top +File: lean4-mode.info, Node: Changelog, Next: Contributing, Prev: Common Pitfalls, Up: Top 5 Changelog *********** @@ -554,33 +555,48 @@ File: lean4-mode.info, Node: Version 10 from 2024-11-16, Prev: Version 101 fro • Specify "Version" in Emacs-Lisp library header. + +File: lean4-mode.info, Node: Contributing, Prev: Changelog, Up: Top + +6 Contributing +************** + +When you contribute to Lean4-Mode, add a personal copyright like ‘;; +Copyright (c) 2024 Firstname Lastname’ to the header of respective +files. + + You can use Emacs' built-in ‘bug-reference-mode’ and +‘bug-reference-prog-mode’ in this repository to make mentions of issues +like ‘#123’ clickable. +  Tag Table: Node: Top224 -Node: Installation1764 -Node: Brief Generic Instructions2055 -Node: Detailed Native Instructions3511 -Node: Instructions for Source-Based Use-Package5661 -Node: Native vc (Emacs 30 or later)7577 -Node: Doom package!8443 -Node: Straight8913 -Node: Usage9442 -Node: lsp-mode10864 -Node: Flycheck11149 -Node: Configuration11759 -Node: lsp-mode (1)11949 -Node: Flycheck (1)12218 -Node: Common Pitfalls12703 -Node: Coexistence with Lean3-Mode12942 -Node: Partial value of lean4-mode-hook or other hook variables14664 -Node: Changelog16385 -Node: Upcoming Version16825 -Node: Version 112 from 2024-12-1018891 -Node: Version 111 from 2024-12-0219756 -Node: Version 110 from 2024-12-0120163 -Node: Version 101 from 2024-11-2120661 -Node: Version 10 from 2024-11-1621024 +Node: Installation1781 +Node: Brief Generic Instructions2072 +Node: Detailed Native Instructions3528 +Node: Instructions for Source-Based Use-Package5678 +Node: Native vc (Emacs 30 or later)7594 +Node: Doom package!8460 +Node: Straight8930 +Node: Usage9459 +Node: lsp-mode10881 +Node: Flycheck11166 +Node: Configuration11776 +Node: lsp-mode (1)11966 +Node: Flycheck (1)12235 +Node: Common Pitfalls12720 +Node: Coexistence with Lean3-Mode12959 +Node: Partial value of lean4-mode-hook or other hook variables14681 +Node: Changelog16402 +Node: Upcoming Version16863 +Node: Version 112 from 2024-12-1018929 +Node: Version 111 from 2024-12-0219794 +Node: Version 110 from 2024-12-0120201 +Node: Version 101 from 2024-11-2120699 +Node: Version 10 from 2024-11-1621062 +Node: Contributing21295  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index cd17454..00968f1 100644 --- a/lean4-mode.texi +++ b/lean4-mode.texi @@ -37,6 +37,7 @@ on the Lean Zulip chat platform. * Configuration:: * Common Pitfalls:: * Changelog:: +* Contributing:: @detailmenu --- The Detailed Node Listing --- @@ -583,4 +584,15 @@ Provide README as Texi and Info manual too. Specify "Version" in Emacs-Lisp library header. @end itemize +@node Contributing +@chapter Contributing + +When you contribute to Lean4-Mode, add a personal copyright like +@samp{;; Copyright (c) 2024 Firstname Lastname} to the header of respective +files. + +You can use Emacs' built-in @code{bug-reference-mode} and +@code{bug-reference-prog-mode} in this repository to make mentions of +issues like @samp{#123} clickable. + @bye