Merge pull request #86 from leanprover-community/milestone-01-repair-…

…status-quo

Fixes all issues listed in Milestone 1: https://github.com/leanprover-community/lean4-mode/milestone/1: Fixes #74. Fixes #78. Fixes #79. Fixes #80.

.github/workflows/melpazoid.yml

@@ -10,10 +10,11 @@ jobs:
   build:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v2
-    - name: Set up Python 3.9
-      uses: actions/setup-python@v1
-      with: { python-version: 3.9 }
+    - uses: actions/checkout@v3
+    - name: Set up Python 3.10
+      uses: actions/setup-python@v4
+      with:
+        python-version: '3.10'
     - name: Install
       run: |
         python -m pip install --upgrade pip

CHANGELOG.org

@@ -0,0 +1,14 @@
+#+title: Lean4-Mode - Changelog
+#+language: en
+
+* Development
+
+* Version 1.0.1
+
+- Specify Yury G. Kudryashov as maintainer.
+- Rework README.  (Now in Org format).
+- Provide README as Texi and Info manual too.
+
+* Version 1.0
+
+- Specify "Version" in Emacs-Lisp library header.

Makefile

@@ -0,0 +1,10 @@
+# GNU- and NonGNU-Elpa accept Org files as package documentation but
+# Melpa does not.  As long as Lean4-Mode is not distributed on GNU- or
+# NonGNU-Elpa, it should ship with .texi and .info manuals.  This
+# depends on: GNU Emacs, Make and GNU Texinfo.
+
+lean4-mode.info lean4-mode.texi: README.org
+	emacs --batch \
+		"--eval=(require 'ox-texinfo)" \
+		'--eval=(find-file "$<")' \
+		'--eval=(org-texinfo-export-to-info)'

README.org

