README: Add preamble. Rework Installation section.

README.org

@@ -1,88 +1,98 @@
 #+title: ~lean4-mode~ - An Emacs major-mode for the Lean language
 
+This package extends GNU Emacs by providing a major-mode for editing
+code written in version 4 of the programming language and theorem
+prover Lean.
+
 * Installation
 
-Before using this major mode, you need to [[https://leanprover.github.io/lean4/doc/setup.html#basic-setup][install Lean 4]].
+** Briefly
 
-To use ~lean4-mode~ in Emacs, add the following to your =init.el=:
-#+begin_src elisp
-;; You need to modify the following line
-(setq load-path (cons "/path/to/lean4-mode" load-path))
+Install dependencies:
+- [[https://lean-lang.org/lean4/doc/setup.html][Lean version 4]]
+- Emacs version 27 or later
+- Emacs packages [[https://github.com/magnars/dash.el][Dash]], [[https://www.flycheck.org][Flycheck]], [[https://emacs-lsp.github.io/lsp-mode][lsp-mode]] and [[https://github.com/magit/magit/blob/main/lisp/magit-section.el][Magit-Section]] (which are
+  available on the Melpa package-archive)
+
+Install Lean4-Mode:
+- Clone the [[https://github.com/leanprover-community/lean4-mode][Git repository of Lean4-Mode]].
+- In your [[https://www.gnu.org/software/emacs/manual/html_node/emacs/Init-File.html][Emacs initialization file]], add the path to that local
+  repository to the ~load-path~ list and
+- load Lean4-Mode with =(require 'lean4-mode)=.
 
-(setq lean4-mode-required-packages '(dash flycheck lsp-mode magit-section))
+** Detailed
 
+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 on the
+default [[https://elpa.gnu.org][GNU Elpa]] package-archive.  You can install the remaining three
+packages either from source or from [[https://melpa.org/#/getting-started][Melpa]] package-archive.  For later
+approach, add the following to your Emacs initialization file
+(e.g. =~/.emacs.d/init.el=):
+#+begin_src elisp
 (require 'package)
-(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))
+(add-to-list 'package-archives
+             '("melpa" . "https://melpa.org/packages/"))
 (package-initialize)
 (let ((need-to-refresh t))
-  (dolist (p lean4-mode-required-packages)
-    (when (not (package-installed-p p))
+  (dolist (package '(dash flycheck lsp-mode magit-section))
+    (unless (package-installed-p package)
       (when need-to-refresh
         (package-refresh-contents)
         (setq need-to-refresh nil))
-      (package-install p))))
-
-(require 'lean4-mode)
+      (package-install package))))
 #+end_src
 
-Alternatively if you are a fan of ~use-package~ and =straight.el= you
-can use:
-#+begin_src elisp
-(use-package lean4-mode
-  :straight (lean4-mode
-	     :type git
-	     :host github
-	     :repo "leanprover/lean4-mode"
-	     :files ("*.el" "data"))
-  ;; to defer loading the package until required
-  :commands (lean4-mode))
+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
 
-If you are a doom-emacs user, adding the following to =packages.el=
-should work:
+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
-(package! lean4-mode :recipe
-  (:host github
-   :repo "leanprover/lean4-mode"
-   :files ("*.el" "data")))
+(add-to-list 'load-path "/path/to/lean4-mode")
+(require 'lean4-mode)
 #+end_src
 
 * Trying It Out
 
 If things are working correctly, you should see the word "Lean 4" in
-the Emacs mode line when you open a file with extension =.lean=.
-Emacs will ask you to identify the "project" this file belongs to.  If
-you then type
+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
 #+begin_src lean
 #check id
 #+end_src
 the word =#check= will be underlined, and hovering over it will show
-you the type of ~id~.  The mode line will show =FlyC:0/1=, indicating
+you the type of ~id~.  The mode-line will show =FlyC:0/1=, indicating
 that there are no errors and one piece of information displayed.
 
 To view the proof state, run ~lean4-toggle-info~ (=C-c C-i=).  This
-will show the =*Lean Goals*= buffer (like the =Lean infoview= pane in
-VSCode) in a separate window.
+will display the =*Lean Goals*= buffer (like the =Lean infoview= pane
+in VS-Code) in a separate window.
 
 * Settings
 
 Set these with e.g. =M-x customize-variable=.
-
 - ~lsp-headerline-breadcrumb-enable~: Show a "breadcrumb bar" of
-  namespaces and sections surrounding the current location (default:
-  off)
+  namespaces and sections surrounding the current location. Defaults
+  to /off/.
 
 * Key Bindings and Commands
 
 | Key           | Function                                                                        |
 |---------------+---------------------------------------------------------------------------------|
-| =C-c C-k=     | show the keystroke needed to input the symbol under the cursor                  |
-| =C-c C-d=     | recompile & reload imports (~lean4-refresh-file-dependencies~)                  |
-| =C-c C-x=     | execute Lean in stand-alone mode (~lean4-std-exe~)                              |
-| =C-c C-p C-l= | builds package with lake (~lean4-lake-build~)                                   |
-| =C-c C-i=     | toggle info view showing goals and errors at point (~lean4-toggle-info-buffer~) |
-| =C-c ! n=     | flycheck: go to next error                                                      |
-| =C-c ! p=     | flycheck: go to previous error                                                  |
+| =C-c C-k=     | Show the keystroke needed to input the symbol under the cursor                  |
+| =C-c C-d=     | Recompile & reload imports (~lean4-refresh-file-dependencies~)                  |
+| =C-c C-x=     | Execute Lean in stand-alone mode (~lean4-std-exe~)                              |
+| =C-c C-p C-l= | Builds package with lake (~lean4-lake-build~)                                   |
+| =C-c C-i=     | Toggle info view showing goals and errors at point (~lean4-toggle-info-buffer~) |
+| =C-c ! n=     | Flycheck: go to next error                                                      |
+| =C-c ! p=     | Flycheck: go to previous error                                                  |
 
 For ~lsp-mode~ bindings, see
 https://emacs-lsp.github.io/lsp-mode/page/keybindings/ (not all