Metaprogramming tutorial

Stream: lean4

[Jannis Limperg]

I've been meaning to write a tutorial about Lean 4 metaprogramming. This would give an overview of the major metaprogramming concepts, to help people get started. To keep the scope somewhat reasonable, I don't want to dive into specifics of the API, so it's not going to be a cookbook.

To begin (and also to force myself to actually do it), can I get some help brainstorming what should go into such an overview? What I have so far:

• expressions
  • Expr; overview of what each constructor stands for
  • smart constructors
  • locally nameless representation; forallTelescope and friends
  • implicit arguments, app builder (mkAppM etc.)
  • matching on expressions
  • normalisation, transparency
  • discrimination trees
• monad stacks
  • ReaderT, StateRefT
  • MonadError, MonadBacktrack etc.
• CoreM
  • the environment
• MetaM
  • metavariables, assignment, types of metavariables
  • metavariables as goals
  • local contexts, withMVarContext
• Syntax
  • syntax declarations, syntax categories (+ behavior)
  • syntax quotations (matching + construction)
• elaboration
  • TermElabM etc.
  • elaboration attributes (for commands, tactics)
  • postponed metas
  • macros
• utilities
  • tracing, dbg_trace
  • MessageData
• env extensions and attributes

Okay it's looking more like a book actually. :(

[Reid Barton]

You should add a chapter of the book about using syntax to design DSLs

[Arthur Paulino]

This is something I wish I was qualified enough to do!
I've given it some thought and maybe it would be less frightening to start with a "learn by example" tutorial about tactic writing specifically. It would be a warm up. Getting the hands dirty right away helps eliminate some mental barriers (at least for me)

• Debugging a tactic
• Reading the type of the goal
• Matching a hypothesis with the goal and closing it (assumption)
• Introducing a hypothesis
• Checking if the goal is of a → b and simulating an intros
• etc

Building these small blocks for tactics

[Jannis Limperg]

Reid Barton said:

You should add a chapter of the book about using syntax to design DSLs

Over my dead body. :smiling_devil: People are way too fond of obfuscating their libraries already.

[Jannis Limperg]

Arthur Paulino said:

I've given it some thought and maybe it would be less frightening to start with a "learn by example" tutorial about tactic writing specifically. It would be a warm up. Getting the hands dirty right away helps eliminate some mental barriers (at least for me)

This would be very helpful as well, and I agree that exercises are instrumental. Ideally, we would have different types of documentation (overview/big picture, cookbooks, reference docs) that address people's different needs.

[Arthur Paulino]

My difficulty with tutorials that cover topics like you mentioned is that, in my mind, I (consciously or unconsciously) seek tutorials to do something. So reading tutorials that are also some sort of reference manuals is usually a hard experience for me

[Mario Carneiro]

To some extent this should just be covered by documentation in the code

[Mario Carneiro]

I think there isn't nearly enough documentation for some of these functions. I wish lean 4 had a similar rule to mathlib: every def needs a doc comment

[Arthur Paulino]

Even if those are documented, if I understood correctly, Jannis intent is to approach those in a less dry way. Docstrings are usually super short and more suitable for people that already understand the abstract concept behind the implementation

[Jannis Limperg]

Mario Carneiro said:

I think there isn't nearly enough documentation for some of these functions. I wish lean 4 had a similar rule to mathlib: every def needs a doc comment

That would also help of course. But many of the big picture concepts are actually covered reasonably well; it's just a matter of finding the right docstring. And this is always going to be an issue, which is why I believe it would be valuable to have a document that has most of the concepts in one place.

[Arthur Paulino]

Maybe what you intend to do is more like a "manual" rather than a "tutorial", given the scope you've mentioned

[Mario Carneiro]

Arthur Paulino said:

Even if those are documented, if I understood correctly, Jannis intent is to approach those in a less dry way. Docstrings are usually super short and more suitable for people that already understand the abstract concept behind the implementation

I don't think this is a given at all. In particular some of the module docs are huge and explain abstract concepts

[Mario Carneiro]

Of course there is always room for supplementary documentation, but for goal directed documentation I think it is better to do this via code comments than a reference manual

[Mario Carneiro]

at least considering the way things are now

[Mario Carneiro]

Maybe an example you could use for inspiration is the rustc dev guide, which covers all the major systems at a high level, without really going in enough depth on any particular bit to qualify as a code comment

[Jannis Limperg]

Mario Carneiro said:

Maybe an example you could use for inspiration is the rustc dev guide, which covers all the major systems at a high level, without really going in enough depth on any particular bit to qualify as a code comment

At a glance, yes, this looks very similar to what I had in mind.

[Arthur Paulino]

[props to referencing the Dhammapada :smiley:]

[Alexander Bentkamp]

Maybe you can add a section about environment extensions? Maybe also custom attributes (registerAttribute) and custom options (register_option)?

[Mario Carneiro]

Also initialization: @[init], initialize, and builtin_initialize

[Mario Carneiro]

I think a general overview of where environments come from and how staging and initialization works would have been very helpful to me when I started

[Arthur Paulino]

The scope is really big already, but I also want to mention an overview of what metaprogramming is for

[Gabriel Ebner]

Other topics that I haven't seen being mentioned so far: delaboration, TacticM

[Gabriel Ebner]

Generally speaking, I think it is more useful to provide a comprehensive overview than to go into great detail. There are so many different ways to do the same thing in Lean 4, that I'm often missing a nicer shortcut because I only know the manual way to do something (and I've seen the same thing with other people's PRs on mathlib4).

[Jannis Limperg]

Gabriel Ebner said:

Other topics that I haven't seen being mentioned so far: delaboration, TacticM

Oh yeah, delaboration is a good one. I know very little about that myself. Thanks everyone for the suggestions, keep them coming!

[Arthur Paulino]

Gabriel Ebner said:

There are so many different ways to do the same thing in Lean 4, that I'm often missing a nicer shortcut because I only know the manual way to do something

Which reminded me of this (can we have something similar for Lean 4?)

[Arthur Paulino]

@Gabriel Ebner I didn't understand your comment. Wouldn't providing detailed examples encourage the standardization of straightforward ways to do things?

[Gabriel Ebner]

I don't really care about standardization per se. But quite often there's shorthand syntax that dramatically reduces the boilerplate. E.g. termElab -> elab_rules -> elab, etc. Or using a two-line macro instead of thirty lines of tactic elaborator. Both approaches accomplish the same, so it's easy to know one but be completely unaware of the other.

[Henrik Böving]

Hijacking this thread a bit, we are also still missing a tutorial for just programming without the Meta, I don't know about you but I learned everything I know about how to write stuff in Lean by grepping around in the compiler and trying stuff out since TPIL is (as its name suggests) focused on theorems and not general purpose programming, maybe we could also brainstorm a bit about what a "Programming in Lean" would need to contain?

[Kevin Buzzard]

Do you know about the unfinished Lean 3 version of programming in Lean? https://leanprover.github.io/programming_in_lean/programming_in_lean.pdf

[Kevin Buzzard]

That reference taught me what a monad was!

[Henrik Böving]

Ah that's certainly going in the right direction yes...although I am a bit unsure about the entire verification part. Yes verification is a pretty big thing in Lean of course but if we want to attract the average functional programming interested person as well and the introduction resource even has formal proofs before introducing how this monad thingy works I don't think that's too attractive for such a person, especially considering that one of the reasons Haskell is disliked among the "normal" programming community is that "it requires you to know so much maths" (which really it does not but but that's not the point here).

[Henrik Böving]

Maybe having another separate resource for that would be good? THen again we are basically talking about a small bookshelf at this point already...

[Siddhartha Gadgil]

I feel the Type-Driven Development with Idris is a good model, except that most of its examples are systems programming related, while with lean having mathematics related examples may be better. It is also rather easy to find mathematics examples with conditions: the first one I use is subtraction defined with a witness to leq.

[Tomás Díaz]

Arthur Paulino said:

My difficulty with tutorials that cover topics like you mentioned is that, in my mind, I (consciously or unconsciously) seek tutorials to do something. So reading tutorials that are also some sort of reference manuals is usually a hard experience for me

I've found this document on documentation (lol) really nice on this topic https://documentation.divio.com/ - idk if it's widely known.

[Mac]

Henrik Böving said:

