Zulip Chat Archive

Stream: general

Topic: trying to use lean via emacs


view this post on Zulip 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?

thanks

Jeremy

view this post on Zulip Yury G. Kudryashov (Jul 16 2019 at 05:37):

Do you have melpa?

view this post on Zulip Yury G. Kudryashov (Jul 16 2019 at 05:38):

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

view this post on Zulip Yury G. Kudryashov (Jul 16 2019 at 05:38):

lean-mode is one of them.

view this post on Zulip Jesse Michael Han (Jul 16 2019 at 11:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jul 16 2019 at 13:35):

I have

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

view this post on Zulip jeremy (Jul 16 2019 at 13:51):

Hi,

I created the file .emacs.d/init.el as indicated at
https://github.com/leanprover/lean-mode
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/"))
(package-initialize)

;; 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.

Cheers,

Jeremy

view this post on Zulip 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?

view this post on Zulip Jesse Michael Han (Jul 16 2019 at 13:57):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jesse Michael Han (Jul 16 2019 at 14:39):

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

view this post on Zulip 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

view this post on Zulip Jesse Michael Han (Jul 16 2019 at 15:35):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 18 2019 at 07:29):

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

view this post on Zulip Johan Commelin (Jul 18 2019 at 07:29):

Otherwise I really recommend giving VS Code a shot.

view this post on Zulip 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

view this post on Zulip jeremy (Jul 30 2019 at 04:50):

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

view this post on Zulip jeremy (Jul 30 2019 at 04:52):

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


Last updated: May 08 2021 at 10:12 UTC