`lean4-mode` is not automatically activated by `.lean` files using README instructions

[scuellar]

The installation instructions currently state:

In your Emacs initialization file, add the path to your local Lean4-Mode repository to the load-path list:

(add-to-list 'load-path "~/path/to/lean4-mode")
Lean4-Mode should now already be enabled when you open a file with .lean extension.

However, following these instructions alone does not result in .lean files being opened with lean4-mode. With only the load-path added, .lean files open in fundamental-mode.

To achieve the expected behavior, it is necessary to explicitly associate the file extension and autoload the mode:

(autoload 'lean4-mode "lean4-mode" "Major mode for Lean 4." t)
(add-to-list 'auto-mode-alist '("\\.lean\\'" . lean4-mode))

The README does include the following statement:

...But you can optionally also already load Lean4-Mode on Emacs startup, e.g. in order to customize variables:
(require 'lean4-mode)

However, this is described as optional and does not imply that it is required for automatic mode activation.

[mekeor]

Thanks for reporting.

I was falsely assuming that Emacs would somehow automatically obey all autoload-cookies in all Elisp files that are inside any directory that is listed in load-path.

I think it's best to correct the readme and instruct users to just (require 'lean4-mode).

(Alternatively, users could perhaps update their autoload-file, and load the regenerated autoload-file.)

(Alternatively, Lean4-Mode could provide a lean4-autoloads.el file as part of its repository which users could load/require. This is a maintenance burden though, especially since the file will be generated by the distributing package-archive (probably Melpa) in future anyway.)

[mekeor]

We should probably also add :mode "\\.lean\\'" to our (use-package ...) forms in readme. It works without, for me, but there might be other cases.

[mekeor]

Rust-Mode has these instructions for manual installation:

(add-to-list 'load-path "/path/to/rust-mode/")
(autoload 'rust-mode "rust-mode" nil t)
(add-to-list 'auto-mode-alist '("\\.rs\\'" . rust-mode))

[mekeor]

Haskell-Mode follows another approach. For installing it from Git, you run some Make command that generates the -autoloads file which you are supposed to require in your init.el:

make EMACS=/path/to/your/emacs

and then adding the following command to your .emacs:

(add-to-list 'load-path "~/lib/emacs/haskell-mode/")
(require 'haskell-mode-autoloads)
(add-to-list 'Info-default-directory-list "~/lib/emacs/haskell-mode/")