trying to use lean via emacs

Stream: general

[jeremy]

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

[Yury G. Kudryashov]

Do you have melpa?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

lean-mode is one of them.

[Jesse Michael Han]

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

[Jesse Michael Han]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

@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]

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]

I have

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

[jeremy]

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

[Yury G. Kudryashov]

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

[Jesse Michael Han]

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

[jeremy]

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]

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]

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

[jeremy]

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]

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]

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

[jeremy]

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

[Jesse Michael Han]

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

[Jesse Michael Han]

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

[jeremy]

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]

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]

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]

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

[Johan Commelin]

Otherwise I really recommend giving VS Code a shot.

[Jesse Michael Han]

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]

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

[jeremy]

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