Zulip Chat Archive

Stream: general

Topic: trying to use lean via emacs

jeremy (Jul 16 2019 at 05:16):

I've tried to start using Lean using emacs, but I get to a point where,
following https://github.com/leanprover/lean-mode
I try to install package lean-mode, but with

M-x package-install and then entering lean-mode, it says [No match]

I've also looked at https://melpa.org/#/getting-started and tried
to run M-x package-refresh-contents - again it said [No match]
but trying it again it said Contacting host: elpa.gnu.org:80
and then nothing happened for a long time.

I tried M-x package-list-packages - it produced a buffer with what
appears to be a long list of packages, not including lean-mode

What is supposed to happen when I try these things? How do I
trouble-shoot this situation?



Yury G. Kudryashov (Jul 16 2019 at 05:37):

Do you have melpa?

Yury G. Kudryashov (Jul 16 2019 at 05:38):

http://melpa.org/ has a large collection of emacs packages not included in elpa.

Yury G. Kudryashov (Jul 16 2019 at 05:38):

lean-mode is one of them.

Jesse Michael Han (Jul 16 2019 at 11:58):

you should additionally see melpa being contacted when you're doing the refresh

Jesse Michael Han (Jul 16 2019 at 11:59):

there's some line you put in your init file to ensure melpa is queried for packages

Yury G. Kudryashov (Jul 16 2019 at 12:03):

@jeremy I think, we can't provide more information without looking at melpa related parts of your Emacs init file

Kevin Buzzard (Jul 16 2019 at 12:56):

@jeremy is there a reason that you are persevering with emacs rather than using VS Code? VS Code has far better support on this chat.

Jesse Michael Han (Jul 16 2019 at 13:01):

there's some line you put in your init file to ensure melpa is queried for packages

you should ensure that something like following is loaded in your init file:

(require 'package)
(add-to-list 'package-archives
         '("melpa" . "http://melpa.org/packages/"))

melpa is queried separately from elpa

Yury G. Kudryashov (Jul 16 2019 at 13:35):

I have

(require 'package)
(add-to-list 'package-archives
             '("melpa" . "https://melpa.org/packages/") t)

jeremy (Jul 16 2019 at 13:51):


I created the file .emacs.d/init.el as indicated at
and it's as follows

[jeremy@hp2017 ~]$ cat .emacs.d/init.el

;; see https://github.com/leanprover/lean-mode
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/"))

;; Trigger completion on Shift-Space
(global-set-key (kbd "S-SPC") #'company-complete)

I tried to use emacs because I've some slight familiarity with it (I had to use it for a bit around 30 years ago), whereas I've never used VSCode. Also it's installed on the system I use at work.



Yury G. Kudryashov (Jul 16 2019 at 13:57):

Try C-h v package-archives. Does it show melpa?
BTW, did you run "Refresh package list" in list-packages?

Jesse Michael Han (Jul 16 2019 at 13:57):

that should work to install lean-mode. did you load the new init file?

jeremy (Jul 16 2019 at 14:19):

C-h v package-archives gives the result
package-archives is a variable defined in ‘package.el’.
Its value is (("melpa" . "http://melpa.org/packages/")
("gnu" . "http://elpa.gnu.org/packages/"))
so I guess that means yes.
No, I didn't run "Refresh package list" in list-packages
(i've no idea how to do that, but I could try it if you can tell me how to do it)

jeremy (Jul 16 2019 at 14:21):

I didn't do anything deliberate to load the new init file, I assumed that would happen automatically when I start emacs. And I would say that must have happened, otherwise wouldn't the process know nothing about melpa.

Jesse Michael Han (Jul 16 2019 at 14:21):

i think he means, try using list-packages first, then do package-refresh-contents once in the packages buffer

jeremy (Jul 16 2019 at 14:25):

OK, well I've done that - it doesn't seem to make any difference. What should I see when I do that?

Jesse Michael Han (Jul 16 2019 at 14:36):

you should see the minibuffer say "contacting melpa" for a few seconds, and then your package list should be refreshed with melpa packages

Jesse Michael Han (Jul 16 2019 at 14:39):

it might be a network issue if your elpa query timed out

jeremy (Jul 16 2019 at 14:49):

Well I do see something about contacting melpa. But the package list still doesn't have lean-mode

Jesse Michael Han (Jul 16 2019 at 15:35):

does the rest of the package list get updated with new entries from melpa?

Jesse Michael Han (Jul 16 2019 at 15:37):

if it's just lean-mode you need, it might be feasible to just install it from source to your ~/.emacs.d/elpa

jeremy (Jul 18 2019 at 01:33):

well, the package list doesn't change. But from the machine here, at work, I don't see anything about contacting melpa, either. All I see is a message about contacting elpa.gnu.org:80, then nothing, for a long time, so I hit C-g to get out of that.

How do I just install it from source to your ~/.emacs.d/elpa - ie, what do I put, exactly where?

Jesse Michael Han (Jul 18 2019 at 01:39):

1. go to MELPA website and search for lean-mode
2. download the tar file from the lean-mode page on MELPA
3. the tar file contains a folder called lean-mode-20180906...
4. move this folder into ~/.emacs.d/elpa (or wherever your Emacs installs its packages to)
5. require lean-mode from your init file

jeremy (Jul 18 2019 at 07:26):

Thanks - as a matter of fact there is a lean expert and emacs expert who was
able to set it up on my computer here.
Contrary to the instructions I had found, the init.el file had to be put into the
directory ~/.xemacs, not ~/.emacs.d
But looking at what he has done, it seems 3. and 4. have been done
I can't find anything that resembles
"5. require lean-mode from your init file",
what does that mean exactly?

Johan Commelin (Jul 18 2019 at 07:29):

@jeremy Were you already using emacs before starting on Lean?

Johan Commelin (Jul 18 2019 at 07:29):

Otherwise I really recommend giving VS Code a shot.

Jesse Michael Han (Jul 18 2019 at 15:27):

oh, you're using XEmacs

"require lean-mode from your init file" means putting the line

(require 'lean-mode)

in your init file. it should succeed silently if your Emacs can find lean-mode among its packages. if it can't, it will fail and complain that it doesn't know what lean-mode is. you can test it by highlighting it and using M-x eval-region.

strictly speaking, this doesn't seem to be necessary to get lean-mode to work if it is already installed, but it will helpfully give you an error message on startup if lean-mode isn't actually installed

jeremy (Jul 30 2019 at 04:50):

I'd used it occasionally, a long time ago.

jeremy (Jul 30 2019 at 04:52):

well, no particular reason - except that it was already installed on the computer

Last updated: Dec 20 2023 at 11:08 UTC