Zulip Chat Archive

Stream: new members

Topic: mathlib in emacs


Bob Bass (Sep 25 2022 at 22:06):

Hello, everyone!
My first post.
While I have not yet started working with Lean in earnest, I appear to have Lean 3 working on emacs 27.1 with lean-mode and I would prefer not to use vscode.
Would you please help me get mathlib set up so that I can work through the book?
I'm using Lubuntu 22.04 on a PC laptop.
Thanks in advance.

Johan Commelin (Sep 26 2022 at 05:22):

@Bob Bass How did you install everything? Because the installation instructions on leanprover-community.github.io should give you working projects out of the box. Do you have leanproject installed? Also: which book are you talking about?

Bob Bass (Oct 01 2022 at 21:45):

@Johan Commelin Hi, Johan!
Sorry I didn't stick around long enough to catch your reply.
I've reformulated my question here: post


Last updated: Dec 20 2023 at 11:08 UTC