More detailed installation instructions for lean4-mode

Stream: new members

[Eduardo Ochs]

Hi all,

the installation instructions in git repository of lean-mode are too brief - they suppose that readers using an old Emacs28 without the new GPG key for ELPA know how to fetch the new key themselves, and that they are willing to restart Emacs several times fixing errors, following the recipes given in error messages...

I'm giving a kind-of-workshop for beginners - in Portuguese, using Emacs, and as beginner-friendly as possible - and after seeing their problems I prepared these more detailed installation instructions, and tested them with several versions of Emacs in an empty home directory with export HOME=/tmp/fake-home-dir:

;; Check the version of your Emacs:
;;   (emacs-version)
;;
;; If you're on emacs 29.1 or newer then the sexp with
;; `package-vc-install' below should work:
;;
(package-vc-install "https://github.com/leanprover-community/lean4-mode")

Otherwise, run this:

rm -Rfv  ~/.emacs.d/elpa/lean4-mode
mkdir -p ~/.emacs.d/elpa/lean4-mode
cd       ~/.emacs.d/elpa/lean4-mode
git clone https://github.com/leanprover-community/lean4-mode .

and run the sexp below, and add it to your ~/.emacs (obs: I'm not showing here my tricks for making this step easier for total beginners):

(add-to-list 'load-path "~/.emacs.d/elpa/lean4-mode")

After that, run this big progn:

(progn
  (add-to-list 'package-archives
    '("melpa" . "https://melpa.org/packages/"))
  ;;
  ;; See:
  ;; https://mail.gnu.org/archive/html/help-gnu-emacs/2024-05/msg00248.html
  (package-initialize)
  (setq package-check-signature nil)
  (package-refresh-contents)
  (package-install 'gnu-elpa-keyring-update)
  (setq package-check-signature t)
  ;;
  ;; See:
  ;; https://emacs.stackexchange.com/questions/80871/how-to-provide-updated-seq-package-to-magit
  (setq package-install-upgrade-built-in t)
  (package-install 'compat)
  (package-install 'seq)
  (progn (unload-feature 'seq t) (require 'seq))
  (package-install 'magit)
  ;;
  ;; Missing in the instructions for lean4-mode:
  (package-install 'company)
  ;;
  ;; From the instructions for lean4-mode:
  (package-install 'dash)
  (package-install 'flycheck)
  (package-install 'lsp-mode)
  (package-install 'magit-section)
  )

and try:

(require 'lean4-mode)

If that require returns lean4-mode, that's a good sign.

[Eduardo Ochs]

The main page of the workshop is here, but I would like to finish the material for the three lessons/meetings and debug it more thorough before announcing that link in more places...

[Eduardo Ochs]

Btw, how do I add an icon/emoji (:emacs:) after my name in my profile?

[Yury G. Kudryashov]

Please submit a PR to the repo!

[Yury G. Kudryashov]

I'm using NixOS and know nothing about issues with the new GPG key for ELPA.

[Eduardo Ochs]

Yury G. Kudryashov said:

Please submit a PR to the repo!

Done: https://github.com/leanprover-community/lean4-mode/issues/75

[Eduardo Ochs]

Sorry, my code above had an error - its (setq package-check-signature t) should be (setq package-check-signature 'allow-unsigned). The most up-to-date version of the progn can be found here:

http://anggtwu.net/eev-intros/find-lean4-intro.html#6