HTTP in lean4-mode installation docs

Stream: new members

[Isak Colboubrani]

The lean4-mode install documentation suggests adding (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/")) to init.el. Is the use of HTTP (instead of HTTPS) intentional?

[Isak Colboubrani]

Perhaps signature checking is done out-of-band in some way, thus reducing the need for HTTPS, that is, there is no risk of code injection via MITM attacks. @Sebastian Ullrich, do you happen to know?