Bad Apple but it's Lean Tactics

Lean is a modern programming language that happens to also be a proof assistant. It’s also the best programming language of all time.

Kublai: No it’s not! You haven’t even convinced any of your friends to try Lean, much less convince them that it’s the best!

OK, uh, good point. I guess “the Ali’s Uyghur Kitchen of programming” is not a very convincing sales pitch to most people. One friend asked me for any examples of Lean programs that actually do real¹ stuff, and sure there’s Verso and lean4-raytracer and of course Lean itself, but they don’t really grab people’s attentions.

Alright, I’ll give a serious reason. One thing that Lean surprisingly excels at is the editor experience. It’s like an interactive Jupyter notebook and the infoview displays a lot of useful real-time information about types and tactic states. Oh, and #eval is amazing. Check out this demo of Lean’s live programming features!

Kublai: Hold up, hold up, what’s the infoview? What’s a tactic?

Here’s an example program opened in VSCode (technically VSCodium).

Imagine a proof in Lean as a board game. The infoview on the right shows the state of the game. We start with some state that contains the goal, which is the thing we’d like to prove. Tactics are moves in this game that modify the state and goal. We win if we can simplify the goal to be a known true statement.

So, if Lean is so amazing, the obvious question of course is: Can we play “Bad Apple!!” in the infoview using Lean tactics?

Warm-up

Let’s cheat a little bit. The easiest way to display stuff in the infoview is by using a custom widget, which are tiny JavaScript snippets. Here’s a simple widget that plays “Bad Apple!!”:

We can now display the widget:

Kublai: What a scam. That’s not Lean! You just made a website that plays a video, wow, what a shocker.

OK, sure sure, that was some pretty heavy cheating. Let’s make it only half-cheating my displaying that widget using a tactic instead of the built-in #widget command.

Writing a Lean tactic is a dark evil art. Tactics are not normal Lean functions. They’re metaprograms. Think macros or C++ templates, but fancier. The nice thing about Lean metaprogramming is that it’s done using Lean itself instead of a cursed DSL like C++ templates. (As the cool kids would say, the the meta-level is reflected to the object-level.) The nasty thing about Lean metaprogramming is that it’s metaprogramming. You’ll see.

There’s a whole book on Lean metaprogramming but somehow the specific thing I want to do here isn’t documented, so I ended up digging up some random magic incantation from the implementation of the apply? tactic that finally worked:

Finally, let’s see our new tactic in action!²

Yay! It works! Well, obviously this would work. But can we do it without cheating? Using 100% Lean?

Let’s metaprogram harder.

Getting spammy

Kublai: Make the goal display a “Bad Apple!!” animation and I’ll stop accusing you of cheating!

Well… this is embarrassing. I couldn’t find a good way to do that. Lean only displays the updated state after a tactic finishes running, so we can’t animate the goal using a single tactic. We could make our proof thousands of lines long where each tactic advances the video frame by one, but Lean only displays the state of the current line so we’d have to hold down an arrow key and scroll at 30 FPS. Or is it LPS? Whatever. Anyways, I’d rather have some way to start the video and leave it running unattended. Also, VSCode seems to wait a bit after moving your cursor before showing the updated state so that caps us to around 5 FPS.

We need a better solution. Look back at that screenshot above. See that “Goals accomplished!” message? It’s being displayed even though the cursor is on the bad_apple line and not the trivial line, where the goal is actually solved. So there we go. We just need to spam the infoview with log messages of “Bad Apple!!” frames.

Let’s dive into the code. I made the implementation a bit more general-purpose so there’s color support even though “Bad Apple!!” is grayscale.

Next I have some boring code (omitted) that uses IO.Process.run to run some shell commands for ffmpeging the “Bad Apple!!” video into PPM images of each frame and using mpv --video=no to play the audio in the background.

I choose PPM because it seemed the least excruciating to parse, so here’s my parser:

Kublai: AAAAAHHH!! Why is there a giant math proof plopped right in the middle?

For disabling bounds checking! The nice thing about Lean is that you can choose your level of verification and safety:

1. The code above proves that bytes[start + 2] is always within bounds so the compiler can emit efficient code.
2. bytes[start]? returns an Option so our code itself can handle the out-of-bounds case.
3. bytes[start]! adds a runtime bounds check, like Rust.
4. Replacing the proof with sorry will YOLO it, like C++, and possibly segfault if you’re wrong.

Let’s skip over more boring code and do some fun metaprogramming! Here’s a tactic that shows a frame, where I’m using a file called idx to persistently track the current frame index since storing it as a goal was too finicky.

Now let’s repeatedly call this tactic from our bad_apple tactic!

Kublai: AAAAAAAAAAAAAAAAAHHHHHHHHHHHHHH!!!!!!!!

I mean… I have a reason for doing it this way (it has to be a macro, not an elab, for technical reasons) but I’m sure some erudite Lean wizard could do it in a much less cursed way, but this method is straightforward and doesn’t hurt my brain.

We can now enjoy our lovely tactic:

And… it works! Hooray! I toold yyoouuu Lleeaaannn iiiissss tttthhheeeeee bbbbbbbeeeeeeeessssssssstttttttttttt…

Ugghhhhh! VSCode is lagging like crazy! This tactic keeps prepending more and more log messages and VSCode really doesn’t like that.

This isn’t my first “Bad Apple!!” rodeo. Last time I had performance problems, I just used a better computer.

So, I tried my tactic with the same Ryzen 3950X as from that previous post and more cores didn’t seem to help. Seems like a single-threaded problem. I also tried using lean.nvim instead of the VSCode Lean extension and I got as far as somehow installing lean.nvim by pasting a bunch of random stuff before realizing I have absolutely no idea how to use Neovim.

But what is a tactic?

Why is this tactic so freaking slow in VSCode? I wrote a short main function that uses the same code to instead print to the terminal and it runs at a buttery smooth 30 FPS. So there’s definitely something slothy about VSCode. And it only becomes slow after several hundred log messages, so what if we could clear them somehow? I tried messing with Lean’s internal MonadLog but it just made my brain hurt.

Let’s take a step back. Lean is a purely functional programming language, so if you’ve been following along very, very carefully, you might’ve noticed something odd. The s tactic reads and writes directly to the filesystem! That’s not very pure, is it? It’d be pretty sad if our proof worked on one machine with the right files and then failed on the next! Wait… what even is a tactic, and what can it do?

A Lean tactic is a thing with type ReaderT Context $ StateRefT State TermElabM Unit. That’s Lean-speak for “you can do whatever the fox you want to”. A tactic can read from the filesystem. A tactic can POST to the SageMath API. A tactic can start a fork bomb. A tactic can spawn a new terminal that asks for your sudo password and becomes root and corrupts the memory of the Lean kernel so it ignores all your sorrys in your marvellous proof of the Riemann hypothesis. A tactic can launch nukes for a lovely game of global thermonuclear war.

Here’s an incredibly cursed thought: what if our tactic controlled VSCode and made it open a new identical file when too many log messages fill up in order to clear the log?

Enjoy the show.

Kublai: Thanks, I hate it.

Full code here, if you wanna give it a try. @Kevin you really need to try Lean, it’s like the Ali’s Uyghur Kitchen of programming!