More detailed installation instructions

[edrx]

The current installation instructions in the git repository are too brief - they suppose that users using old versions of Emacs28 know how to fix the "no public key" problem, and they suppose that people don't mind restarting Emacs several times fixing errors, following the recipes given in error messages...

I'm giving a workshop for beginners who have very little experience with Emacs, and I had to prepare installation instructions that fix these problems, and test them with several versions of Emacs. They are here:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/More.20detailed.20installation.20instructions.20for.20lean4-mode

Cheers!

[t-c-acc]

I agree.

Also, having instructions for straight.el is too much. I think whoever uses straight.el already knows how to add a package from github, and getting into straight.el just for one package is too complicated, and unnecessary since package-vc is in newer versions of Emacs.

I'd also like to note that from Emacs 30, vc-use-package will be included in Emacs, and one will be able to just add a :vc keyword to a use-package declaration.

[edrx]

Sorry, my suggestion below 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

[urkud]

Could you please open a PR with specific edits you suggest?

[edrx]

I'd rather not, because I don't know how to adapt what I did to the style that you are using in the README... for example(s): I don't know if you really want to support versions of Emacs28 that were not patched with the new GPG key, I don't know if you would like to keep the link to my page about fixing the problem with the GPG key - this one: http://anggtwu.net/2024-no-public-key.html - and AFAIK the style that I used, in which the sexps can be either executed one by one as a series of (mostly) one-liners or executed in a single progn, is very unusual... and worse, some friends of mine tested those instructions on Linuxes, but they haven't been tested on MacOS yet...

Shouldn't we start by discussing how to test these new instructions?...

[mekeor]

As far as I can tell, this issue can be condensed to the consideration if the following configurations should be added in the READMEs installation instructions:

(package-install 'gnu-elpa-keyring-update)
(setq package-install-upgrade-built-in t)

I'll look into this. I rename the ticket accordingly.

The following configuration is already default, so we can assume that people who changed it know what they are doing; i.e. we don't need to add the following line to our installation instructions:

(setq package-check-signature 'allow-unsigned)

[mekeor]

I'm closing this issue because it's not specific to Lean4-Mode.

If anyone provides a PR along an explanation under which circumstances (package-install 'gnu-elpa-keyring-update) (setq package-install-upgrade-built-in t) is needed, we can happily add it to a Troubleshooting section under the Installation chapter.