[O]ne of the reasons Haskell is disliked among the "normal" programming community is that "it requires you to know so much maths" (which really it does not but but that's not the point here).

And one of the reasons why people think this is because a lot of the documentation for Haskell utilities explains concepts in mathematical terms (e.g., monads) which gives users the impression you need to know the math to use the concept, when generally, you don't. A great example of this is monads, which are described in the API documentation largely by the mathematical monad laws (despite the fact many Haskell monads are not lawful) instead of describing them from a control flow / do notation approach, which would be easier for a non-mathematics-focused computer scientist to follow.

This is something we should probably keep in mind for any programming-focused Lean docs. The examples and descriptions should probably avoid any reference mathematics to attract the less mathematically inclined so as to not give Lean the same (false) reputation as Haskell (i.e., that you need to know maths to use it).

[Kevin Buzzard]

I think that this is particularly important here because lean 3 has made an impact with its mathematics so one can incorrectly deduce from this that Lean is "for mathematicians" or even worse "only for mathematicians".

[Edward Ayers]

Hi all, I half-wrote a metaprogramming tutorial for Lean 3 about 3 years ago and I'm spending today porting it over to Lean 4. I'm plopping it in mathlib4 for now. https://github.com/leanprover-community/mathlib4/pull/243

more to come.

[Jannis Limperg]

Oh very nice! I'll coordinate with you to contribute more stuff once I'm no longer consumed by my eternal quest to have Aesop correctly deal with metavariables.

[Arthur Paulino]

@Jannis Limperg nice!
I started a tactics writing tutorial and then Edward brought his material. @Ian Benway also told me that he wants to participate with his learnings. Soon enough we'll need to organize the content in a more cohesive structure

[Arthur Paulino]

I think the structure you gathered in the beginning of the thread with input from the community is really good

[Arthur Paulino]

After talking to @Edward Ayers, I've moved the content to this repository: https://github.com/arthurpaulino/lean4-metaprogramming-book.

This repository is meant to be temporary. Once the content is finished (in markdown), we can place it wherever we want.

I'm almost done finishing up the introductory chapter, whose first version was written by Ed.

If anyone wants to be a collaborator, just let me know. Or feel free to open PRs :pray:

[Siddhartha Gadgil]

Thanks for this effort. I would be happy to contribute a bit. One suggestion: have an Expressions section as there are a huge number of helpers for constructing expressions (unless the plan is to put these in some other section). For instance, the monadic mkLambdaFVars is extremely useful.

[Arthur Paulino]

Expr is one of the datatypes discussed in the second chapter

[Patrick Massot]

It's really amazing that this meta-programming tutorial is making progress. This is a very very important project.

[Arthur Paulino]

@Siddhartha Gadgil let me know if you want to be a collaborator in the repo (create branches, issues etc)

[Siddhartha Gadgil]

Either way is fine with me. I can work with fork and pull-request or directly with the repository.

[Siddhartha Gadgil]

I see that there is a nice discussion of Expr in datatypes.

What I was asking about was the huge range of helpers taking care of hygiene, unification, hashing and such things as well as matching, so the user does not need to directly deal with expressions. I mean stuff like mkLambdaFVars to create lambda-expressions, mkAppM for unified application, Expr.eq? to match equalities, forallTelescope and friends (I personally don't really understand telescopes).

Perhaps these should be a separate Expr.md file (or Cookbook.md)?

[Siddhartha Gadgil]

Another question: is the format designed to run with docgen4? Or some other literate programming framework?

[Henrik Böving]

If its markdown we can render it

[Arthur Paulino]

My current plan is to use my lean2md Python script to turn those lean files into markdown files. I want to be able to write while typechecking stuff. I also don't want to be copy/pasting Lean code to markdown codeblocks manually

[Henrik Böving]

No no I mean, if your doc comments are markdown doc-gen4 can render it, there is no need for any further tangling

[Arthur Paulino]

Ah, I see. But still, for a book I think we want the actual md files in the end

[Arthur Paulino]

Siddhartha Gadgil said:

I see that there is a nice discussion of Expr in datatypes.

What I was asking about was the huge range of helpers taking care of hygiene, unification, hashing and such things as well as matching, so the user does not need to directly deal with expressions. I mean stuff like mkLambdaFVars to create lambda-expressions, mkAppM for unified application, Expr.eq? to match equalities, forallTelescope and friends (I personally don't really understand telescopes).

Perhaps these should be a separate Expr.md file (or Cookbook.md)?

I think those are totally worth mentioning and even showing use examples.

I guess Expr is too important of a datatype and deserves a chapter of its own? That's how Jannis structured the TOC in the beginning of this thread

[Jannis Limperg]

I still think so, yes! However, there's a bit of a dependency problem since many of these Expr functions need MetaM. So you either introduce MetaM quickly and superficially, deferring detailed discussion to the monad chapter; or you split the Expr stuff. I think I prefer option 1, but I'd have to try it to see how it works out.

[Arthur Paulino]

Monads got me thinking that this book would need a "Programming in Lean 4" book first. The fact that we're introducing specific notation for monadic programming like ← and do makes me a bit uncomfortable

[Jannis Limperg]

I was planning to assume that the audience already knows how to program in Lean (with maybe quick links to TPIL4 or the reference manual for more esoteric stuff).

[Arthur Paulino]

That's a good assumption. On the helper functions to manipulate terms of Expr, what if we delay their introduction and talk about them in the MetaM chapter? I think it will make the text more cohesive

[Jannis Limperg]

This is what I meant with "split the Expr stuff". I'm fine with trying this option first if you feel it's gonna be better. Just have a forward reference in the Expr chapter so readers know they won't have to write abominations (mkApp (mkApp (mkConst `Eq #[Level.one]) (mkFVar x) (mkFVar y)) forever.

[Sebastian Ullrich]

Henrik Böving said:

No no I mean, if your doc comments are markdown doc-gen4 can render it, there is no need for any further tangling

Alectryon would probably be more appropriate since you want to see the code as is, no?

[Arthur Paulino]

Alectryon would work too, but I think it's a bit of overkill. Being able to extract the markdown files in order to have input for something like https://github.com/leanprover/theorem_proving_in_lean4 should be enough

[Sebastian Ullrich]

We're considering porting all Lean 4 documentation over to LeanInk+Alectryon since really there's no reason not to do it

[Arthur Paulino]

Oh, I see now. We'll see after the content is more ready

[Siddhartha Gadgil]

There is a natural split as the basic constructors (like mkAppN) are in Expr.lean while the meta helpers (like mkLambdaFVars) are in Meta/Basic.lean. So the latter can go into the Meta.md chapter and the former in Expr.md.

[Arthur Paulino]

@Siddhartha Gadgil please feel free to propose changes to the structure that we have so far. I've already changed it a bit after some input from this thread (regarding Expr) but I'm sure we can do better together. "skeleton building" PRs are very much welcome. By "skeleton building" I mean building the structure with sections and subsections but leaving the content marked with --todo

[Arthur Paulino]

Also notice that I'm putting extra effort trying to follow the suggestion from the community of not making it sound like a "Lean is for mathematics and mathematicians" text. Most of the changes that I made on Ed's first version (which he had written targeting Lean 3, 3 years ago) were on that direction

[Arthur Paulino]

I had this idea of starting from Syntax and building up to Expr. Basically every example involves processing syntaxes.

If we start from Syntax, we can introduce macros right away. I think it can be motivating

What do you folks think?

[Arthur Paulino]

Sebastian Ullrich said:

We're considering porting all Lean 4 documentation over to LeanInk+Alectryon since really there's no reason not to do it

Is there an example of the end result of that combination? I find the output of mdbook remarkably pretty and pleasant to read

[Leonardo de Moura]

Yes, we have:

• input: https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean
• output: https://pp.ipd.kit.edu/~ullrich/tmp/examples/tc.lean.html

It is not as pretty as the mdbook output yet, but we are all confident we will get there. It already has really nice hover information, and we can visualize the tactic state.

[Siddhartha Gadgil]

I have created a pull request with a bunch of examples of constructing expressions both directly and using smart constructors.

[Jannis Limperg]

Arthur Paulino said:

I had this idea of starting from Syntax and building up to Expr. Basically every example involves processing syntaxes.

If we start from Syntax, we can introduce macros right away. I think it can be motivating

What do you folks think?

I somewhat dislike the whole Syntax layer. Lots of sugar ($[$t:term],*); some annoying edge cases (leading_ident_behavior := both); subtle differences between syntax categories and syntax defs; macros are too powerful for my liking (recursion and nondeterminism) and simultaneously never powerful enough for what I want to do. This is entirely personal preference, of course, but as a result I would try to de-emphasise this layer.

For my students, I wrote a little tactic that takes a 'MetaM tactic' x : MVarId -> MetaM (List MVarId) and executes it. This way, they can run their metaprograms without having to think about syntax at all.

import Lean

open Lean
open Lean.Elab
open Lean.Elab.Term
open Lean.Elab.Tactic (Tactic liftMetaTactic)
open Lean.Meta

syntax (name := runMetaMTactic) &"run_MetaM_tactic" term : tactic

abbrev MetaMTacticType := MVarId → MetaM (List MVarId)

unsafe def evalMetaMTacticUnsafe (e : Expr) : TermElabM MetaMTacticType :=
  withDefault $ withoutModifyingEnv do
    let type ← inferType e
    let expectedType := Lean.mkConst ``MetaMTacticType
    let (true) ← isDefEq type expectedType
      | throwTypeMismatchError "runMetaMTactic" expectedType type e
    let name ← mkFreshUserName `_tmp
    let decl := Declaration.defnDecl {
        name := name, levelParams := [], type := type,
        value := e, hints := ReducibilityHints.opaque,
        safety := DefinitionSafety.unsafe
    }
    ensureNoUnassignedMVars decl
    addAndCompile decl
    evalConst MetaMTacticType name

@[implementedBy evalMetaMTacticUnsafe]
constant evalMetaMTactic (e : Expr) : TermElabM MetaMTacticType

@[tactic runMetaMTactic]
def evalRunMetaMTactic : Tactic
  | `(tactic|run_MetaM_tactic $t:term) => do
      let t ← withoutErrToSorry $ elabTerm t (Lean.mkConst ``MetaMTacticType)
      synthesizeSyntheticMVars (mayPostpone := false)
      let t ← instantiateMVars t
      let tac ← evalMetaMTactic t
      liftMetaTactic tac
  | _ => unreachable!

def greet (msg : String) (goal : MVarId) : MetaM (List MVarId) := do
  trace[debug] "{msg}"
  return [goal]

set_option trace.debug true

example : True := by
  run_MetaM_tactic greet "hi"
  trivial

[Siddhartha Gadgil]

I also agree (this was also discussed in another thread) that using Syntax for logic and control is far from ideal, and it is best to work at the Meta/TermElab level for this. Lean 4 macros are superb for notation and for creating some shortcuts. But passing around bits of syntax as proxies for function arguments is very fiddly.

[Arthur Paulino]

But if there's no clear intention from Lean 4 core devs to change it, I think we better talk about it and explicit the issues. Otherwise readers will have many questions when reading Lean 4 source code (or even the code of some Mathlib4 tactics)

[Henrik Böving]

There should be separate chapters for it that dont introduce knowledge that is a hard requirement to understand the rest IMO

[Jannis Limperg]

Arthur Paulino said:

But if there's no clear intention from Lean 4 core devs to change it, I think we better talk about it and explicit the issues. Otherwise readers will have many questions when reading Lean 4 source code (or even the code of some Mathlib4 tactics)

Yes, of course. I just wouldn't put Syntax front-and-centre. Another way to deal with this would be to have a Syntax primer towards the beginning of the book with a warning that the material there is incomplete (and with a forward reference to the full explanation). That could work as well.

[Arthur Paulino]

Another approach I've been thinking about: focus on functions like @[macro myMacro] def expandMyMacro : Macro := fun stx => ..., similar to what you'd do with the tactic tag. And then later talk about the macro and elab shorctuts. Is my read accurate that the main issue lives on the macro/elab syntax?

[Arthur Paulino]

Siddhartha Gadgil said:

I have created a pull request with a bunch of examples of constructing expressions both directly and using smart constructors.

Thanks!! Will read soon!

[Siddhartha Gadgil]

Understanding Syntax is very much necessary. I think the point both @Jannis Limperg and I are making is that one should avoid readers driven to using macros and working with syntax where it is better to use Meta/Elab and work with expressions, simply because one can start working with macros a bit quicker.

[Arthur Paulino]

Alright, thanks for clarifying! I will throw this idea away for now and stick to the current TOC sequence

[Eric Rodriguez]

Leonardo de Moura said:

Yes, we have:

• input: https://github.com/leanprover/lean4/blob/master/doc/examples/tc.lean
• output: https://pp.ipd.kit.edu/~ullrich/tmp/examples/tc.lean.html

It is not as pretty as the mdbook output yet, but we are all confident we will get there. It already has really nice hover information, and we can visualize the tactic state.

one thing that I found in the Lean3 Alectryon port is that showing the state after every <;> and similar combinators quickly got unwieldy - I feel like maybe it's nicer to just ignore combinators and put everything together. Although maybe this is a bit different as Lean4 does show all the intermediate states affected

[Eric Rodriguez]

(and similarly with goals accomplished, but it actually looks really nice here - maybe a green-colour bubble is good to signal that it's not got any state information?)

[Arthur Paulino]

Some extra progress has been made and reviews are very welcome:
https://github.com/arthurpaulino/lean4-metaprogramming-book

@Jannis Limperg do you mind being more specific on what you mean by the following topics on the "Expressions" chapter?

• matching on expressions
• normalisation, transparency
• discrimination trees
• unification

[Siddhartha Gadgil]

Made another pull request with a couple of more examples.

[Siddhartha Gadgil]

And another example, involving matching.

[Jannis Limperg]

Arthur Paulino said:

• matching on expressions

I was thinking about (a) various functions to match specific expressions (equalities etc.), just noting where to find them; (b) a note about matching up to computation. The latter means that you have to whnf to the right level before you match. The mechanics of this are not hard (though a bit annoying), but some examples would be nice, since I think people tend to not be aware how deeply computation permeates metaprogramming. (At least I was a little naive about this when I started, even though I had done a fair amount of type theory before.)

• normalisation, transparency

whnf. Normalisation in the presence of unfoldable constants (this is where transparency comes in, i.e. withReducible etc.) Maybe a short note about normalisation in the presence of metavariables.

• discrimination trees

A discrimination tree is a map with Expr keys where lookup is performed (efficiently) up to normalisation. They're used all over the place to index expressions, e.g. for simp lemmas.

• unification

isDefEq. The effect of transparency (again). Metavariable assignment during unification, including the different MetavarKinds.

Obviously, some reordering of these topics is in order. ;)

[Jannis Limperg]

I've added delayed-assigned metavariables (which I've had the pleasure(?) to learn about this week) to the structure in the OP.

[Arthur Paulino]

Great news: @Henrik Böving has written the chapter on Elaboration :octopus:
Feedback is very much welcome :pray:

[Henrik Böving]

@Arthur Paulino and I were trying to figure out an order to present the topics in that actually makes sense to people. We figured that most end users will most likely care about 1 of 3 things:

• just basic notation for writing code quicker
• actual DSLs
• tactics

so i attempted to draw a DAG that shows the "knowledge dependencies" (i am aware of) so to speak, dotted lines represent optional dependencies so for example one can understand term elaboration etc. without knowing how attributes work in detail even though the inner workings rely on attributes: image.png (Does this graph look correct? (not in the aesthetic sense :p))

One thing we noticed was that, the ability to deal with syntax so to declare it and match on it seems rather central when viewed like this so its probably close to impossible to avoid a good explanation of it rather early on. It also shows that a lot of the topics mentioned above are not relevant across use cases so for example a tactic programmer will most likely be fine with just knowing Syntax, MetaM and Expr while DSL people are interested in term elaboration and so on. So now we are wondering whether it even makes sense to build the tutorial/book as a linear resource? The knowledge graph does definitely not look linear.

[Arthur Paulino]

Thanks a lot for the DAG!

Yeah, we are trying to figure out a good way to present connected topics with a (minimal) building path. Ideas are very welcome.

Here are my ideas:

• We can cut off Attribute, CoreM, Env Extension, Initialization, Delaboration and Options (at least in the first iteration of the guide)
• Instead of making TacticM as a big goal, we can make Tactics as a big goal and Macro and TacticM as means to achieve it

[Arthur Paulino]

This is what I thought. We'd go from left to right. @Jannis Limperg what do you think?
image.png

[Jannis Limperg]

Looks good to me. The general problem -- that not all content of the book is relevant to all audience members -- is something that happens with just about any text. I don't think this merits any radical changes to the form of the text (e.g. breaking it up into separate volumes). But it may be useful to design multiple "paths" through the book and to ensure that these can be followed independently. Software Foundations, for example, has this roadmap.

[Arthur Paulino]

Hello everyone! I bring some updates about this front.

@Henrik Böving has been extremely helpful and we've been talking a lot about the content and didactic of this book lately. As you can see above, we were able to simplify the chapters by asking ourselves what are the most common practical motivations to learn metaprogramming in Lean 4.

We thought about DSLs and Tactics, so we backtracked the requirements without allowing ourselves to regress too much. We, then, simplified the chapters even further to come up with the current model:

• Introduction
• Expressions
• MetaM
• Syntax
• Elaboration
• Macros
• DSLs
• Tactics

So far, we got the 6 first chapters written to a point that's worth sharing. So this is a good moment for experts and beginners to read and provide corrections and feedback. If something is not clear or if some piece of information is missing, please let us know!

https://github.com/arthurpaulino/lean4-metaprogramming-book

Thanks everyone who's been helping out. Only two more chapters to go :pray:

[Arthur Paulino]

Hi! We're happy to announce that the first version of the main trunk of the Lean 4 Metaprogramming Book is now complete. There are still items to cover (and help is welcome, as always), but all chapters have content so the read show be fluid at this point.

HUGE thanks to everyone who's helped and/or has been helping. @Siddharth Bhat was able to kill the last two chapters and @Henrik Böving has revamped the chapter about elaboration.

If you've read the book and hasn't understood something, please let me know. Comment here or send me a DM and I will take a look.

[Malcolm Langfield]

In the chapter on expressions, there is mention of the quotation/backtick syntax for names. It would be nice if this were defined a bit more explicitly, e.g. why you can't just use ordinary strings, difference between double and single, etc. There is almost nothing on this in the Lean 4 manual or TPIL, just this:

Declaring a new syntax category like this one automatically declares a quotation operator `(binderterm| ...).

I was not able to easily find anything in the Lean 4 source describing this syntax either. But it does appear in some places in the manual, and it appears almost immediately in the metaprogramming book.

I think I would have been pretty confused by this syntax if I hadn't seen Lisp before.

[Malcolm Langfield]

Though perhaps everyone who is interested in metaprogramming in Lean has already been exposed to all the related syntax.

[Arthur Paulino]

I apologize. We had it before and I probably stripped it away doing some scope simplification. This time I probably cut too much. I'll add it back, thanks for pointing it out!

[Malcolm Langfield]

No worries! The book is excellent!

[Adam Topaz]

@Arthur Paulino congratulations to you and your coauthors on this work! I'm looking forward to reading it soon. Quick question: is there a quick way to compile this into a PDF?

[Arthur Paulino]

Not that I know... Currently we're using a Python script to turn Lean files into markdown files. Eventually we can switch to the LeanInk + Alectryon approach and we should have more powers there. Maybe then we'll be able to extract the respective PDF files

[Julian Berman]

Maybe pandoc knows how (to compile a bunch of markdown to pdf)

[Julian Berman]

Otherwise md2html -> pdf would be a thing. Can try when back at a computer if no one succeeds first.

[Julian Berman]

Yeah probably needs a bit of tweaking for word wrapping (and syntax highlighting) and a few additional missing characters, but e.g.:

pandoc --to pdf md/{main/intro.md,main/expressions.md,main/metam.md,main/syntax.md,main/macros.md,main/elaboration.md,main/dsls.md,main/tactics.md,main/cheat-sheet.md,extra/options.md,extra/attributes.md,extra/pretty-printing.md} -o 'Lean 4 Metaprogramming (Paulino et al.).pdf' --pdf-engine=xelatex -V monofont='DejaVu Sans Mono'

produces Lean-4-Metaprogramming-Paulino-et-al..pdf.

Arthur happy to PR that as a GH Action workflow if helpful of course.

[Arthur Paulino]

It looks nice but some lines are going through the right margin :thinking:

[Arthur Paulino]

How to prevent that?

[Arthur Paulino]

Ah, it also got the chapter order messed up, which is expected. I guess it's sorting the chapters by alphabetical order

[Patrick Massot]

I don't understand what is the intended way of reading the book. Are we meant to read the md files on GitHub?

[Arthur Paulino]

Yes, at least for now. I wanted us to focus on the content first (while having this bare bones presentation). Now that the content has reached a more stable form, we can discuss how we want to present it

[Arthur Paulino]

@Malcolm Langfield I forgot to say but the info about single/double quotes is on the chapter about expressions. And the info about `(foo| ⋯) can be found on the chapter about Syntax

[Julian Berman]

It looks nice but some lines are going through the right margin

I think slightly better and prettier now (by using a different template): Lean-4-Metaprogramming-Paulino-et-al..pdf

The chapter order is correct no? I specified it manually just copying what was in the README

[Julian Berman]

Syntax highlighting requires some XML file that maybe someone has written for teaching pandoc to highlight Lean4.

[Arthur Paulino]

Yes, my bad about the order! It is indeed correct :+1:
Btw, it's looking beautiful. Syntax highlight seems to be the last ingredient

Ah, and a cover with credits to everyone involved. Maybe we need a cover.md?

[Julian Berman]

Bout to jump on a call but yeah think so.

[Julian Berman]

I did absolutely nothing to make it look nice btw, just used / found https://github.com/Wandmalfarbe/pandoc-latex-template. The command I ran now was:

pandoc --from markdown --to pdf md/{main/intro.md,main/expressions.md,main/metam.md,main/syntax.md,main/macros.md,main/elaboration.md,main/dsls.md,main/tactics.md,main/cheat-sheet.md,extra/options.md,extra/attributes.md,extra/pretty-printing.md} -o 'Lean 4 Metaprogramming (Paulino et al.).pdf' --pdf-engine=lualatex -V monofont='DejaVu Sans Mono' --toc --template eisvogel.latex --data-dir .

in case you want to run it yourself.

[Patrick Massot]

With syntax highlighting I would print it tomorrow.

[Julian Berman]

I am trying to figure out how to adapt these listings instructions from the lean4 repo but I am LaTeX inept... no luck yet.

[Julian Berman]

Here's a version with syntax highlighting (and updated to today): Lean-4-Metaprogramming-Paulino-et-al..pdf

What I did to get it is slightly not pretty, so undoubtedly I may have introduced a mistake or two.

[Arthur Paulino]

It looks nice! There are some "unexpected" import Lean lines that are a bit funny out of context. It's dragging the import Lean from the beggining of the next chapter

[Julian Berman]

Aha. I see. OK probably I'm missing an option telling it to page break between chapters, that should be easy to fix.

[Henrik Böving]

What tool are you using for this? Some pandoc framework I guess?

[Henrik Böving]

Noticed this cosmetic bug as well: image.png

[Julian Berman]

Yeah, it's roughly the command above, combined with this template, but then I can't figure out how to get pandoc to make use of listings in the same way as the lean4 repo recommends, so I literally turned it off and then the ugliness is replacing lines with \begin{verbatim} with \begin{lstlisting}.

[Arthur Paulino]

@Julian Berman don't bother with those import Lean. I'm solving it in another way. I'm removing them from the top of the files

[Julian Berman]

Henrik Böving said:

Noticed this cosmetic bug as well: image.png

This is some font alignment issue I think, since it's correct in the .tex file and just being misrendered, so now have to see what I'm (or really the template is) doing differently there.

[Arthur Paulino]

And btw Julian, this looking really nice. And of course requires effort.
Feel free to setup a GH workflow to generate this PDF whenever you're satisfied with the result, as you proposed before :pray:

[Orestis Melkonian]

s/indexes/indices/g

[Arthur Paulino]

Updates:

1. @Damiano Testa has added a new chapter, which is a Cheat Sheet for quick look up
2. MANY typos were fixed. Thanks everyone for the PRs
3. The DSL chapter has been simplified and I believe it's now easier to follow

[Julian Berman]

Third time's a charm (though not yet for CI where I'm down to issues installing DejaVu fonts...). But here's a version with proper rendering of unicode.

[Dan Velleman]

I've been reading this tutorial, and I've got a few suggestions. These suggestions are based on my understanding of what I've read, which might not be completely correct.

In the chapter on MetaM, I think it would be helpful in some of the examples to explain what problem is being solved by the new functions that are being introduced. For example, in the doubleM example, it might be helpful to point out that, in a context in which n is a free variable of type Nat, the expression n + n has type Nat, but the expression fun (n : Nat) => n + n makes sense even in a context in which n is not a free variable. So to create an Expr for this function one needs to create a temporary context in which there is a free variable n of type Nat, construct the expression n + n in that context, and then abstract to construct the lambda expression, which will then make sense in the original context. The purpose of the withLocalDecl function, as I understand it, is to create that temporary context. Also, although I understand why you chose to use the letter n in so many places in this example, I actually found it a little confusing. I found myself wondering whether it was necessary to use n as the variable in the definition of the function that is the last argument to withLocalDecl. I think it might actually be clearer to write the last line as fun x : Expr => mkLambdaFVars #[x] $ mkAppN (mkConst ``Nat.add) #[x, x], to make it clear that the last argument to withLocalDecl is a function that would take any free variable and construct a lambda expression using that free variable, and then that function gets applied to the variable named n.

Similarly, I'd like to see an explanation of the problem that is solved by mkAppM in the lenExprM example. You might explain that, even though #eval List.length egList gives the result 4, it wouldn't work to use mkApp (mkConst ``List.length) list in the definition of lenExprM. My understanding is that the reason for this is that List.length has an implicit argument for the type of the elements of the list. That argument is inferred by Lean when you give the command #eval List.length egList, but it is not inferred by mkApp. As I understand it, mkAppM solves this problem by inferring and filling in the missing argument. (Would it work to use mkApp (mkApp (mkConst ``List.length) (mkConst ``Nat)) list in the definition of lenExprM? It seems to work without reduce, but when I include reduce I get an error message. Why?)

In the propM example, it seems like mkAppM is being used for a much less important reason. It might be clearer to use let rhs := mkApp f (mkApp (mkConst ``Nat.succ) n), since there is no implicit argument that needs to be filled in here, so there is no need for mkAppM.

Finally, I think it might be helpful to have a little more explanation of the role of monads here. I don't mean an explanation of the theory behind monads. I'd just like more explanation of the practical effects of declaring something to have type MetaM Expr rather than Expr. For example, as I understand it, if F has type Expr then I can write let x := F, but if it has type MetaM Expr then I have to write let x ← F.

[Henrik Böving]

First things first thank you for the feedback, I think it will definitely help to clear up the issue I'm about to describe^^

We are aware of the issues surrounding the MetaM chapter, particularly that it doesn't really have a thread of thought, there is just things being introduced at random, we hope to clear this up eventually. The reason it is done this way is mostly because MetaM is a tool to be used by the future chapters and not exactly a thing on its own, you usually don't see MetaM being used alone, it's always MetaM getting called from a TermElabM, a TacticM etc.

Regarding monads, the book right now assumes that the user has a grasp on what a monad does up to what monad stacks are, there is some material on what those are and what they do in the temp folder: https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/temp/monad-stacks.lean. For your basic example, not exactly right, if F has type MetaM Expr you can still write let x := F and it will have type MetaM Expr. If you want to unwrap the Expr value from the MetaM monad you have to use the arrow notation. As a very dumbed down view ( I will refrain from writing yet another monad tutorial here, but maybe in the future if the need arises) you can think of let x <- F notation as a "programmable semicolon" that is if you write some let binding with an arrow like this there will be some sort of additional thing happening implicitly, depending on what monad you ar eoperating in, this can be a variety of effects:

• in the IO monad its actually performing the IO operation
• in the Option monad it checks whether the value on the right hand side is a None and if it is will return early from the function you are currently in with a None
• in the State monad it might make changes to your state.
• in the Reader monad it might read from the read only state that is getting explicitly passed around

and so on. Most of the Monads you see in Lean meta programming are a monad stack (which is basically a combination of multiple of these effects) that consist of State and Reader, so they provide your program with some read only and some writeable state that enables you to have a nicer meta programming experience in this case.

[Dan Velleman]

Oh, and one more thing. In the oneMetaVar example, I think the explanation before the example gets the roles of mvar2 and mvar3 backwards.

[Dan Velleman]

(deleted)

[Mario Carneiro]

@Dan Velleman you can edit your posts fyi

[Dan Velleman]

Thanks Henrik. Yes, you're right, I wasn't precise enough in my attempt to distinguish between MetaM Expr and Expr.

My knowledge of monads is limited to what I learned from Chapters 6 and 7 of The Hitchhiker's Guide to Logical Verification. That was enough for me to learn to write simple tactics in Lean 3, and in fact I eventually decided that it was more than I needed to know for that purpose--to write tactics, I really just had to know when to use := and when to use ←, when to use return, and how to deal with the fact that a tactic might fail. It would be nice if the tutorial you are writing could be written in such a way that it would be readable by someone with my limited knowledge of monads--if that's possible.

[Arthur Paulino]

In my current understanding, covering monads is not an easy task. Mostly because it's hard to to hit the sweetspot for what the reader needs. Monadic programming is an involved topic in itself and could be covered on a reasonably long chapter of a book about functional programming.

On the other hand, I'm a fan of self-contained sources of knowledge, so there's clearly a conflict for me. I really don't know if a short intro to monads in Lean 4 would be helpful or if it would be vague enough to cause more confusion! Maybe a section in the intro chapter talking about the syntax and keywords? Mostly to mention some things you mentioned like <- versus :=, do notation and when to use return.

@Leonardo de Moura do you know how this topic will be covered in the Functional Programming in Lean book?

[Leonardo de Moura]

@Arthur Paulino Yes, the book will cover monadic programming :)
cc @David Thrane Christiansen

