Setting up library on Emacs

Stream: general

[Pradana Aumars]

Hi, I'm learning Lean in a course I'm taking and the professor provides us the course's Lean library but as a collections of .lean files, instead of packaging properly, since it's supposed to be used with the VSCode binary that he also provides. I use Emacs so when I copy-and-paste the .lean files onto my own working directory, it doesn't import correctly. Does anyone have experience with using a library on Emacs?

[Kevin Buzzard]

Just to be sure -- is this Lean 3 or Lean 4, and are you using mathlib? Finally, if you let me use the standard VS Code (and had all the Lean files) do you think I would be able to get it up and running, or is there some more trickery going on?

[Patrick Massot]

The modified VSCode is almost unmodified, it's simply VSCodium for licence reasons (you are not allowed to distribute VSCode with Microsoft branding, and VSCodium has the added bonus of being telemetry-free) and it comes with a very slightly modified Lean extension (adding syntax highlighting for my custom verbose tactics). None of this has anything to do with importing files. If emacs cannot find files it mean it's not finding the leanpkg.path file. I don't know how the emacs lean-mode searches for this file, or actually how it searches for the lean executable.

[Patrick Massot]

I should add you are creating artificial difficulties by using emacs since the Lean support in emacs is way below the support in VSCode (no tactic state widgets).

[Jannis Limperg]

Packaging information is stored in the leanpkg.toml file. If you've installed elan, you should have a leanpkg binary on the PATH. Then run leanpkg configure in the directory where leanpkg.toml is stored. This should set up leanpkg.path and install the correct Lean version. At this point Emacs' lean-modeshould pick everything up.

[Patrick Massot]

If lean-mode needs the toml file then you can create a file leanpkg.toml inside the exos folder with content

[package]
name = "mdd154"
version = "0.1"
lean_version = "leanprover-community/lean:3.24.0"
path = ".."

[dependencies]
mathlib = {path="../mathlib"}

But again using emacs is a very bad idea.