search

leanprover / leanprover.github.io

www
https://lean-lang.org/
15 stars 24 forks source link

help user find information on configuring emacs #38

Open avigad opened 8 years ago

avigad commented 8 years ago

Yesterday I had a problem with the unicode fonts, and I fixed it following the instructions in the Emacs mode README file. (I installed emacs-unicode-fonts.) But to do this I had to (1) remember that Soonho once told us about this, and (2) look for the README. Users with the same problem may be more frustrated.

Two possible solutions:

(1) On leanprover.github.io, add a more prominent link to the Emacs README file, under "Download". For example, at the bottom of the page, we can write:

Once Lean is installed, you can start the Emacs with Lean mode using the command leanemacs. For information on how to configure Emacs yourself and install unicode-friendly fonts, see [here].

(2) On the Documentation page, we can start a FAQ. This could go in a "troubleshooting" section. We could do this, for example, by changing the header "Forum" to "Additional Information", with entries:

o You are welcome to join the [Lean user forum] on Google Groups. o There is also a list of [Frequently Asked Questions].

@leodemoura @soonhokong ? I will be happy to make either or both of these changes. (I am not sure how to set up a new page for the FAQ, but I can probably figure it out.)

soonhokong commented 8 years ago

I like both of them.

(I am not sure how to set up a new page for the FAQ, but I can probably figure it out.)

You can create a new file (i.e. documentation/FAQ.md) and write things there. Then, you can make a link from documentation/index.md such as [FAQ](FAQ.html).

avigad commented 8 years ago

I just added a sentence about Emacs and issued a pull request. I am still working on a FAQ.