[David Thrane Christiansen]

Here's the current plan, subject to revision as the text reveals itself. The book will cover what I think are the basic skills of functional programming:

• Understanding computation as evaluation of expressions
• How to think about honest-to-goodness side effects in that context
• Programming with structures like functors, monads, monoids, etc, and thinking about code as "programming up to axioms" rather than just seeing what a concrete instance does (this includes do-notation and the like)
• Higher-order functions, functions as values
• Polymorphism and how polymorphic function types help write correct programs by restricting the allowable variation in the implementation

I'll also have some things about dependently-typed functional programming:

• Making friends with a termination checker, various techniques for making things structurally recursive where possible
• Using universes a la Tarski to do things like what people use GADTs for in Haskell

And of course some things about Lean 4 in particular:

• How to think about and evaluate the run-time performance of programs
• How partial functions work
• Useful tools in the Lean libraries, like arrays
• An intro to the FFI

[Siddhartha Gadgil]

I should clarify (I really should have responded) that there was a common motivation for many of the examples there (which I put), which was forward/mixed reasoning. I did not mention this as I thought the application was not of great interest, but as there is clear feedback from many that a goal helps, I will try to bring this in.

Part of the problem is that finally doing forward reasoning generally needs one to go to the TermElabM level. But I will try to give examples that do not need this.