@@ -0,0 +1,170 @@
+#+title: Lean4-Mode - Emacs major-mode for Lean language
+#+language: en
+#+export_file_name: lean4-mode.texi
+#+texinfo_dir_category: Emacs misc features
+#+texinfo_dir_title: Lean4-Mode: (lean4-mode).
+#+texinfo_dir_desc: Emacs major-mode for Lean language
+
+This package extends GNU Emacs by providing a major-mode for editing
+code written in version 4 of the programming language and theorem
+prover Lean.
+
+The Lean4-Mode source code is developed at [[https://github.com/leanprover-community/lean4-mode][Github]] and its issues
+tracked there too.  Further discussions and question-answering takes
+place in the [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs][#Emacs channel]] of Lean's Zulip chat.
+
+For legacy version 3 of Lean, use the archived [[https://github.com/leanprover/lean3-mode][Lean3-Mode]] (formerly
+known as /Lean-Mode/).
+
+* Installation
+
+** Brief and Generic Instructions
+
+Install dependencies:
+- [[https://lean-lang.org/lean4/doc/setup.html][Lean version 4]]
+- Emacs version 27 or later
+- Emacs packages [[https://github.com/magnars/dash.el][Dash]] (which is available on GNU-Elpa
+  package-archive), [[https://www.flycheck.org][Flycheck]], [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]], and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (which are
+  available on Melpa package-archive)
+
+Install Lean4-Mode:
+- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]].
+- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to that local
+  repository to the ~load-path~ list and
+- load Lean4-Mode with =(require 'lean4-mode)=.
+
+** Detailed and Concrete Instructions
+
+Install Lean version 4.
+
+Install Emacs version 27 or later.
+
+Install the Emacs packages Dash, Flycheck, lsp-mode and Magit-Section.
+Dash is the only one of these packages that is available in the
+default [[https://elpa.gnu.org][GNU Elpa]] package-archive.  You can install the remaining three
+packages either from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive.  For later
+approach, add the following to your Emacs initialization file
+(e.g. =~/.emacs.d/init.el=):
+
+#+begin_src elisp
+(require 'package)
+(add-to-list 'package-archives
+             '("melpa" . "https://melpa.org/packages/"))
+(package-initialize)
+(let ((need-to-refresh t))
+  (dolist (package '(dash flycheck lsp-mode magit-section))
+    (unless (package-installed-p package)
+      (when need-to-refresh
+        (package-refresh-contents)
+        (setq need-to-refresh nil))
+      (package-install package))))
+#+end_src
+
+Clone the Git repository of Lean4-Mode:
+
+#+begin_src shell
+git clone https://github.com/leanprover-community/lean4-mode.git /path/to/lean4-mode
+#+end_src
+
+In your Emacs initialization file, add the path to your local
+Lean4-Mode repository to the ~load-path~ list and load Lean4-Mode:
+#+begin_src elisp
+(add-to-list 'load-path "/path/to/lean4-mode")
+(require 'lean4-mode)
+#+end_src
+
+** Instructions for Source-Based Use-Package
+
+If you use a source-based package-manager (e.g. =package-vc.el=,
+Straight or Elpaca), then make sure to list the ="data"= directory in
+your Lean4-Mode package recipe.
+
+If you use the ~use-package~ macro and intent to defer loading of
+packages in order to improve your Emacs startup time, then make sure
+to specify ~lean4-mode~ as a =:command=.
+
+Following subsections show concrete examples.
+
+*** Native =:vc= (Emacs 30 or later)
+
+GNU Emacs comes with =use-package.el= built-in since version 29.  And
+since version 30, it also comes with a built-in =:vc= keyword for the
+~use-package~ macro that utilizes =package-vc.el= to install Emacs
+packages from remote source repositories.
+
+#+begin_src elisp
+;; Use Melpa as package archive:
+(require 'package)
+(add-to-list 'package-archives
+             '("melpa" . "https://melpa.org/packages/"))
+(package-initialize)
+
+;; Install Lean4-Mode:
+(use-package lean4-mode
+  :commands lean4-mode
+  :vc (:url "https://github.com/leanprover-community/lean4-mode.git"
+       :rev :newest))
+#+end_src
+
+*** Doom-Emacs
+
+If you use Doom-Emacs, you can place the following code in your Doom
+initialization file:
+
+#+begin_src elisp
+(package! lean4-mode :recipe
+  (:host github
+   :repo "leanprover/lean4-mode"
+   :files ("*.el" "data")))
+#+end_src
+
+*** Straight
+
+If you use the Straight package manager through Use-Package, then
+place the following code in your Emacs initialization file:
+
+#+begin_src elisp
+(use-package lean4-mode
+  :commands lean4-mode
+  :straight (lean4-mode :type git :host github
+                        :repo "leanprover/lean4-mode"
+                        :files ("*.el" "data")))
+#+end_src
+
+* Usage
+
+If things are working correctly, you should see the word "Lean 4" in
+Emacs mode-line when you open a file with =.lean= extension.  Emacs
+will ask you to identify the /project/ this file belongs to.  If you
+then type =#check id=, the word =#check= will be underlined, and
+hovering over it will show you the type of ~id~.  The mode-line will
+show =FlyC:0/1=, indicating that there are no errors and one piece of
+information displayed.
+
+To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=).  This
+will display the =*Lean Goals*= buffer (like the Lean Info-View pane
+in VS-Code) in a separate window.
+
+If you want breadcrumbs of namespaces and sections to be shown in the
+header-line, set the user option ~lsp-headerline-breadcrumb-enable~ to
+~t~.
+
+* Key Bindings and Commands
+
+| Key                    | Description                                            | Command                           |
+|------------------------+--------------------------------------------------------+-----------------------------------|
+| =C-c C-k=              | Echo the keystroke needed to input the symbol at point | ~quail-show-key~                  |
+| =C-c C-d=              | Recompile and reload imports                           | ~lean4-refresh-file-dependencies~ |
+| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode                       | ~lean4-std-exe~                   |
+| =C-c C-p C-l=          | Builds package with lake                               | ~lean4-lake-build~                |
+| =C-c C-i=              | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~        |
+|------------------------+--------------------------------------------------------+-----------------------------------|
+| =C-c ! n=              | Flycheck: Go to next error                             | ~flycheck-next-error~             |
+| =C-c ! p=              | Flycheck: Go to previous error                         | ~flycheck-previous-error~         |
+
+For key bindings from ~lsp-mode~, see [[https://emacs-lsp.github.io/lsp-mode/page/keybindings/][its respective documentation]] and
+note that not all capabilities are supported by Lean4-Mode.
+
+In the default configuration, the Flycheck annotation =FlyC:N/M=
+indicates the number of errors (~N~) and responses (~M~) from Lean;
+clicking on =FlyC= opens the Flycheck menu.

lean4-mode.el

@@ -7,12 +7,13 @@
 ;;         Soonho Kong       <[email protected]>
 ;;         Gabriel Ebner     <[email protected]>
 ;;         Sebastian Ullrich <[email protected]>
-;; Maintainer: Sebastian Ullrich <[email protected]>
+;; Maintainer: Yury G. Kudryashov <[email protected]>
 ;; Created: Jan 09, 2014
 ;; Keywords: languages
 ;; Package-Requires: ((emacs "27.1") (dash "2.18.0") (flycheck "30") (magit-section "2.90.1") (lsp-mode "8.0.0"))
 ;; URL: https://github.com/leanprover/lean4-mode
 ;; SPDX-License-Identifier: Apache-2.0
+;; Version: 1.0.1
 
 ;;; License: