No errors.

Glasgow.

Before I start, a word on Glasgow. I am really disappointed that I will not be going to the Postgraduate Combinatorial Conference 2020 up there in April. Bhavik Mehta and I were going to run a one-day workshop on Lean. We told the students to warm up by playing the natural number game, we were going to do some simple graph theory stuff, and then Bhavik was going to show off his Combinatorics in Lean repo, where he proves, amongst other things, the Kruskal-Katona theorem. Bhavik is now working with a team in Cambridge on topos theory in Lean. As Mario once said — when I was complaining about breaking changes being made in mathlib — “you can’t stop progress”.

I went to Glasgow to speak at a very enjoyable BMC in 2001. I thought the indie record shops were great too. I had plans to go there twice in the near future — once to the PCC, and once to the joint BMC/BAMC meeting, where I was going to speak about Lean; of course this has also been postponed. I very much hope to get back to Glasgow in the near future — it’s been too long.

The other reason I am disappointed was that I was really looking forward to see how a room full of intelligent mathematics PhD students would react when asked to fill in a sorry with essentially no Lean training other than the natural number game, and then how much further we could see them go over the weeks beyond. I was very interested in watching them learn. I find it more interesting watching people learning in real life rather than in a chatroom. Maybe I should do more stuff in my Discord Lean server?

I have been thinking about teaching in general, and talking to learners who I meet on the Zulip Chat like Shing Tak Lam, who had mathematics and computer science A-level exams scheduled for May and is now faced with months off school. Shing decided they would try doing a question from one of the past STEP exams in Lean, and they’ve managed to do it! I think it is very interesting that they have, very early on, noticed our brand spanking new documentation — many many thanks to Rob Lewis and all the others involved in making it happen. It is opening doors for newcomers.

But let me get to the point: a tip for beginners who want to know why their code doesn’t work.

No errors

A few months ago I isolated what I think is a basic principle in teaching Lean to people — it’s the concept that when you’re working on your code, you should try to keep it from having any errors. If you are stuck on something, then you might well have an error in your code. But in this case you should have just one error, and you should be able to fix this error with one sorry. Errors are bad. Aim for no errors.

How do you know if you have no errors? Say you have just finished writing a tactic mode proof in Visual Studio Code or on CoCalc, and you are about to enjoy the buzz which goes with solving another level of the Lean maths game. Just before you do, I think you should just check that there are no errors anywhere in the file you are working on.

That picture of the bottom left hand corner of my VS Code window (it’s a level in the group theory game which I am designing) has a “tick” by the word “Lean”, meaning “I finished compiling and there are no orange bars”. There is also an x in a circle, and a 0 by it — “no errors”. If there are no errors, then you are winning. If there are no errors and also no warnings, you have won. In Cocalc just look at the All Messages window and it’s the same thing — look for a tick at the top, and then check for red errors.

Sometimes I see students whose file is absolutely full of errors. Their file is 400 lines long, getting really slow, and has 23 errors. They ask me why something doesn’t work, and I know from experience that the answer might be of the form “because something you wrote 100 lines up which caused an error and means that things aren’t the way you think they are”. Some people can get into a real state. They’re in a tactic mode proof and Lean is simply not printing the tactic state, or they have an error which just says sync. This post is to just cover some of the basic problems which I’ve seen people have, and how one might attempt to solve them.

The right way to proceed when you have a file with 23 errors is to click on this icon in VS Code

Opening the Lean Messages window in VS Code

to get the “Lean Messages” window. In CoCalc this is called the “All Messages” window and you don’t need to click anything — it should already be there. In this window you will be able to see all the errors and warnings in your code. In the online Lean web editor the icon you want is the same but they are in the top right. The warnings are in orange, the errors are in red. Let’s try and tidy up this output.

• Some of the “warnings” might just be debugging output — output of #check commands for example. Why not just comment those out or delete them? If you want to know the output of a #check command, why not just paste it as a comment in your code like this?

/- trying to figure out how to use insert.

#check @set.insert

set.insert : Π {α : Type u_1}, α → set α → set α

-/

• Maybe some code is just old and doesn’t work and you don’t want to think about it right now. Just comment it all out with /- ... -/ or move it to another file. This might be a good time to think about whether the file you’re working on has a good name. Too many files called things like scratch73.lean or test1.lean is not a great way to organise your work in a project. Are you proving lots of theorems about groups? Why not call the file groupstuff.lean and move all of the non-group stuff to somewhere else?