Specifically:

• mkAppM is used for forward reasoning if we want to generate terms by applying functions wherever this is legal.
• withLocalDecl is used with mkAppM if one wants to prove say _modus ponens_.

As I said I will try to make a PR with such motivating examples.

[Patrick Massot]

I took some time to read the metaprogramming book (a version I printed a couple of days ago). It was really a quick read, without typing any code. I only wanted to get an idea of what is covered and provide some quick feedback. The most important point is I'm grateful that all the authors took time to write documentation.

However the main impression I get from this book is that meta-programming is much more complicated in Lean 4 than in Lean 3. It's probably because you wanted to explain shiny new stuff that is not really needed for easy tactic writing. I also think that a major difficulty is that many of the authors are not so interested in theorem proving but rather in programming or theory of programming languages. For instance I couldn't get anything from the chapter "Embeddin DSLs by elaboration". I have no idea what this chapter is about, and I guess this was announced by the sentence "IMP, which is a simple imperative language, often used for teaching operational and denotational semantics." (I don't know what operational and denotational semantic means).

To illustrate why it all feels more complicated than Lean 3, let's consider the assumption tactic (which is confusingly called custom_trivial although it has nothing to do with tactic#trivial). In https://leanprover-community.github.io/extras/tactic_writing.html, this is a 4 lines long tactic. In https://youtu.be/-RQQxFVZnn4?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2&t=928 Rob golfed it to one line. In the Lean 4 book it's 13 lines long...

Maybe we could have an introduction that would be closer to a translation of https://leanprover-community.github.io/extras/tactic_writing.html, with some pointers to later chapters for more details and fancier ways.

[Damiano Testa]

Patrick, even though I am one of the authors, I share your view. I am planning to learn more metaprogramming in Lean4 and implement a simple tactic, from a more naïve point of view and maybe write, either a chapter or a separate document with more details.

[Damiano Testa]

(Also note that my main contribution to the book has been to write the cheat-sheet, which I hoped to be more useful for what you are saying.)

[Patrick Massot]

Now I'll list some more specific comments or suggestions. Page numbers refers to Julian's pdf at https://leanprover.zulipchat.com/user_uploads/3121/62PFBMZpXE_GWjK0Qi7ULQrn/Metaprogramming-in-Lean-4.pdf

• Page 3, the acronym AST is not defined anywhere.
• Page 5 is the first appearance of withStuff. At that point it's officially not meant to be understood, but later in MetaM chapter it is also not really explained.
• Page 13 and in many other places there are lists that are not rendered correctly. It works nicely where seen on https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/metam.md, but not in the pdf. Also in the pdf many comments go out of the page.
• Page 13, could you tell what N and M stand for in mkAppN and mkAppM? That would help remembering which one is which
• Page 19, in the last code block near the bottom, what are :10 and :11? I understand they refer to precedences. But are they actual Lean syntax or stuff you write to tell something to readers? The whole precedence thing really needs a lot of explanation. In Lean 3 they are rather difficult to understand and users need to understand them as soon as they want to define any notation. Sebastian told is a long time ago that they will be easier to understand in Lean 4, but they still requires a careful explanation. About notation, one very difficult part in Lean 3 is notation involving binders (using scoped). It would be nice to explicitly show examples of how it's done in Lean 4. I guess this is somewhere in the syntax chapter, but again having more mathematical examples would help immensely. For instance describing notations with binders for integrals. Or even the union examples from Sebastian's famous state of the union talk;
• Page 31, I cannot make any sense of the first sentence.
• Page 49, the first paragraph refers to admit that appears nowhere in the code

[Patrick Massot]

But let me insist again on the fact that I'm very grateful and I hope you will all continue this effort, maybe adding examples for us mere mathematicians.

[Henrik Böving]

Patrick Massot said:

s. For instance I couldn't get anything from the chapter "Embeddin DSLs by elaboration". I have no idea what this chapter is about, and I guess this was announced by the sentence "IMP, which is a simple imperative language, often used for teaching operational and denotational semantics." (I don't know what operational and denotational semantic means).

This is in fact by design, if you look further up this thread you will see that we constructed a DAG https://leanprover.zulipchat.com/user_uploads/3121/n9oow1Wc3UKgQn3FdQc7Bhg1/image.png
For the topics, as you can see the DSL part is one of the two tips of the DAG and is entirely unrelated to tactics, if you are only interested in tactics you can ignore it and the things that point to it basically.

The general idea was that if a reader wanted to learn about a certain topic they could just look at the DAG and read up on all topics required for what they want to learn.

[Henrik Böving]

That being said thanks for the feedback, I'll try to improve on my explanation of Syntax....guess you will have to re :printer:

[Arthur Paulino]

@Patrick Massot I am very grateful that you took the time to read the book and provide feedback, with some careful details, even!

If you scroll up to the very beginning of this thread, you will see that my first effort would be to make a tutorial focused on tactics specifically. And I indeed tried to do so! But it was just super hard to accomplish that goal because my impression (just like yours) is that metaprogramming in Lean 4 is indeed more complex.

