installing for linux and emacs, single user

Stream: Berkeley Lean Seminar

[Kyle Miller]

I just went through figuring out how to get a basic setup for linux and emacs. In case it's helpful for others (or in case someone can tell me what I should have done), here's what I did.

First install elan:

$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

I chose N for "set path" because I like modifying my startup scripts myself. The script puts everything into ~/.elan/. If you use zsh, then add this to your .zshenv:

source ~/.elan/env

Then

$ pip3 install --user mathlibtools

In emacs, do M-x package-list-packages and install lean-mode and helm-lean. You do this by navigating to each entry and pressing i, then pressing x to execute the installation.

You might need to M-x customize-variable lean-rootdir. Set it to "~/.elan/" (with quotes).

Now when you open a .lean file in emacs, it should be all set, though I haven't tested much out yet beyond opening a couple files and proving a theorem.

Helm lets you do C-c C-d to look up definitions. M-. finds the definition for the symbol at the point. C-c C-b shows boxes for things like #check. C-c C-g opens up the goal window.

[K Y]

How does helm-lean compare to company-lean in terms of usability? I have been using company-lean (for no reason).

[Kyle Miller]

I've been using helm-lean (for no reason), so I can't really compare. Have you had any desynchronization issues with lean-mode? It seems sometimes the errors aren't correct, especially when using the calc tactic (though thankfully you can get the current goals inside curly brackets of by { ... } most of the time).

[Kentarô YAMAMOTO]

I believe the desynchronization issue for me manifests itself as inability to complete stuff by company-lean; I get something like error (interrupted). Doing C-c C-r and being patient usually fix the problem.