2. Milestone: Internal Cleanup

[mekeor]

This PR fixes all issues under milestone 2 - internal cleanup. It aims to clean up some internals while avoiding breaking changes.

Each commit solves a specific problem. The PR can be best reviewed by reviewing each commit on its own.

[urkud]

Could you please also fix the long lines warnings from melpazoid?

[mekeor]

@urkud, are you referring to this?:

The ;;; Commentary for this file is much wider than 80 characters

Let's take a look at each of these:

---

lean4-eri.el with melpazoid:

- The `;;; Commentary` for this file is much wider than 80 characters

This refers to this URL in the commentary: https://github.com/agda/agda/blob/b40c6fc2e0ced7b547553654f81e5898082d700c/src/data/emacs-mode/eri.el. But I'd prefer to keep it as is.

---

lean4-info.el with byte-compile using Emacs 29.4:

lean4-info.el:75:2: Warning: docstring wider than 80 characters

Fixed in a new commit: 89a1b29

---

lean4-input.el with melpazoid:

- The `;;; Commentary` for this file is much wider than 80 characters

This refers to the URL https://github.com/agda/agda/blob/d2cbd2dd4f49fa84c5ca6fcf464c3211adcc0088/src/data/emacs-mode/agda-input.el in the commentary which I'd also like to keep as is.

[mekeor]

Generally, I dislike Melpazoid. It's implemented in Python and has too many false-negatives. Its author themself admits this too. We may look for an alternative some time in future.

[mekeor]

I was mistaken. This...:

⸺ lean4-info.el with byte-compile using Emacs 29.4:

lean4-info.el:75:2: Warning: docstring wider than 80 characters

... has not been fixed by one of my commits. Instead, it is referring to this...:

(eval-when-compile
  (lsp-interface
    (lean:PlainGoal (:goals) nil)
    (lean:PlainTermGoal (:goal) nil)
    (lean:Diagnostic (:range :fullRange :message) (:code :relatedInformation :severity :source :tags))))

which expands to a very long Elisp code including this definition that Melpazoid may be warning about due to a too wide docstring:

(cl-defun lsp-make-lean-diagnostic (&rest plist &key code? related-information? severity? source? tags? range full-range message &allow-other-keys) (ignore code? related-information? severity? source? tags? range full-range message) "Constructs lean:Diagnostic from `plist.'
Allowed params: (:message :full-range :range :tags? :source? :severity? :related-information? :code?)"
  ;; ...
  )

Long story short, this is an issue in lsp-mode because they are the developers of the lsp-interface macro.