In Lean 3, we do linters, tactics and notations, roughly speaking. In Lean 4, as a fully fledged general purpose programming language, the metaprogramming capabilities have to accommodate for much more possibilities. And while I, as a software engineer with a CS background, find it all just incredibly interesting, I also admit that the bar has been raised a bit higher for tactic writing. This is my impression.

One of the goals of the book is to situate the reader in a way that they would have a much easier time reading and understanding what's already in the Mathlib4 repo. There are syntax definitions, macros, macro rules (which can also be recursive!), elab, elaboration functions, more monads... There's clearly more ways to make tactics in Lean 4. In Lean 3, you declare your monadic function that consumes some parsers and you're pretty much set to write your logic.

I will iterate on your feedback and complement the intro chapter. I will also add the DAG that Henrik posted here so the reader will have an easier time when reading the book with a more specific goal in mind.

Thank you again for the feedback!!

[Siddhartha Gadgil]

Thanks @Patrick Massot for the feedback. I have added quite a bit to the explanations in the metam chapter in a PR. I would be happy to add more explanations, examples etc based on feedback.

@Arthur Paulino I have made a PR. I feel now that my planned motivation adds a lot to the complexity so make make things harder for the reader. I am taking as the thread here: constructing and manipulating expressions, to be used for tactics and elaborators.

[Arthur Paulino]

Will review after I wake up

[Mac]

I just took my first look at the book and I am very impressed with how much work all of you have put into it! :tada: You have also already outstripped the breadth of my knowledge in Lean 4 metaprogramming, which shows just how much more I have to learn! However, as person who has done a good bit of metaprogramming in other languages (e.g., Python, Ruby, Haskell, Java, C++), I do find your definition of the related terms rather narrowly tailored to Lean? Is that intentional?

For example, the term reflection in metaprogramming is generally used in interpreted languages like Python, Ruby, Java, and JavaScript to refer to introspection of the program's own code. That is, listing the functions, classes, methods, imported modules etc.; finding and inspecting their sources, and other analysis tasks. The term metaprogramming generally includes reflection, instrumentation, and other forms of dynamically generating and inspecting code. Such techniques are available in many languages without extensible syntax and in the same language as the source.

However, the books makes statements like: "the meta-level activities are done in a different language to the one that we use to write code" and "One cool thing about Lean, though, is that it allows us [...] to implement our own meta-level routines to elaborate those in the very same development environment that we use to perform object-level activities". Such a characterization would be very weird for someone coming from Ruby, Python, C++, or even JavaScript and Java (to an extent) where metaprogramming is generally though of just another part of the same language (though Java does also have external template engines for metaprogramming like Apache Velocity and JavaScript has its many transpilers). The fact the book terms this feature "reflection" would also be weird, though I can somewhat see the connection.

I did notice that most of the examples cited were other theorem provers / functional programming languages (e.g., Isabelle, Coq, and Haskell), so this may be due to a difference between the communities. I would be curious to hear how others understand the term "metaprogramming" and "reflection" and why they do. New perspectives are always interesting!

Anyway, sorry for the long essay about the second heading of the first chapter of the book (and a rather short section at that). I will hopefully have more practical and less philosophical comments about the rest of the book as I make my way through it. This part just particularly stuck out to me due to the unfamiliar framing -- especially since I thought I had a rather uncontroversial understanding of the general meanings of the terms being used here.

[Mac]

Interesting StackOverflow question on the topic: https://stackoverflow.com/questions/514644/what-exactly-is-metaprogramming

[Sebastian Ullrich]

Patrick Massot said:

The whole precedence thing really needs a lot of explanation. In Lean 3 they are rather difficult to understand and users need to understand them as soon as they want to define any notation. Sebastian told is a long time ago that they will be easier to understand in Lean 4, but they still requires a careful explanation.

I'm curious, have you read https://leanprover.github.io/lean4/doc/notation.html? What do you think of that explanation?

[Sebastian Ullrich]

Patrick Massot said:

However the main impression I get from this book is that meta-programming is much more complicated in Lean 4 than in Lean 3.

It really doesn't have to be, apart from learning finer-grained APIs and monad hierarchies. Also, I think you forgot to count the helper method used in the paper assumption impl. I would argue the following is a more idiomatic implementation in Lean 4.

/-
meta def find_matching_type (e : expr) : list expr → tactic expr
| []         := tactic.failed
| (H :: Hs)  := do t ← tactic.infer_type H,
                   (tactic.unify e t >> return H) <|> find_matching_type Hs

meta def my_assumption : tactic unit :=
do { ctx ← tactic.local_context,
     t   ← tactic.target,
     find_matching_type t ctx >>= tactic.exact }
<|> tactic.fail "my_assumption tactic failed"
-/

elab "my_assumption" : tactic => do
  let target ← getMainTarget
  for ldecl in (← getLCtx) do
    if (← isDefEq ldecl.type target) then
      closeMainGoal ldecl.toExpr
      return
  throwTacticEx `my_assumption (← getMainGoal) m!"unable to find matching hypothesis of type{indentExpr target}"

[Sebastian Ullrich]

Henrik Böving said:

For the topics, as you can see the DSL part is one of the two tips of the DAG and is entirely unrelated to tactics, if you are only interested in tactics you can ignore it and the things that point to it basically.

Just wanted to note that this description is in stark contrast to the opening of the tactic chapter

We've finally come to what may be considered by many the end goal of this book. The reason why this chapter is placed after the DSL chapter is because the tactic mode in Lean 4 is itself a DSL.

[Patrick Massot]

Sebastian Ullrich said:

Patrick Massot said:

The whole precedence thing really needs a lot of explanation. In Lean 3 they are rather difficult to understand and users need to understand them as soon as they want to define any notation. Sebastian told is a long time ago that they will be easier to understand in Lean 4, but they still requires a careful explanation.

I'm curious, have you read https://leanprover.github.io/lean4/doc/notation.html? What do you think of that explanation?

I think this explanation is already very good! I had to read certain sentences several times, but the topic is inherently complicated. Maybe you should first explain the number next to notation. And maybe it would help to explain how parsing runs on some example, with sentences like "Lean sees this token, register this information, look up in this table, then sees this token, compare that number to that other number...".

Also maybe focusing on associativity first is a bad move for mathematicians readers. In an average mathematician's mind, addition and multiplication are neither left associative nor right associative. We don't even teach those words. We teach the word "associative" alone, and it mean that (a+b)+c and a+(b+c) are the same in a very strong sense. Each year when I start teaching my course using Lean I have a very hard time explaining to students that a+b+c has to be one of those two options and not both on equal footing, and then to explain that a lemma says those things are equal. And then much later in the course I have to go to each student at least once to unblock them when they write:

calc |a - b| = |a - c + c - b| : by ring
... ≤ |a - c| + |c - b| : abs_add (a-c) (c-b),

and Lean complains it doesn't see |a - c + (c - b)| anywhere (actually the situation is often much worse because they write apply abs_add so the error message is less helpful). So if you want to avoid stacking two difficulties on top of each other, I would definitely start the precedence discussion by explaining how the precedence number decide how to parse a + b * c and then, in a second step, write "by the way this also applies to an operator and itself", explaining how Lean parses a - b - c and a^b^c and, in a third step, the really psychologically complicated one: parsing a + b + c`.

[Patrick Massot]

Sebastian, your my_assumption tactic looks really nice! It's very easy to read for someone knowning a bit of Lean 3 meta programming. The only confusing thing for me is let target ← getMainTarget which very weirdly mixes the two big classes of assignments in Lean 3: monadic ones using ... ← ... and regular ones using let ... := ....

[Patrick Massot]

Mac said:

I just took my first look at the book and I am very impressed with how much work all of you have put into it! :tada: You have also already outstripped the breadth of my knowledge in Lean 4 metaprogramming, which shows just how much more I have to learn! However, as person who has done a good bit of metaprogramming in other languages (e.g., Python, Ruby, Haskell, Java, C++), I do find your definition of the related terms rather narrowly tailored to Lean? Is that intentional?
[...]
I did notice that most of the examples cited were other theorem provers / functional programming languages (e.g., Isabelle, Coq, and Haskell), so this may be due to a difference between the communities. I would be curious to hear how others understand the term "metaprogramming" and "reflection" and why they do. New perspectives are always interesting!

For me it makes a lot of sense to use a vocabulary which is somewhat compatible with the vocabulary uses in other proof assistants rather than python or Java. Maybe there could be a warning sentence at the very beginning.

[Henrik Böving]

Patrick Massot said:

Sebastian, your my_assumption tactic looks really nice! It's very easy to read for someone knowning a bit of Lean 3 meta programming. The only confusing thing for me is let target ← getMainTarget which very weirdly mixes the two big classes of assignments in Lean 3: monadic ones using ... ← ... and regular ones using let ... := ....

Basically that difference doesn't exist anymore, all variable bindings are let nowadays, you can in fact even write let foo := ←bar which is equivalent to let foo ← bar

[Marc Huisinga]

Patrick Massot said:

Sebastian, your my_assumption tactic looks really nice! It's very easy to read for someone knowning a bit of Lean 3 meta programming. The only confusing thing for me is let target ← getMainTarget which very weirdly mixes the two big classes of assignments in Lean 3: monadic ones using ... ← ... and regular ones using let ... := ....

You can think of let ... ← ... as being a shorter notation for let ... := ← ..., e.g.

def foo : Reader Nat Nat := do
  let x := ← read
  let x' ← read
  return x + x'

[Henrik Böving]

In general the ← can go anywhere on a variable that is monadic, for example:

if ←foo then ←bar else foobar

[Patrick Massot]

Thanks Mark and Henrik! I should say that I have very mixed feelings about how much comparison with Lean 3 should be included in this kind of documentation. Maybe there should be dedicated subsections or appendices in each chapter in order to help people coming from Lean 3. But clearly it shouldn't be everywhere. One of the main reasons I came to Lean after briefly trying Coq was that all the SSReflect documentation was constantly referring to standard Coq, and I didn't want to first learn standard Coq and then unlearn it while learning SSReflect. We definitely don't want people to first learn Lean 3 in order to learn Lean 4.

[Henrik Böving]

I'd try to do that but the issue is that I'd have to learn Lean 3 for that first :D

[Sebastian Ullrich]

We might get proper docstrings when hovering over ←, return, etc. soon, which with LeanInk would also be displayed in an HTML version

[Jannis Limperg]