• Locate your first error. That’s the one we’re going to work on. If you’re in the middle of a proof and you don’t know how to continue — don’t leave it as an error. Say sorry. Get rid of all the errors you’re not interested in, until we find the first error which you do not understand. That’s the error we should be working on. If it’s not the one you want to work on — comment it out. If your code breaks when you comment it out, we might have just located the actual problem.

When you have located the first error, let’s take a look at what it is. Sometimes with beginners I see errors like invalid expression or sync (although sync is not usually the first error). These are errors which say that the structure of your tactic proof is messed up. A tactic proof is supposed to be a sequence of tactics separated by commas. A comma-separated sequence of tactics within a { } block is considered as one tactic. Two very common mistakes: to forget the tactic (“Why doesn’t mul_comm work?” “Because you have to use the rewrite tactic: write rw mul_comm “) or to forget the comma (which usually causes no end of confusion because Lean then thinks that the name of the next tactic is an input to the tactic before and there is probably no variable called apply). As a general hint: if you have invalid expression under a } then there is probably no { and you might want to delete it. In general if you have an invalid expression, try getting rid of it. Try adding a } or a , or an end to see if they’re valid expressions. See if you can make the expression valid. If there are unsolved goals, try sorry. If there are lots of goals, try { sorry }, — that might get rid of the first one, and if it’s the one you’re interested in then try working within those brackets. Try and tame the situation. You know that you can use #exit to completely abort Lean just after your first error? I had an error in a Lean file today and I just wanted to make 100% sure that it was isolated away from everything else, so I wrote this (and it took a little time to figure it out):

  ,sorry

  ,},sorry end #exit

I was in the middle of a tactic mode proof. After the sorry (which changed the error into a warning), I then figured out from experimenting and looking at errors that Lean wanted some combination of commas, sorrys and an end, and then I got out with #exit and all of a sudden compilation time shot down. I can now work on this error properly.

Once you just have one error, if you’re in tactic mode, you can now try and solve it. Safe in tactic mode you can switch back to info view in VS Code or the online web editor using this symbol

How to switch to info view in VS Code

(or just look at the window called “Info at cursor” on CoCalc) and you should be able to see the tactic state and any error messages which you generate.

The error won’t go away

If you simply cannot understand the error message, or if you understand the error but don’t know what to do about it, then ask on #new members. Change the error into a sorry, so that the code now compiles with no errors, and post all the code including all import statements — all the code up to and including the problem — to the chat and also quote the exact error. If an expert sees all your code and your error message then they might be able to solve it while they’re on their phone without even firing up Lean. I am really bad at second-guessing what people mean — they are talking about something so they obviously assume that we all know they have imported some file or other — but I don’t know my way around parts of the mathlib library at all. Please post working code when you are asking about errors. If I can’t cut and paste it and reproduce your issue — I am far less likely to open my mouth and try to say something helpful.

I learnt very on in my Lean career that it was really important to learn to read error messages. Errors are bad. Error messages is like losing life in Zelda. If you are on no errors, you are on 100% health. Aim for no errors. If there are no errors in your file — are there errors in your project? An error-free project is a healthy project. Aim to keep your projects free of errors, but feel free to litter them with sorrys. The perfectoid project was always full of sorrys while it was in development. We started by writing the definition of a perfectoid space and we sorried a part of it, and that sorry was there from the start. But whenever we pushed code, we did our best to ensure that it did not contain any errors.

If your code is too long, too amateurish, not remotely at mathlib standard, or runs on Lean 3.3.0 and the mathlib you happen to have on your computer — that is absolutely fine by me. If the goal was to fill in a sorry, and the sorry is gone, and there are no warnings and no errors, then you beat the level and you get the credit. Over on the Lean chat there are level-creators and level-solvers. I myself like to do both (current levels: commutative algebra related to the Nullstellensatz), but if you’re a beginner wanting to get into Lean, then you can start by finding some other levels out there in the wild, like these ones on CoCalc and all the ones which are thrown up every day by people asking questions on the Lean chat. Can’t go to school? Try solving some exam questions in Lean! Aim for no errors!