Milestone 3: Breaking Refactor

[mekeor]

Changelog

Let's first set up the Changelog so that later commits can keep it updated.

• Incorporate changelog into readme/manual.

Delete obsolete code

First of all, we delete code, so that we don't waste time fixing obsolete code.

Following files were already independently deleted by Yury on the master branch:

• -debug
• -dev

Features and other code:

• Abbrev table
• Tool-bar menu entry for Flycheck
• Feature of whitespace cleanup before save
• Feature of automatic version detection, and related code
• Note that we do not delete lean4-input-export-translations and lean4-input-export-translations-to-stdout function definitions from -input file because it'd be a waste of time as later milestones/PRs will reimplement -input. See: Rework Abbreviations for Input Method #93.)

And, at least temporarily:

• Delete -util and -lake files in favor of a minimalist approach for locating the lake and lean binaries as well as the project root (Remove lean4-lake.el in favor of Emacs built-in compile command #90, Refactor lake find dir #100)

Separate concerns

We separate concerns, i.e. we move definitions of functions and variables as well as other code to those files where they belong, so that we don't keep stumbling upon our own feet but rather have a nice and tidy code base, in particular for later PRs.

Delete -settings file after moving following out of it:

• Keybindings to -mode
• Move -show-file-progress to -fringe
• Move -highlight-inaccessible-names to -info
• Move customization group and mode hook to -mode

Move following code out of -mode file:

• Definition of -tab-indent to -eri
• Input related code to -input
• Addition to markdown-code-lang-modes to new -markdown
• lsp-mode related code to new -lsp
• Evaluate if moving Flycheck related code to new -flycheck makes sense. No, it doesn't.

Rename variables and functions such that they use the prefix of the file
where they are defined:

• -lsp
• -input
• -eri
• -info

Note that we do not rename -info file to -lsp-info, even though Lean4 Info currently only works for lsp-mode, as we hope that it might perhaps eventually also work with Eglot.

Minor mode lean4-info-mode

• Define minor mode lean4-info-mode

Minor mode lean4-lsp-mode

We separate logic relating Lean4-Mode to lsp-mode into a new minor mode. This lays the ground for later PRs that'd provide alternative minor modes for using alternative LSP clients, like Eglot.

• Define minor mode lean4-lsp-mode
• Move all lsp-mode specific keybindings to lean4-lsp-mode-map

Refactor Lean4-Mode

• Replace lean4-hooks-alist with entries in lean4-mode-hook
• Replace lean4-mode-setup with entries in lean4-mode-hook
• Tidy up lean4-mode definition by using setq-local and with entries in lean4-mode-hook

Globally consistent patterns

We consistently implement repository-wide code patterns and conventions. We do so near the end of the PR in order to reduce chances for merge conflicts when reordering commits within this PR's branch.

Consistently use Lean4 name across project:

• In description in first line of Emacs-Lisp files (prop-line)
• In docstrings
• As symbol of customization group
• As name of input method, if existent

Other:

• Style of URLs in code comments
• Order of require (1. built-ins, 2. third-party, 3. local)
• Style of copyright statement
• Capitalization of "This file is NOT part of GNU Emacs"

Improve documentation and formalia

• Improve phrasing of code comments
• Improve Emacs-Lisp file commentary sections
• Reformat Package-Requires library header. Won't do this because of incompatibility with Melpazoid.
• Fix errors reported by Melpazoid

In readme/manual:

• Improve introduction
• Explain pitfall with lean4-mode-hook (Document the pitfall of modifying lean4-mode-hook before Lean4-Mode has been loaded #101)
• Fix installation instructions regarding autoloading. Suggest to either eagerly load lean4-mode and describe how to explicitly autoload. (lean4-mode is not automatically activated by .lean files using README instructions #103)
• Explain pitfall with Lean3-Mode (lean-mode)
• Resurrect a section on Contributing