From 02f40c795296f55d9edf45a4c2752f44d9398c0b Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Tue, 15 Jul 2025 00:10:35 +0200 Subject: [PATCH 1/9] [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 2/9] [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 3/9] [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 4/9] [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 5/9] [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 6/9] [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 7/9] [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 8/9] [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 9/9] [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'."