From e777ee89dee65b7faae0f72796fb0ec40c219fdb Mon Sep 17 00:00:00 2001 From: Mekeor Melire Date: Fri, 6 Dec 2024 11:07:59 +0100 Subject: [PATCH] README: Rephrase introduction; resurrect Contributing chapter --- README.org | 37 ++++++++++------- lean4-mode.el | 4 +- lean4-mode.info | 105 +++++++++++++++++++++++++++--------------------- lean4-mode.texi | 39 +++++++++++------- 4 files changed, 107 insertions(+), 78 deletions(-) diff --git a/README.org b/README.org index 750a0f7..c68a893 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 Lean language -This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by providing a major mode for editing -code written in version 4 of the programming language and theorem -prover [[https://lean-lang.org][Lean]]. +This package extends [[https://www.gnu.org/software/emacs/][GNU Emacs]] by a major mode for [[https://lean-lang.org][Lean]] version 4, a +programming language and theorem prover. -The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues -tracked there too. Further discussions and question-answering takes -place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat. - -For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (also known -as /Lean-Mode/). +Lean4-Mode is developed on [[https://github.com/leanprover-community/lean4-mode][Github]]. Bugs and feature requests are also +tracked there. Further discussions take place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs]] channel +on the Lean Zulip chat platform. * Installation @@ -194,12 +190,23 @@ option accordingly. * Common Pitfalls -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix =lean-= for its symbols. E.g. you should not use -=lean-=-prefixed commands in a buffer with Lean4-Mode as major mode. +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use [[https://github.com/leanprover/lean3-mode][Lean3-Mode]], which is also known as +/Lean-Mode/ due to historical reasons. In principle, it is fine to +have both Lean3-Mode and Lean4-Mode installed at the same time. But +note that Lean3-Mode uses the prefix =lean-= for its symbols. Make +sure to not use these =lean-=-prefixed commands in buffers where +Lean4-Mode is the major mode. + +* Contributing + +When you contribute to Lean4-Mode, add a personal copyright like =;; +Copyright (c) 2024 Firstname Lastname= to the header of respective +files. + +You can use Emacs' built-in ~bug-reference-mode~ and +~bug-reference-prog-mode~ in this repository to make mentions of +issues like =#123= clickable. * Changelog diff --git a/lean4-mode.el b/lean4-mode.el index 4883eb0..e300343 100644 --- a/lean4-mode.el +++ b/lean4-mode.el @@ -36,8 +36,8 @@ ;; Provides highlighting, diagnostics, goal visualization, ;; and many other useful features for Lean users. -;; See the README.md for more advanced features and the -;; associated keybindings. +;; For more information, see the README.org which is also provided as +;; Info manual. ;;; Code: diff --git a/lean4-mode.info b/lean4-mode.info index 4936b87..8e4254d 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: @@ -32,6 +28,7 @@ Lean's Zulip chat. * Usage:: * Configuration:: * Common Pitfalls:: +* Contributing:: * Changelog:: -- The Detailed Node Listing -- @@ -309,23 +306,38 @@ installed, then customize the ‘lsp-diagnostics-provider’ user option accordingly.  -File: lean4-mode.info, Node: Common Pitfalls, Next: Changelog, Prev: Configuration, Up: Top +File: lean4-mode.info, Node: Common Pitfalls, Next: Contributing, Prev: Configuration, Up: Top 4 Common Pitfalls ***************** -Lean4-Mode only supports version 4 of Lean. For editing Lean version 3, -use Lean3-Mode (https://github.com/leanprover/lean3-mode), which is also -known as Lean-Mode due to historical reasons. In principle, it is fine -to have both Lean3-Mode and Lean4-Mode installed at the same time. But -note that Lean3-Mode uses the prefix ‘lean-’ for its symbols. E.g. you -should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as -major mode. +Lean4-Mode only supports version 4 of Lean. For editing code written in +deprecated version 3, use Lean3-Mode +(https://github.com/leanprover/lean3-mode), which is also known as +_Lean-Mode_ due to historical reasons. In principle, it is fine to have +both Lean3-Mode and Lean4-Mode installed at the same time. But note +that Lean3-Mode uses the prefix ‘lean-’ for its symbols. Make sure to +not use these ‘lean-’-prefixed commands in buffers where Lean4-Mode is +the major mode. + + +File: lean4-mode.info, Node: Contributing, Next: Changelog, Prev: Common Pitfalls, Up: Top + +5 Contributing +************** + +When you contribute to Lean4-Mode, add a personal copyright like ‘;; +Copyright (c) 2024 Firstname Lastname’ to the header of respective +files. + + You can use Emacs' built-in ‘bug-reference-mode’ and +‘bug-reference-prog-mode’ in this repository to make mentions of issues +like ‘#123’ clickable.  -File: lean4-mode.info, Node: Changelog, Prev: Common Pitfalls, Up: Top +File: lean4-mode.info, Node: Changelog, Prev: Contributing, Up: Top -5 Changelog +6 Changelog *********** * Menu: @@ -339,7 +351,7 @@ File: lean4-mode.info, Node: Changelog, Prev: Common Pitfalls, Up: Top  File: lean4-mode.info, Node: Development, Next: Version 111, Up: Changelog -5.1 Development +6.1 Development =============== • Fix occasional error message "The connected server(s) does not @@ -353,7 +365,7 @@ File: lean4-mode.info, Node: Development, Next: Version 111, Up: Changelog  File: lean4-mode.info, Node: Version 111, Next: Version 110, Prev: Development, Up: Changelog -5.2 Version 1.1.1 +6.2 Version 1.1.1 ================= • Assign all customizable user-options to the Lean4-Mode specific @@ -363,7 +375,7 @@ File: lean4-mode.info, Node: Version 111, Next: Version 110, Prev: Developmen  File: lean4-mode.info, Node: Version 110, Next: Version 101, Prev: Version 111, Up: Changelog -5.3 Version 1.1.0 +6.3 Version 1.1.0 ================= • To ‘lean4’ customization group, add link to local info manual and @@ -375,7 +387,7 @@ File: lean4-mode.info, Node: Version 110, Next: Version 101, Prev: Version 11  File: lean4-mode.info, Node: Version 101, Next: Version 10, Prev: Version 110, Up: Changelog -5.4 Version 1.0.1 +6.4 Version 1.0.1 ================= • Specify Yury G. Kudryashov as maintainer. @@ -385,7 +397,7 @@ File: lean4-mode.info, Node: Version 101, Next: Version 10, Prev: Version 110  File: lean4-mode.info, Node: Version 10, Prev: Version 101, Up: Changelog -5.5 Version 1.0 +6.5 Version 1.0 =============== • Specify "Version" in Emacs-Lisp library header. @@ -394,26 +406,27 @@ File: lean4-mode.info, Node: Version 10, Prev: Version 101, Up: Changelog  Tag Table: Node: Top223 -Node: Installation1589 -Node: Brief and Generic Instructions1832 -Node: Detailed and Concrete Instructions2781 -Node: Instructions for Source-Based Use-Package4438 -Node: Native vc (Emacs 30 or later)5159 -Node: Doom-Emacs6067 -Node: Straight6493 -Node: Usage6993 -Node: lsp-mode8439 -Node: Flycheck8724 -Node: Configuration9334 -Node: lsp-mode (1)9524 -Node: Flycheck (1)9793 -Node: Common Pitfalls10278 -Node: Changelog10870 -Node: Development11115 -Node: Version 11111696 -Node: Version 11012023 -Node: Version 10112441 -Node: Version 1012724 +Node: Installation1423 +Node: Brief and Generic Instructions1666 +Node: Detailed and Concrete Instructions2615 +Node: Instructions for Source-Based Use-Package4272 +Node: Native vc (Emacs 30 or later)4993 +Node: Doom-Emacs5901 +Node: Straight6327 +Node: Usage6827 +Node: lsp-mode8273 +Node: Flycheck8558 +Node: Configuration9168 +Node: lsp-mode (1)9358 +Node: Flycheck (1)9627 +Node: Common Pitfalls10112 +Node: Contributing10737 +Node: Changelog11178 +Node: Development11420 +Node: Version 11112001 +Node: Version 11012328 +Node: Version 10112746 +Node: Version 1013029  End Tag Table diff --git a/lean4-mode.texi b/lean4-mode.texi index 679a5a1..dea8e82 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 @@ -40,6 +36,7 @@ as @emph{Lean-Mode}). * Usage:: * Configuration:: * Common Pitfalls:: +* Contributing:: * Changelog:: @detailmenu @@ -319,12 +316,24 @@ option accordingly. @node Common Pitfalls @chapter Common Pitfalls -Lean4-Mode only supports version 4 of Lean. For editing Lean version -3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as Lean-Mode due to historical -reasons. In principle, it is fine to have both Lean3-Mode and -Lean4-Mode installed at the same time. But note that Lean3-Mode uses -the prefix @samp{lean-} for its symbols. E.g. you should not use -@samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode. +Lean4-Mode only supports version 4 of Lean. For editing code written +in deprecated version 3, use @uref{https://github.com/leanprover/lean3-mode, Lean3-Mode}, which is also known as +@emph{Lean-Mode} due to historical reasons. In principle, it is fine to +have both Lean3-Mode and Lean4-Mode installed at the same time. But +note that Lean3-Mode uses the prefix @samp{lean-} for its symbols. Make +sure to not use these @samp{lean-}-prefixed commands in buffers where +Lean4-Mode is the major mode. + +@node Contributing +@chapter Contributing + +When you contribute to Lean4-Mode, add a personal copyright like @samp{;; +Copyright (c) 2024 Firstname Lastname} to the header of respective +files. + +You can use Emacs' built-in @code{bug-reference-mode} and +@code{bug-reference-prog-mode} in this repository to make mentions of +issues like @samp{#123} clickable. @node Changelog @chapter Changelog