Using Mathlib in emacs (no vscode allowed!)

Stream: new members

[Bob Bass]

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?
Thanks!

[Jason Rute]

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]

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]

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