Zulip Chat Archive

Stream: new members

Topic: Using Mathlib in emacs (no vscode allowed!)

Bob Bass (Oct 01 2022 at 20:13):

Hello, all.
Trying this question again.
So I have Lean 3.4.2 running in emacs lean-mode on a PC laptop in Lubunut 22.04 and I am working through the book Logic and Proof.
I would also like to be able to work through the book Mathematics in Lean using the Mathlib library.
I have downloaded the TryLean binary and it works, but I don't want to run vscode or vscodium if I can avoid doing so.
Is there any way that I can just tell emacs to use the Mathlib library from the TryLean download? Or maybe just copy the Mathlib library files to someplace where emacs lean-mode can see them?

Jason Rute (Oct 01 2022 at 21:58):

Lean 3.4.2 is really old. Even if you get it working, it will require a really old version of Mathlib. Is this what you want? (Lean 3 was forked and taken over by the Lean community. The current version is Lean 3.48c.)

Jason Rute (Oct 01 2022 at 22:08):

Looking at https://leanprover-community.github.io/mathematics_in_lean/01_Introduction.html I think you only need to do the following (none of these steps use vs code):

  • Make sure you have elan installed (so you can get whatever version of Lean you need)
  • Make sure you have mathlibtools tools installed
  • Use leanproject as follows: leanproject get mathematics_in_lean to make a project directory with the right version of lean and mathlib
  • Open that newly created directory in emacs.

Jason Rute (Oct 01 2022 at 22:09):

(I don't use emacs, windows, or mathematics in lean, so your mileage may vary with my directions. :smile: )

Last updated: Dec 20 2023 at 11:08 UTC