While better explanations in the book will certainly make things clearer (it's very young after all), I think there's no question that metaprogramming in Lean 4 is more complicated than in Lean 3. Off the top of my hat, new complications include:

• The MetaM/TermElabM/TacticM split (plus a couple minor monads on the side).
• The whole syntax layer, which in Lean 3 was -- from the tactic writer's point of view -- just a combinator-based parser and some annotations on a tactic's arguments.
• The sheer size of the API. Discoverability is much worse compared to Lean 3, where you can look at tactic.lean and have essentially the whole API.
• Below TacticM, the need to pass the current goal explicitly, using copious shadowing and withMVarContext.
• auxDecls (Sebastian's example above has a bug related to these and I've forgotten about them many times).

There are also many improvements and the new API is much more powerful, so I'm not complaining at all. But as usual, a more powerful API makes simple things harder and hard things possible. I think there might be value in a simpler API that's good enough for 80% of tactics.

Btw I'm currently writing more content for the MetaM chapter, starting with some stuff on computation.

[Sebastian Ullrich]

Other comments from reading that chapter:

• We will start by implementing tactics that compute in TacticM and then we shall see how some tactics can be implemented as macros.

  I would probably have went with the other order, top-down.

• This informs the elaborator that in the context of elaborating tactics, the piece of syntax admit must be elaborated as what we write to the right-hand-side of the => (we fill the ... with the body of the tactic).

  nit: The tactic is not named admit, and there are no ...

• sorryAx should probably be explained

elab "custom_sorry_2" : tactic => do
  let goal ← Lean.Elab.Tactic.getMainGoal
  let goal_declaration ← Lean.Meta.getMVarDecl goal
  let goal_type := goal_declaration.type
  Lean.Elab.admitGoal goal

I understand the educational goal, but it's a bit weird that half of the code is not even used. Perhaps there are better examples. Also style nitpicks here and throughout: snake case and overuse of namespaced names. I assume the latter are are intended for better understanding the code outside of an interactive environment, but to me it makes the code look overcrowded, and this is again something that LeanInk would solve.

TacticM = ReaderT Context $ StateRefT State TermElabM

This is the one place where I would expect namespaces: Tactic.Context/State

(H2 : 2 = 2): 2 = 2

nit: spacing here and elswhere

• We get the type of LocalDefinition by calling Lean.Meta.inferType on the local declaration's expression.

  Below you show that this is not necessary as there is LocalDefinition.type

• Until now, we've only performed read-like operations with the context. But what if we want to change it?
  In this section we will see how to change the order of goals [...]

  This first example looks misplaced, it does not change the context

• For this task, first we will need to use Lean.Elab.Tactic.withMainContext, which can run commands taking into consideration the entire goal state.

  This is just as relevant for the assumption-like tactic before. Indeed, it should be added to my implementation as well, at which point together with isAuxDecl it is basically the built-in implementation.

• We write this as a macro expansion, which expands the piece of syntax custom_sorry_macro into the piece of syntax sorry:

  Is this a good first example? Most people think of sorry as a term I would assume, not a tactic.

• Extensible Tactics by Macro Expansion

  It should be noted that tactic elaborators are equally extensible

• Here, a <;> b means "run tactic a, and apply "b" to each goal after running a".

  No, it means to apply b to each goal *produced by a. Thus the implementation needs an extra set of braces/focus:

`(tactic| { $a:tactic; all_goals $b:tactic })

("But what if a consumes more than one goal"? This is indeed an issue with the built-in implementation of <;> as well I'd say.)

• In fact, <;> itself is a tactic combinator.

  Did you mean "tactic macro"?

• One can create tactic syntax using the macro (tactic| ⋯).

  missing backtick

This is not meant as criticism, I like the overall structure and examples of the chapter.

[Arthur Paulino]

@Jannis Limperg thanks a lot! Are you building on top of the PR that @Siddhartha Gadgil wrote? I haven't looked at it yet (still in bed) but it will be easier if we don't need to clash content with merge conflicts

[Jannis Limperg]

I'll merge this PR, yes.

[Arthur Paulino]

Also thank you @Mac ! Please feel free to propose changes. You're clearly more experienced than me with these concepts from other languages

And thank you @Sebastian Ullrich ! Your input is invaluable

[Henrik Böving]

Patrick Massot said:

Now I'll list some more specific comments or suggestions. Page numbers refers to Julian's pdf at https://leanprover.zulipchat.com/user_uploads/3121/62PFBMZpXE_GWjK0Qi7ULQrn/Metaprogramming-in-Lean-4.pdf

• Page 3, the acronym AST is not defined anywhere.
• Page 5 is the first appearance of withStuff. At that point it's officially not meant to be understood, but later in MetaM chapter it is also not really explained.
• Page 13 and in many other places there are lists that are not rendered correctly. It works nicely where seen on https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/metam.md, but not in the pdf. Also in the pdf many comments go out of the page.
• Page 13, could you tell what N and M stand for in mkAppN and mkAppM? That would help remembering which one is which
• Page 19, in the last code block near the bottom, what are :10 and :11? I understand they refer to precedences. But are they actual Lean syntax or stuff you write to tell something to readers? The whole precedence thing really needs a lot of explanation. In Lean 3 they are rather difficult to understand and users need to understand them as soon as they want to define any notation. Sebastian told is a long time ago that they will be easier to understand in Lean 4, but they still requires a careful explanation. About notation, one very difficult part in Lean 3 is notation involving binders (using scoped). It would be nice to explicitly show examples of how it's done in Lean 4. I guess this is somewhere in the syntax chapter, but again having more mathematical examples would help immensely. For instance describing notations with binders for integrals. Or even the union examples from Sebastian's famous state of the union talk;
• Page 31, I cannot make any sense of the first sentence.
• Page 49, the first paragraph refers to admit that appears nowhere in the code

Regarding this state of the union talk, I took a look at this version on you tube https://www.youtube.com/watch?v=yAizjui7CKA but the sound is rather meh and the image is...well you can see the image, is there a better version available somewhere? Otherwise I guess I'll follow the sound and read the presentation as PDF next to the video.

[Henrik Böving]

(just watching with the described approach now)

[Mac]

Patrick Massot said:

For me it makes a lot of sense to use a vocabulary which is somewhat compatible with the vocabulary uses in other proof assistants rather than python or Java. Maybe there could be a warning sentence at the very beginning.

As Lean is part proof assistant, I can see that rational. However, it is also intending to be a general purpose language, and the book's intent seems to be a general introduction to metaprogramming Lean. Thus, it seems like it should try to be a smooth transition both for those coming from the theorem proving world and those coming from the general purpose programming world. Therefore, orienting its focus within both frames of reference and having examples from both spaces seems like worthwhile goal.

Also, I don't even know if the vocabulary currently used in the book is in fact more natural to the theorem proving community. For all I know, the current framing could be novel to both domains. I haven't delved into other theorem provers sufficiently to know how they define metaprogramming. I just know that it fell weird coming from my background (of Ruby, Python, C++, Java, JavaScript, and Haskell).

[Mac]

Arthur Paulino said:

Also thank you Mac ! Please feel free to propose changes. You're clearly more experienced than me with these concepts from other languages.

You're welcome! I might hopefully write-up with a few tweaks in the future. :pen:

[Arthur Paulino]

Dear all (Damiano's style!),

I want to seize the opportunity and sincerely thank everyone who's helped out so far. I cannot see any way of writing this book other than by collaboration: each of us is able to understand and structure some parts of the content, and together I believe we have a reasonable coverage of what metaprogramming in Lean 4 is about.

Some updates:

• @Siddhartha Gadgil and @Jannis Limperg have improved the MetaM chapter. It may not be perfect yet, but we've made some progress
• I've improved the intro chapter, being more explicit about the goal of the book and its structure
• I've also made some drastic changes to the chapter on tactics based on the feedback from @Sebastian Ullrich
• @Henrik Böving is working on the comments from @Patrick Massot (we'll ask for your feedback again soon, Patrick!)
• I've created an issue for the comments from @Dan Velleman. We'll review them after the MetaM chapter is more complete

The topic is broad and getting the level of details right is hard. Thus, we rely on more readers exposing what's confusing for them. So, if you read the book and don't understand something, please let us know!

There's a PDF link in the README (thank you @Julian Berman!):
https://github.com/arthurpaulino/lean4-metaprogramming-book

[Siddhartha Gadgil]

I made a tiny PR (inserting two blank lines) to hopefully fix a formatting issue.

[Alex Keizer]

First of all, I, too, want to thank everyone working on this tutorial. It really helps a lot in understanding how metaprogramming works.

As for my feedback:

• I agree with the earlier comments surrounding reflection being confusing coming from a general purpose programming background.

• Similarly, I'd argue most (general purpose) systems do metaprogramming in the same language (Java/C++/Rust). Maybe changing the wording of the introduction to "In most theorem provers, the meta-level activities are done in a different language". I'll concede this point is approaching nitpicking, though.

• The paragraph below the MonadQuotation code (page 41 of the pdf) is a bit confusing. I don't see where a "function of type Syntax -> m a" is being evaluated? I thought this was talking about withRef, but that seems to execute a monadic action with some given syntax. From the text I'd expect a function (Syntax -> m a) -> m a`

The topic I'd like to see covered a bit more is how parser/syntax-combinators interact with anti-quotations. For example, what is going in with $[$loc]? in this code

macro_rules
| `(tactic| clean $tac:tactic $[$loc:location]?) => `(tactic| $tac; simp only [clean] $[$loc]?)

But also, how do I use an ar : Array Syntax in an antiquotation where a delimited list of things is expected (I think that is $[ar]*, right)?

Finally, the section on hygiene might also want to clarify that if a macro expands to some def foo := "bar", foo is also subject to hygiene (this came unexpected for me, even after reading the macro hygiene paper, and is quite difficult to debug/realize by oneself), plus a note on how to circumvent hygiene for names that you do want to be accessible outside the macro scope (i.e., the mkIdent trick)

[Henrik Böving]

Thanks for the feedback, I opened an issue here: https://github.com/arthurpaulino/lean4-metaprogramming-book/issues/47, I'll get to the syntax/macro stuff in the coming days!

[Dan Velleman]

In the Tactics chapter, the FAQ section at the end gives an example illustrating how to access the local context. Here's a slightly modified version of the example:

elab "faq_get_hypotheses" : tactic => do
  let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
  ctx.forM (fun (decl : Lean.LocalDecl) => do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declType := decl.type -- Find the expression of the declaration.
    let declName := decl.userName -- Find the name of the declaration.
    dbg_trace f!" local decl: name: {declName} | expr: {declExpr} | type: {declType}"
  )

example (H1 : 1 = 1) (H2 : 2 = 2): 3 = 3 := by
  have H3 : 4 = 4 := rfl
  faq_get_hypotheses
  -- local decl: name: test_faq_get_hypotheses | expr: _uniq.10814 | type: ...
  -- local decl: name: H1 | expr: _uniq.10815 | type: ...
  -- local decl: name: H2 | expr: _uniq.10816 | type: ...
  rfl

The modification is that I have added have H3 : 4 = 4 := rfl before the invocation of faq_get_hypotheses. I was expecting to see the new hypothesis H3 in the output, but I didn't. Why? How do I get access to not only the original hypotheses, but also any new hypotheses that have been added?

[Arthur Paulino]

The issue is that a Lean.Elab.Tactic.withMainContext is missing. I'm fixing it right now. Will try to address more issues throughout this weekend.
Thanks for pointing that out!

[Horațiu Cheval]

At the end of the Expressions chapter,

We next consider the helper mkLambda to construct a simple function named cz which takes any natural number and returns Nat.zero

To me, this reads as if we were talking about some expression fun x : Nat => 0 to which we give the name cz.
Am I right that this is not intended and that we are talking about the expression fun cz : Nat => 0, in which the variable bound by fun is given the name cz?

[Henrik Böving]

Yes, that's a mistake in the explanation, in general an expression does not carry a name on its own.

[Arthur Paulino]

Yeah, sorry. mkLambda consumes a Lean.Name because we can give a name to the variable being bound:

import Lean

open Lean in
def constZero : Expr :=
  mkLambda `cz BinderInfo.default (mkConst ``Nat) (mkConst ``Nat.zero)

elab "testing" : term => return constZero

#check testing -- fun cz => Nat.zero : Nat → Nat

[Arthur Paulino]

I'm going to fix it right now. Thanks for pointing that out!

[Horațiu Cheval]

No problem, thanks for working on this!

[Arthur Paulino]

Hi everyone :wave:
Time for another update on the book!

• @Jannis Limperg has drastically improved the MetaM chapter
• @Henrik Böving has updated the book to use the new TSyntax API
• Many minor changes and fixes to address comments mentioned by the readers

To anyone interested, please give it another read to see if anything else needs a better explanation. This book is an important piece to empower the community to take more ownership of the Lean 3 => Lean 4 migration of mathlib :pray:

[Andrés Goens]

Nice! Thanks for keeping this up to date and make it easier to digest for the rest of us :)

[Patrick Massot]

Are the cheat-sheet and options chapter meant as appendices? If so then it's weird that pretty-printing come after them in the pdf.

[Patrick Massot]

The book seems toe 20 pages longer than the version I have. Is this a page layout artifact or does it really comes from new content?

[Henrik Böving]

The syntax and macro chapter got a little bit longer for sure, elaboration was not really touched, I can't speak for the rest...I guess a git diff would show but I don't know the commit you :printer: the book on /o\

[Arthur Paulino]

The MetaM chapter is a lot longer and more detailed :+1:

[Arthur Paulino]

Patrick Massot said:

Are the cheat-sheet and options chapter meant as appendices? If so then it's weird that pretty-printing come after them in the pdf.

No appendices. Maybe the cheat-sheet and the FAQ from the chapter on tactics can be unified into a single unit. The extra chapters are like "more things you can do with metaprogramming, but not as important"

[Patrick Massot]

Then I would expect the extras to be at the end. Or is pretty-printing also an extra?

[Arthur Paulino]

It's also an extra :+1:

[Arthur Paulino]

(or at least we've been considering it an extra. we're open to suggestions of course!)

[Patrick Massot]

Mathematicians certainly don't consider that having pretty printing is an extra.

[Patrick Massot]

But I don't know how much we need to know. Last time I checked the notation chapter didn't do any pretty-printing, but I know there have been some PRs improving the situation in the mean time.

[Henrik Böving]

The notation heuristic for pretty printing is pretty good now it will cover the vast majority of syntax. As soon as you want to pretty print stuff from macro or macro_rules etc. You'll have to consider the pretty printing chapter.

[Moritz Doll]

Hi,
I have read through the tactics chapter and I found it really nice. Some minor complains were

• sometimes there are unused variables in the example code (for instance goal in custom_assump_0)
• you sometimes use Lean.Elab.Tactic.getMainTarget and sometimes goalDecl.type to get the goalType and I don't see the difference and it is not explained in the text (I changed it in one example from one to the other and it just worked).
• in custom_assump_2 in the end there should not be a line break (isn't there some fancy unicode symbol suggesting that the line should not break in the code)
• in custom_let I would have liked some explanation to what elabTerm does (the explanation seems to be in the introduction examples, where it says that I don't have to understand the details)

I have not read the other chapters and except for the 'Tweaking the context' chapter that just worked fine for me. I guess that will change if more fancy stuff gets done in the tactics chapter.

[Henrik Böving]

The process of elabTerm is explained (well not fully explained, large parts of the compiler are related to elabTerm but the general idea) in the elaboration chapter. In general if you want to read the tactic chapter you are expected to have read at leats:

• Expr
• MetaM
• Syntax
• Macro
• Elaboration

[Mario Carneiro]

• you sometimes use Lean.Elab.Tactic.getMainTarget and sometimes goalDecl.type to get the goalType and I don't see the difference and it is not explained in the text (I changed it in one example from one to the other and it just worked).

These are equivalent. If you already have the goal decl then probably callling .type is easier, but if you only need the type and not the goal itself then getMainTarget does both parts.

• in custom_assump_2 in the end there should not be a line break (isn't there some fancy unicode symbol suggesting that the line should not break in the code)

I wasn't able to work out where you are referring to. I don't see anything in this example that goes against the usual formatting or would be an error.

[Moritz Doll]

oh, I forgot a tab, I did not know that they had any meaning.

[Moritz Doll]

Henrik Böving said:

The process of elabTerm is explained (well not fully explained, large parts of the compiler are related to elabTerm but the general idea) in the elaboration chapter. In general if you want to read the tactic chapter you are expected to have read at leats:

• Expr
• MetaM
• Syntax
• Macro
• Elaboration

I briefly looked into the elaboration chapter, but I did not find anything about the specific functions elabTerm and elabTermEnsuringType. I agree that for a understanding of tactics one has to read more, but I just wanted a brief peak into how tactic-writing works

[Henrik Böving]

it uses elabTerm in the end once, though we could probably explicitly mention its meaning. In general it is the entry point to the term elaboration process as the name suggests. And that process is explained in the elaboration chapter.

[Arthur Paulino]

@Moritz Doll thanks! I've added a brief explanation for the unused goal variable

[Moritz Doll]

thanks Arthur. One more thing: the difference between Lean.Meta.assert and Lean.Meta.define is not explained in the text.

[Arthur Paulino]

This is an open question: how much should we go into detail?
At this point, ctrl+clicking on them should take you to their definitions in core and there you should be able to see their docstrings and implementations, which will definitely be more instructive and precise.

In the intro chapter we state the goal of the book, which is not to provide a detailed notion of the API. Instead, we're trying to situate the reader and provide a bigger picture of what metaprogramming in Lean 4 is. We hope to provide enough context so the reader can explore the core code as well as understand what's already written in Mathlib4 without the same overwhelming experience I had in the past

[Arthur Paulino]

This is a hard compromise because ctrl+click is obviously not an option for those who are reading the book from a md, pdf or html. Maybe I should state in the intro chapter that cloning the repo and exploring the Lean files is encouraged for those who want to go into more details with the help of the go-to-definition functionality

[Sebastian Ullrich]

We do have docstrings in LeanInk HTML output

[Mac]

Arthur Paulino said:

This is a hard compromise because ctrl+click is obviously not an option for those who are reading the book from a md, pdf or html.

Also, is couldn't you also hyperlink method definitions in the PDF output as well? The only case where this seems impossible is for people who print out the book.

[Arthur Paulino]

It sounds like a lot of work to get everything wired for that. Maybe it's about time we migrate to LeanInk

[Kevin Buzzard]

I'm trying to read the metaprogramming book as preparation for next week.

In the DSL example there are Arith.symbols in commented out claimed #check outputs, but I get Arith.vals in the actual output. Furthermore for #check ⟪ "x" * "y" + "z" ⟫ -- precedence I get a different answer, the :75 seems to have no effect (changing it and adding 75 to other choices didn't seem to do anything?)

In this section I don't see all the big numbers in the #eval output.

[Sebastian Ullrich]

https://leanprover.github.io/lean4/doc/metaprogramming-arith.html has a correct version of the Arith grammar

[Arthur Paulino]

@Kevin Buzzard did you clone the book repo? I am suspecting that you are using a different toolchain

[Arthur Paulino]

I'm going to check it on my machine again in a few minutes

[Kevin Buzzard]

I didn't do any repo-cloning, I was literally reading the markdown files I linked to.

[Kevin Buzzard]

I googled, found the github repo with a bunch of links in the README and just started. What is the correct way to read the book?

[Arthur Paulino]

I see. The API has changed recently. Expr no longer carries metadata as it used to. I might just update the book to the newest toolchain

[Kevin Buzzard]

Note that I'm not very good at computers. I'm just using a random recent lean4 I guess. It hadn't occurred to me that there was an exactly-right version.

[Arthur Paulino]

I see two ways of reading the book: you can use the markdown files or the PDF, but if you're willing to experiment with code then cloning the repo and tweaking the Lean files is better

[Arthur Paulino]

(to make sure you're on the same version that the text was written)

[Arthur Paulino]

Either way, I will try to update the book today. Let's see if I can find some time

[Kevin Buzzard]

OK so I have cloned the repo and typed lake build (I don't really have a clue what I'm doing) and then I open VS Code and go to lean.main.intro and on line 178/179 I see

#check ⟪ "x" * "y" + "z" ⟫ -- precedence
-- Arith.add (Arith.mul (Arith.symbol "x") (Arith.symbol "y")) (Arith.symbol "z")

and when I click on the #check I get the completely different

Arith.mul (Arith.var "x") (Arith.add (Arith.var "y") (Arith.var "z")) : Arith

Is my set-up wrong in some way? I don't know what I'm doing, so sorry if these questions are not so smart.

[Sebastian Ullrich]

No, that's an error in the book as I tried to imply

[Arthur Paulino]

Yeah that's an error. But the output of the #evals in the expression chapter should be as expected now

[Kevin Buzzard]

Speaking as someone who has never parsed a grammar in their life, when both the manual and the book claim to be parsing a "classic grammar", namely arithmetic expressions, does this just mean "a grammar known to Gauss" or does it mean something technical like "a grammar which involves some old rules which modern grammars don't have because the theory of grammars has now moved on"?

[Henrik Böving]

classical as in "it is usual to be used as an example here"

[Arthur Paulino]

I've just pushed a fix to the arith example in the intro chapter. Thanks for pointing it out Kevin!

[Kevin Buzzard]

I see plenty of evidence for this, given that the only two times I've ever read about parsing grammars are in the manual and the book, and both of them do this one :-)

[Kevin Buzzard]

Thanks Arthur! I will be pressing on with reading the book over the weekend. Wish me luck...

[Arthur Paulino]

If more contributors want access to push directly to master, please let me know. I'll be taking my family to a trip during this weekend so my spare time is limited for the next two days

[Henrik Böving]

Kevin Buzzard said:

Thanks Arthur! I will be pressing on with reading the book over the weekend. Wish me luck...

If you're at DSLs already you're almost through though right?

[Kevin Buzzard]

No I've only just started!

[Henrik Böving]

Are you reading in a weird order then? DSL is the 2nd last chapter, the proper order can be found in the README

[Arthur Paulino]

Okay I just pushed a commit updating the book to the latest toolchain (2022-07-16). @Kevin Buzzard please pull from master before continuing :+1:

[Arthur Paulino]

The chapter on expressions (the first one after the introductory chapter) was the most affected one

[Kevin Buzzard]

The DSL we are talking about is in a file called intro.md. Let me know which chapters I should have been reading before this one ;-)

[Henrik Böving]

Ahhh

[Kevin Buzzard]

DSLs looked pretty easy to me, it's rather heartening to know that they're supposed to be hard :-)

[Patrick Massot]

The very first example in the introduction also has an unused variable linter error:

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM `assertTypeCmd
    try
      let tp ← elabType typeStx
      let tm ← elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"

Variable tm is never used. How should this be written? Replacing tm by an underscore is accepted by the linter, but it looks weird.

[Patrick Massot]

In Lean 3 I guess I would write elabTermEnsuringType termStx tp >>= skip, but that doesn't seem to exist in Lean 4.

[Siddhartha Gadgil]

As far as I understand one should replace this by an underscore. The skip won't work because lean 4 has a hierarchy CoreM, MetaM , TermElabM, TacticM (somewhat analogous to semigroup, monoid, group, abelian group) and skip is at the tactic level.

[Patrick Massot]

Ok. Should I use let _ or _ alone?

[Patrick Massot]

In the tactic example of the introduction, it would help a bit to point out this is a reimplementation of suffices (or explain the difference with suffices if any)

[Siddhartha Gadgil]

I believe it should be let _. If the function returns a Unit in a monad then the let _ can be omitted.

[Patrick Massot]

I mean that both seem to work, but it's unclear if one is better

[Siddhartha Gadgil]

Patrick Massot said:

I mean that both seem to work, but it's unclear if one is better

I don't know if there is a difference. My guess is that there is a macro that transforms one to the other so they will be equivalent.

[Mac]

Patrick Massot said:

Variable tm is never used. How should this be written? Replacing tm by an underscore is accepted by the linter, but it looks weird.

Another way would be to use discard :

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM `assertTypeCmd
    try
      let tp ← elabType typeStx
      discard <| elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"

[Arthur Paulino]

Some changes are now on master:

• Mentioned suffices in the intro chapter, as proposed by Patrick
• Used discard on the implementation of #assertType, as proposed by Mac
• Merged David's fix for replacing <|> by first | ... in the MetaM chapter (reference)
• Fixed the and_then tactic, whose problem was pointed out here

Thanks everyone for the observations!

[Chad McBride]

Where can I find a syntax guide for Axioms Examples, Theorems and so forth? So far what I see in the manual, there are good examples, but is there a syntax guide to go along with it?

[Arthur Paulino]

@Chad McBride do you mean to add those to the environment via metaprogramming instead of via the common axiom foo : bar syntax?

[Chad McBride]

Sorry, yes I sent this to the wrong group.

[Arthur Paulino]

Oh, that's not covered in the book yet and I think it's an important topic. I never tried to do it myself, but I believe you can not only access, but also modify the Environment with a custom command via CommandElabM

[Henrik Böving]

As above you can read the implementations of elaborators that are already there, e.g. the axiom one: https://github.com/leanprover/lean4/blob/f6b6b36f47909fe8a089c16efdb87372154e7efa/src/Lean/Elab/Declaration.lean#L78-L110

The thing that is actually adding the declaration is https://github.com/leanprover/lean4/blob/f6b6b36f47909fe8a089c16efdb87372154e7efa/src/Lean/Elab/Declaration.lean#L97-L104, the stuff above is responsible for figuring out the types, the stuff below does a little extra book keeping for special cases.

[Dan Velleman]

The MetaM chapter is now very good, but I have a few small suggestions:

1. At the beginning, after listing 4 monads, you say "These monads extend each other." This wording isn't very helpful. I assume what is meant is that each monad in the list extends those earlier in the list.
2. In the section "Tactic Communication via Metavariablers", you say that the first apply tactic generates three new metavariables, and then you say "Call these metavariables ?m2, ?m3 and ?b". This suggests that you are making up the names of the three metavariables, but in fact Lean must have made up the name ?b, because it occurs in ?m2 and ?m3. Is Lean in fact making up names for all of the metavariables? This confused me briefly. Also, later in this example, you say "the target of ?m3 is now f (f a) = a", but I think that's a typo; isn't the target of ?m3 now f a = a?
3. I think the explanation of forallMetaTelescope, forallMetaTelescopeReducing, etc. is misleading. These functions don't take a computation as an argument, as forallTelescope does, do they? Rather, they return the result of replacing the bound variables with metavariables.

[Arthur Paulino]

Thanks! I'm creating an issue to keep track of those points

[Evgenia Karunus]

Some updates:

• I started adding exercises to the chapters, we now have exercises and solutions for Expressions and MetaM chapters (issue #84, PR #85).
• Pdf is generated upon every push to PR now, too (not only upon every push to master) (PR #86).

[Evgenia Karunus]

Added exercises for Ch.Syntax & Ch.Elaboration, would someone take a look at the PR please? @Henrik Böving /@Jannis Limperg?

[Henrik Böving]

Left a review on the syntax part

[Evgenia Karunus]

Thanks for the review @Henrik Böving!

macro_rules is also not introduced here yet, in general it is pretty hard to give nice examples for non trivial syntax without using stuff from chapters to come after the syntax chapter.

About using stuff that hasn't been introduced yet - I do this across all exercises actually, yes.
That's intentional - when I was reading the book chapter to chapter, I couldn't actually properly play with the introduced concepts, because there is no mechanism by which I could build up a fully functional example, bottom-up approach doesn't really work if the low-level concepts are not self-encompassing. In fact I had to port some tactics before I could proceed with the book. So I've been using concepts we haven't yet learned in exercises to try and give a bigger picture of how the concepts fit together/how you can play with them.

[Evgenia Karunus]

The perfect solution to this is to have an introductory chapter that gives the overview of metaprogramming in Lean & the explanation of how to use [shallowly, without details] the main building blocks (syntax, macro, elab). I can write it up, but I'm afraid it might be a bit misguided bc I just learned a lot of this.

I created a description of what I gather though, mb if someone could review & if it's generally sensible I could rewrite it a bit & add it to the introduction chapter https://lakesare.brick.do/metaprogramming-in-lean-BEwZboNyq9ZO.

[Arthur Paulino]

Images!!

[Sebastian Ullrich]

This looks very nice. From a cursory glance though it feels inconsistent that you primarily use macro for macros, but not elab for elaborators. And notations etc. are macros, not elaborators.

[Evgenia Karunus]

@Sebastian Ullrich,

inconsistent that you primarily use macro for macros, but not elab for elaborators.

Agreed, changed all instances of using macro to the no-syntax-sugar version.

And notations etc. are macros, not elaborators.

Thanks, fixed.

[Arthur Paulino]

The exercises that @Evgenia Karunus added have been merged into master. Make sure to redownload the book if you're reading it :pray:

https://github.com/arthurpaulino/lean4-metaprogramming-book/

[Evgenia Karunus]

Some updates:

• added the "Overview" chapter (https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/99)
• added exercises for the "Tactics" chapter (https://github.com/arthurpaulino/lean4-metaprogramming-book/pull/98).

Would someone take a look at the PRs please?

---

Update: "Overview" chapter reviewed & merged

[Arthur Paulino]

Hello everyone! Since I haven't had the time to maintain the book as I used to, I've been thinking about moving the https://github.com/arthurpaulino/lean4-metaprogramming-book to either the leanprover or the leanprover-community organizations.

What do you folks think? Is there anyone who would like to take ownership of this front?

[Mario Carneiro]

I think it would be better to move it to leanprover-community, I think it is more likely to get maintenance there

[Scott Morrison]

@Arthur Paulino, I've just sent you an invitation to the leanprover-community organization, which should grant you the necessary rights to transfer your repository into the organization.

[Arthur Paulino]

It's done: https://github.com/leanprover-community/lean4-metaprogramming-book
:octopus:

[Kevin Buzzard]

Thanks once again for writing it! It is because of the efforts of people like you and others who have written basic documentation on this very new language, that we are able to grow as a community

[Johan Commelin]

I've decided that I should really learn more metaprogramming. So I'm reading through the book. I noticed that I find it helpful to read it directly in VScode, so that I can test out things immediately.
For that reason, I've created a PR that prefixes all filenames with their section number, so that the files appear in order in the VScode file browser.

[Johan Commelin]

Relatedly, I'm wondering, would people be happy if I reformat all the text so that it has < 100 chars/line?
I'm also happy with switching on word-wrapping Alt-Z when needed.

[Johan Commelin]

/poll How should we format the text in this book

• Please leave it like it is: arbitrary line length
• Lines should be < 100 chars, otherwise fill as much text on a line as possible
• Use semantic linebreaks, that way changes to the text result in meaningful git diffs

[Johan Commelin]

semantic linebreaks

[Johan Commelin]

Here is a first PR: https://github.com/leanprover-community/lean4-metaprogramming-book/pull/110

The only content is in the whitespace changes.

[Scott Morrison]

This is a bit off topic, but the unanimity of that vote suggests that maybe we should endorse semantic linebreaking in Mathlib! I've always used semantic linebreaks in comments that I write, but as there is a big mix of styles at present I've resisted the temptation to reflow existing text. :-)

[Johan Commelin]

I would be in favour!

[Arthur Paulino]

Scott Morrison said:

This is a bit off topic, but the unanimity of that vote suggests that maybe we should endorse semantic linebreaking in Mathlib! I've always used semantic linebreaks in comments that I write, but as there is a big mix of styles at present I've resisted the temptation to reflow existing text. :-)

Going offtopic with you: it's probably worth making a poll about that. AFAIK, semantic linebreaking is not much of a consensus in docstrings as it is in pure text files like markdown

[Eric Wieser]

Johan Commelin said:

For that reason, I've created a PR that prefixes all filenames with their section number, so that the files appear in order in the VScode file browser.

I think this has broken some links in the table of contents

[Julian Berman]

Can you share which, I thought I fixed all of those

[Evgenia Karunus]

Who's able to overview/merge PRs now that the book is in leanprover-community?
I just fixed all merge conflicts in /pull/98 and it would be nice to merge, /pull/109 should certainly be merged, /pull/112, /pull/111 are good to go too.

[Henrik Böving]

I'll review 98 again.

109 still has conflicts, 112 and 111 don't follow the markdown vs Lean guide from the README

[Johan Commelin]

The very weird thing is that locally in a fresh clone git claims that there aren't any conflicts between 109 and master

[Johan Commelin]

On July 13 I pushed

commit 773195ab9ec23d3e58237cc9f83badfbfcbad06f (HEAD -> 02-grammarly, origin/02-grammarly)
Merge: e60e547 545eb0a
Author: Johan Commelin <johan@commelin.net>
Date:   Thu Jul 13 14:55:48 2023 +0000

    Merge branch 'master' into 02-grammarly

[Johan Commelin]

But the GH UI isn't picking up on this commit

[Julian Berman]

I'm going to merge 109, it seems fine.

[Julian Berman]

I'm going to merge 106 too, which I left for you to merge I think Johan (or else I never asked how many reviewers you folks wait for there) but seems like that one too seems good still.

[Julian Berman]

Also merging 102 which I manually confirmed locally and seems pretty trivial.

[Jim Fowler]

I have found this book really helpful: following the book, I can take a Lean.Expr for a user-provided constant and I can use Lean.Meta.inferType from inside the MetaM monad, which I can run from IO. The goal is to add links to definitions in mathlib from https://topology.pi-base.org/ and verify that the labels are actually properties of topological spaces. (Maybe this isn't really the right way to do this.)

Given a name of a theorem, lemma, etc., I'd like to know the filename in which that name is defined.

[Kevin Buzzard]

You can hover over it if you can see it in VS Code and it says in small letters at the bottom. If you can't see it, you can search for it

[Arthur Paulino]

I think he means to do this programatically, for a bunch of declarations (definitions, theorems, types etc)

[Arthur Paulino]

@Jim Fowler if I understood you correctly, doc-gen4 probably implements a superset of what you need

[Jim Fowler]

Yes, programatically -- I will take a look at doc-gen4. Thank you!