emacs instructions on download page

[avigad]

It seems to me that the instructions on the download page should tell users that they have to set up emacs, and it should provide guidance for doing that.

I can think of a few options.

(1) We can link to the instructions here:

https://github.com/leanprover/lean/blob/master/src/emacs/README.md

(2) We can make a copy of that file in leanprover.github.io.

(3) We can cut and paste parts of that file into the download instructions on leanprover.github.io.

(4) The download instructions on leanprover.github.io can tell users where to find the README file on their computer, once Lean has been installed.

If you tell me which option you think is best, I will be happy to make these changes. If it is (4), please tell me what directory contains the lean folder after the installations on the various systems.

Also, even though there is a github ribbon in the corner, it wouldn't hurt to mention the github repository as a download option.

[leodemoura]

I completely agree.

BTW, we have a leanemacs command in the Ubuntu and Windows versions. When we use this command, we don't have to configure Emacs. Everything is automatic. We just have to execute

sudo apt-get install emacs24
sudo add-apt-repository ppa:leanprover/lean
sudo apt-get update
sudo apt-get install lean

Then, we execute leanemacs, and Lean and Emacs start without any additional configuration. I tried it on a blank Ubuntu VM, and it worked smoothly.

[avigad]

O.k., unless Soonho has another preference, I will use option (1). It is easiest, and we don't have to maintain another file. Under the Windows and Ubuntu instructions, I will also explain the leanemacs option.

[soonhokong]

O.k., unless Soonho has another preference, I will use option (1). It is easiest, and we don't have to maintain another file. Under the Windows and Ubuntu instructions, I will also explain the leanemacs option.

I have no problem with option (1).

There are just a few extra step for Ubuntu-12.04 where you can only find emacs23 (we need emacs24):

sudo add-apt-repository ppa:ubuntu-elisp/ppa
sudo apt-get update
sudo apt-get install emacs-snapshot

[leodemoura]

I updated the Download page. I added instructions for downloading Emacs 24 on Ubuntu 14.04 and Ubuntu 12.04. I also described leanemacs.

Later today, I will play with the OSX version, and add instructions for this version

[avigad]

Oh, good. I was editing the files at the same time, but your revisions are better!

On Sun, Feb 1, 2015 at 3:22 PM, Leonardo de Moura notifications@github.com wrote:

I updated the Download page. I added instructions for downloading Emacs 24 on Ubuntu 14.04 and Ubuntu 12.04. I also described leanemacs.

Later today, I will play with the OSX version, and add instructions for this version

— Reply to this email directly or view it on GitHub https://github.com/leanprover/leanprover.github.io/issues/26#issuecomment-72382209 .

[avigad]

It looks like we forgot to close this.