It’s been a while since I’ve blogged, and today seemed like a good day to plant some new seeds.  Recently, I’ve been trying to move away from VS Code and decided to go back to an old Linux staple: Emacs. 

It’s a relatively new machine, so I took notes along the way in hopes it might be helpful to someone else.  Most of this is based off the official installation instructions available here: https://github.com/leanprover-community/lean4-mode

I originally tried to use the Emacs for Windows installation, but I found it hard to configure that way and ended up using the Windows Subsystem for Linux instead.  I choose to go with a Debian install because that’s what I’m familiar with.  To start, you need to enable Windows Subsystem for Linux.

Open start menu, and search for “features”.  Click on “Turn Windows features on or off”.  Scroll down until you find the folder for “Windows Subsystem for Linux” and click the check box, followed by the “OK” button.  You should then be able to install Debian through WSL via the official Windows Store.

I also recommend pinning it to the taskbar.  Click the start button, type “debian” in the search bar, right click, “Pin to Taskbar”.  

You’ll also need to create a user account. Record your password in a safe location as you will need it for the following “sudo” commands to install the prerequisite software.

Install git:

sudo apt install git

Install curl:

sudo apt install curl

Install emacs:

sudo apt install emacs

Finally, we install “elan”,  our Lean 4 engine.  From your Debian console:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Type 1[Enter] to proceed

Source ~/.elan/env

Run “lake –version” to check that it installed correctly.

Launch emacs

emacs

Within Emacs, use the following to open your initialization file:

C-x C-f ~/.emacs.d/init.el

Copy (from whatever you’re reading this with) and Paste (C-y) in the following:

(require 'package)

(add-to-list 'package-archives

             '("melpa" . "https://melpa.org/packages/"))

(add-to-list 'package-selected-packages 'dash)

(add-to-list 'package-selected-packages 'lsp-mode)

(add-to-list 'package-selected-packages 'magit-section)

(package-refresh-contents)

(package-install-selected-packages 'no-confirm)

Save with C-x C-s, then exit with C-x C-c, then run emacs again to update.  I recommend you read through the tutorials if it’s your first time, then exit once you’re done.

Clone the lean4 mode from github

git clone https://github.com/leanprover-community/lean4-mode.git ~/lean4-mode

emacs ~/.emacs.d/init.el

At the bottom add:

(add-to-list 'load-path "~/lean4-mode")

Save with C-x C-s

Add emacs to taskbar:

At this point “Emacs (Client) (Debian)” showed up in my start menu.  Right click and “Pin to Taskbar”

The LEAN4 engine doesn’t load properly this way,  so Shift-Right click and select “Properties”. 

Change “emacsclient” to “emacs” and delete the “–alternate-editor=   –create-frame” part and so the semicolon directly follows “emacs”.

Click the new shortcut to test it out.  Now’s also a pretty good time to check out the tutorial if you’re a new Emacs user.  I still need to work out the double icons, so I’ll keep you posted…

My next step was to create a test Lean 4 Project. From your home in Debian (~/):

lake new Lean4TestProject

cd Lean4TestProject

lake build

Hopefully this should complete successfully! Now we double check:

emacs Main.lean

The first time I ran this, I get a whole bunch of warnings . They looked something like this:

⛔ Warning (lsp-mode): Unknown request method: workspace/inlayHint/refresh

Click one, and select “Yes, ignore `lsp-mode` warnings completely.”  If I find a better option, I’ll let you know.

Add a line with the text “#check id” between “import Lean4TestProject” and “def main : IO Unit :=”.

Click “Lean 4” in the menu and then “Execute Lean”.  It will prompt for an argument, so just hit Enter.  If everything so far has gone well, you’ll see something like the following:

-*- mode: compilation; default-directory: "~/Lean4TestProject/" -*-

Compilation started at Tue Apr 14 20:00:02

/home/ryan/.elan/bin/lake env /home/ryan/.elan/bin/lean  /home/ryan/Lean4TestProject/Main.lean

id.{u} {α : Sort u} (a : α) : α

Compilation finished at Tue Apr 14 20:00:02, duration 0.22 s

Close emacs to get back to the console. Change back to your home directory as needed.

cd ~

Download “Mathematics in Lean 4”:

git clone https://github.com/leanprover-community/mathematics_in_lean.git

cd mathematics_in_lean

emacs .

Opens emacs with a directory listing. Navigate to the MIL folder. You may want to read through the files in the C01_Introduction subdirectory, but the fun stuff really starts in C02_Basics with “S01_Calculating.lean”.  The first example is as follows:

example (a b c : ℝ) : a * b * c = b * (a * c) := by

  rw [mul_comm a b]

  rw [mul_assoc b a c]

This example provides a simple multiplication proof.  It applies the commutative property on “a” to get “b * a * c”, and the associative property

Turn on the Lean4 display with C-c TAB.  You should get a new pane with the following text:

Messages below:

9:0:

declaration uses ‘sorry’

12:0:

declaration uses ‘sorry’

22:0:

declaration uses ‘sorry’
…

Our first error is the ‘sorry’ declaration on line 9.  Notice how “example” is underlined in the other pane.  Left click it and watch the other pane update. 

The error should read as follows:

Expected type:

⊢ ∀ (a b c : ℝ), c * b * a = b * (a * c)

…

This is our first puzzle to solve!  How to we get from “c * b * a” to “b * (a * c)”?  

Scroll further for spoilers…

I’d start with the commutative property.  Replace the “sorry” with “rw [mul_comm c b]” and see what happens.  Note that this command is order sensitive!

Notice that the pane above now reads as follows:

Messages here:

9:49:

unsolved goals

a b c : ℝ

⊢ b * c * a = b * (a * c)

…

Well, how do we get from “b * c * a” to “b * (a * c)”? 

The associative property again!

Try adding a new line below with “rw [mul_assoc b c a]”.  Our unsolved goals should update again to the following:

a b c : ℝ

⊢ b * (c * a) = b * (a * c)

There’s one last step.  Can you figure it out on your own?  

Scroll down for the solution.

The last step is to apply the commutative property again, but this time between “c” and “a”.  Add the following to complete the proof: “rw [mul_comm c a]”.

If you’ve done this correctly, you should see a “goals accomplished” when selecting the last line of the proof.  The next error should be line ~14 with the next “sorry”.  See how far you can get from there!