using mdgen instead of lean2md

.gitignore

@@ -1,2 +1,2 @@
 /build
-/lean_packages
+.lake/

README.md

@@ -34,16 +34,13 @@ Sources to extract material from:
 
 ## Contributing
 
-The markdown files are generated automatically via [lean2md](https://github.com/arthurpaulino/lean2md).
+The markdown files are generated automatically via [mdgen](https://github.com/Seasawher/mdgen).
 Thus, if you're going to write or fix content for the book, please do so in the original Lean files inside the [lean](lean) directory.
 
-**Important**: since `lean2md` is so simple, please avoid using comment sections
+**Important**: since `mdgen` is so simple, please avoid using comment sections
 in Lean code blocks with `/- ... -/`. If you want to insert commentaries, do so
 with double dashes `--`.
 
 ### Building the markdown files
 
-This is not required, but if you want to build the markdown files, you can do so by running `lake run build`.
-It requires having Python installed, as well as the `lean2md` package.
-
-Or, if you have [viper](https://github.com/arthurpaulino/viper) installed and a linked environment that has `lean2md`, you can call `lake run viper_build`.
+This is not required, but if you want to build the markdown files, you can do so by running `lake exe mdgen lean md`.

lake-manifest.json

@@ -0,0 +1,14 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/Seasawher/mdgen",
+   "type": "git",
+   "subDir": null,
+   "rev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "name": "mdgen",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«lean4-metaprogramming-book»",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -8,6 +8,9 @@ lean_lib «lean4-metaprogramming-book» where
   roots := #[`cover, `extra, `main, `solutions]
   globs := #[Glob.one `cover, Glob.submodules `extra, Glob.submodules `main, Glob.submodules `solutions]
 
+require mdgen from git
+  "https://github.com/Seasawher/mdgen" @ "c501f6b8fa2502362bf94678d404857e46e2b65d"
+
 def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   let out ← IO.Process.output {
     cmd := cmd
@@ -19,21 +22,5 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   return hasError
 
 script build do
-  let _ ← runCmd "rm" #["-rf", "md"]
-
-  if ← runCmd "python3" #["-m", "lean2md", "lean", "md"] then return 1
-  if ← runCmd "python3" #["-m", "lean2md", "lean/main", "md/main"] then return 1
-  if ← runCmd "python3" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1
-  if ← runCmd "python3" #["-m", "lean2md", "lean/solutions", "md/solutions"] then return 1
-
-  return 0
-
-script viper_build do
-  let _ ← runCmd "rm" #["-rf", "md"]
-
-  if ← runCmd "viper" #["-m", "lean2md", "lean", "md"] then return 1
-  if ← runCmd "viper" #["-m", "lean2md", "lean/main", "md/main"] then return 1
-  if ← runCmd "viper" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1
-  if ← runCmd "viper" #["-m", "lean2md", "lean/solutions", "md/solutions"] then return 1
-
+  if ← runCmd "lake exe mdgen" #["lean", "md"] then return 1
   return 0

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-12-16
+leanprover/lean4:v4.4.0

md/main/01_intro.md

@@ -6,8 +6,8 @@ This book aims to build up enough knowledge about metaprogramming in Lean 4 so
 you can be comfortable enough to:
 
 * Start building your own meta helpers (defining new Lean notation such as `∑`,
-building new Lean commands such as `#check`, writing your own tactics such as `use`, etc.)
-* Read and discuss metaprogramming API's like the ones in Lean 4 core and
+building new Lean commands such as `#check`, writing tactics such as `use`, etc.)
+* Read and discuss metaprogramming APIs like the ones in Lean 4 core and
 Mathlib4
 
 We by no means intend to provide an exhaustive exploration/explanation of the
@@ -30,11 +30,11 @@ dependency structure is as follows:
 * "Elaboration" builds on top of "`Syntax`" and "`MetaM`"
 * "`MetaM`" builds on top of "Expressions"
 
-After the chapter on tactics, you find a cheat-sheet containing a wrap-up of key
+After the chapter on tactics, you find a cheat sheet containing a wrap-up of key
 concepts and functions. And after that, there are some chapters with extra
-content, showing other applications of metaprogramming in Lean 4. Most chapters contain exercises in the end of the chapter - and in the end of the book you will have full solutions to those exercises.  
+content, showing other applications of metaprogramming in Lean 4. Most chapters contain exercises at the end of the chapter - and at the end of the book you will have full solutions to those exercises.
 
-The rest of this chapter is a gentle introduction for what metaprogramming is,
+The rest of this chapter is a gentle introduction to what metaprogramming is,
 offering some small examples to serve as appetizers for what the book shall
 cover.
 
@@ -60,21 +60,21 @@ and Scala. In Coq, it's OCaml. In Agda, it's Haskell. In Lean 4, the meta code i
 mostly written in Lean itself, with a few components written in C++.
 
 One cool thing about Lean, though, is that it allows us to define custom syntax
-nodes and to implement our own meta-level routines to elaborate those in the
+nodes and implement meta-level routines to elaborate them in the
 very same development environment that we use to perform object-level
-activities. So for example, one can write their own notation to instantiate a
+activities. So for example, one can write notation to instantiate a
 term of a certain type and use it right away, in the same file! This concept is
 generally called
 [__reflection__](https://en.wikipedia.org/wiki/Reflective_programming). We can
 say that, in Lean, the meta-level is _reflected_ to the object-level.
 
 If you have done some metaprogramming in languages such as Ruby, Python or Javascript,
-it probably took a form of making use of predefined metaprogramming methods in order to define
+it probably took the form of making use of predefined metaprogramming methods to define
 something on the fly. For example, in Ruby you can use `Class.new` and `define_method`
 to define a new class and its new method (with new code inside!) on the fly, as your program is executing.
 
 We don't usually need to define new commands or tactics "on the fly" in Lean, but spiritually
-similar feats are possible with Lean metaprogramming, and are equally straightforward, e.g. you can define
+similar feats are possible with Lean metaprogramming and are equally straightforward, e.g. you can define
 a new Lean command using a simple one-liner `elab "#help" : command => do ...normal Lean code...`.
 
 In Lean, however, we will frequently want to directly manipulate
@@ -85,15 +85,15 @@ a large chunk of this book is contributed to studying these types and how we can
 
 ## Metaprogramming examples
 
-Next, we introduce a number of examples of Lean metaprogramming, so that you start getting a taste for
+Next, we introduce several examples of Lean metaprogramming, so that you start getting a taste for
 what metaprogramming in Lean is, and what it will enable you to achieve. These examples are meant as
-mere illustration - do not worry if you don't understand the details for now.
+mere illustrations - do not worry if you don't understand the details for now.
 
 ### Introducing notation (defining new syntax)
 
 Often one wants to introduce new notation, for example one more suitable for (a branch of) mathematics. For instance, in mathematics one would write the function adding `2` to a natural number as `x : Nat ↦ x + 2` or simply `x ↦ x + 2` if the domain can be inferred to be the natural numbers. The corresponding lean definitions `fun x : Nat => x + 2` and `fun x => x + 2` use `=>` which in mathematics means _implication_, so may be confusing to some.
 
-We can introduce notation using a `macro` which transforms our syntax to lean's own syntax (or syntax we previously defined). Here we introduce the `↦` notation for functions.
+We can introduce notation using a `macro` which transforms our syntax to Lean's syntax (or syntax we previously defined). Here we introduce the `↦` notation for functions.
 
 ```lean
 import Lean
@@ -133,21 +133,21 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
 #assertType [] : Nat -- failure
 ```
 
-We started by using `elab` to define a `command` syntax, which, when parsed
-by the compiler, will trigger the incoming computation.
+We started by using `elab` to define a `command` syntax. When parsed
+by the compiler, it will trigger the incoming computation.
 
 At this point, the code should be running in the `CommandElabM` monad. We then
 use `liftTermElabM` to access the `TermElabM` monad, which allows us to use
-`elabType` and `elabTermEnsuringType` in order to build expressions out of the
+`elabType` and `elabTermEnsuringType` to build expressions out of the
 syntax nodes `typeStx` and `termStx`.
 
-First we elaborate the expected type `tp : Expr` and then we use it to elaborate
-the term expression, which should have the type `tp` otherwise an error will be
-thrown. The term expression itself doesn't matter to us here, as we're calling
+First, we elaborate the expected type `tp : Expr`, then we use it to elaborate
+the term expression. The term should have the type `tp` otherwise an error will be
+thrown. We then discard the resulting term expression, since it doesn't matter to us here - we're calling
 `elabTermEnsuringType` as a sanity check.
 
 We also add `synthesizeSyntheticMVarsNoPostponing`, which forces Lean to
-elaborate metavariables right away. Without that line, `#assertType 5  : ?_`
+elaborate metavariables right away. Without that line, `#assertType [] : ?_`
 would result in `success`.
 
 If no error is thrown until now then the elaboration succeeded and we can use

md/main/02_overview.md

@@ -12,34 +12,34 @@ Metaprogramming in Lean is deeply connected to the compilation steps - parsing,
 >
 > Leonardo de Moura, Sebastian Ullrich ([The Lean 4 Theorem Prover and Programming Language](https://pp.ipd.kit.edu/uploads/publikationen/demoura21lean4.pdf))
 
-Lean compilation process can be summed up in the following diagram:
+The Lean compilation process can be summed up in the following diagram:
 
 <p align="center">
 <img width="700px" src="https://github.com/arthurpaulino/lean4-metaprogramming-book/assets/7578559/78867009-2624-46a3-a1f4-f488fd25d494"/>
 </p>
 
-First we will have Lean code as a string. Then `Syntax` object. Then `Expr` object. Then we can execute it.  
+First, we will start with Lean code as a string. Then we'll see it become a `Syntax` object, and then an `Expr` object. Then finally we can execute it.  
 
 So, the compiler sees a string of Lean code, say `"let a := 2"`, and the following process unfolds:
 
 1. **apply a relevant syntax rule** (`"let a := 2"` ➤ `Syntax`)  
 
-    During the parsing step, Lean tries to match a string of Lean code to one of the declared **syntax rules** in order to turn that string into the `Syntax` object. **Syntax rules** are basically glorified regular expressions - when you write a Lean string that matches a certain **syntax rule**'s regex, that rule will be used to handle subsequent steps.
+    During the parsing step, Lean tries to match a string of Lean code to one of the declared **syntax rules** in order to turn that string into a `Syntax` object. **Syntax rules** are basically glorified regular expressions - when you write a Lean string that matches a certain **syntax rule**'s regex, that rule will be used to handle subsequent steps.
 
 2. **apply all macros in a loop** (`Syntax` ➤ `Syntax`)  
 
-    During the elaboration step, each **macro** simply turns the existing `Syntax` object into some new `Syntax` object. Then, the new `Syntax` is processed in a similar way (steps 1 and 2), until there are no more **macros** to apply.
+    During the elaboration step, each **macro** simply turns the existing `Syntax` object into some new `Syntax` object. Then, the new `Syntax` is processed similarly (repeating steps 1 and 2), until there are no more **macros** to apply.
 
 3. **apply a single elab** (`Syntax` ➤ `Expr`)  
 
-    Finally, it's time to infuse your syntax with meaning - Lean finds an **elab** that's matched to the appropriate **syntax rule** by the `:name` argument (**syntax rules**, **macros** and **elabs** all have this argument, and they must match). The newfound **elab** returns a particular `Expr` object.
+    Finally, it's time to infuse your syntax with meaning - Lean finds an **elab** that's matched to the appropriate **syntax rule** by the `name` argument (**syntax rules**, **macros** and **elabs** all have this argument, and they must match). The newfound **elab** returns a particular `Expr` object.
     This completes the elaboration step.
 
-Expression (`Expr`) is then converted to the executable code during the evaluation step - we don't have to specify that in any way, Lean compiler will handle that for us.
+The expression (`Expr`) is then converted into executable code during the evaluation step - we don't have to specify that in any way, the Lean compiler will handle doing so for us.
 
 ## Elaboration and delaboration
 
-Elaboration is a overloaded term in Lean, for example you can meet the following usage of the word "elaboration", which defines elaboration as *"taking a partially-specified expression and inferring what is left implicit"*:
+Elaboration is an overloaded term in Lean. For example, you might encounter the following usage of the word "elaboration", wherein the intention is *"taking a partially-specified expression and inferring what is left implicit"*:
 
 
 > When you enter an expression like `λ x y z, f (x + y) z` for Lean to process, you are leaving information implicit. For example, the types of `x`, `y`, and `z` have to be inferred from the context, the notation `+` may be overloaded, and there may be implicit arguments to `f` that need to be filled in as well.
@@ -54,9 +54,9 @@ We, on the other hand, just defined elaboration as the process of turning `Synta
 
 These definitions are not mutually exclusive - elaboration is, indeed, the transformation of `Syntax` into `Expr`s - it's just so that for this transformation to happen we need a lot of trickery - we need to infer implicit arguments, instantiate metavariables, perform unification, resolve identifiers, etc. etc. - and these actions can be referred to as "elaboration" on their own; similarly to how "checking if you turned off the lights in your apartment" (metavariable instantiation) can be referred to as "going to school" (elaboration).
 
-There also exists a process opposite to elaboration in Lean - it's called, appropriately enough, delaboration. During delaboration, `Expr` is turned into the `Syntax` object; and then the formatter turns it into a `Format` object, which can be displayed in Lean's infoview. Every time you log something to the screen, or see some output upon hovering over `#check`, it's the work of the delaborator.
+There also exists a process opposite to elaboration in Lean - it's called, appropriately enough, delaboration. During delaboration, an `Expr` is turned into a `Syntax` object; and then the formatter turns it into a `Format` object, which can be displayed in Lean's infoview. Every time you log something to the screen, or see some output upon hovering over `#check`, it's the work of the delaborator.
 
-Throughout this book you will see references to the elaborator; and in the "Extra: Pretty Printing" chapter you can read on delaborators.
+Throughout this book you will see references to the elaborator; and in the "Extra: Pretty Printing" chapter you can read about delaborators.
 
 ## 3 essential commands and their syntax sugars
 
@@ -66,7 +66,7 @@ Now, when you're reading Lean source code, you will see 11(+?) commands specifyi
 <img width="500px" src="https://github.com/arthurpaulino/lean4-metaprogramming-book/assets/7578559/9b83f06c-49c4-4d93-9d42-72e0499ae6c8"/>
 </p>
 
-In the image above, you see `notation`, `prefix`, `infix`, and `postfix` - all of these are combinations of `syntax` and `@[macro xxx] def ourMacro`, just like `macro`. These commands differ from `macro` in that you can only define syntax of particular form with them.
+In the image above, you see `notation`, `prefix`, `infix`, and `postfix` - all of these are combinations of `syntax` and `@[macro xxx] def ourMacro`, just like `macro`. These commands differ from `macro` in that you can only define syntax of a particular form with them.
 
 All of these commands are used in Lean and Mathlib source code extensively, so it's well worth memorizing them. Most of them are syntax sugars, however, and you can understand their behaviour by studying the behaviour of the following 3 low-level commands: `syntax` (a **syntax rule**), `@[macro xxx] def ourMacro` (a **macro**), and `@[command_elab xxx] def ourElab` (an **elab**).
 
@@ -81,7 +81,7 @@ This image is not supposed to be read row by row - it's perfectly fine to use `m
 If we write `#h "#explode"`, Lean will travel the `syntax (name := shortcut_h)` ➤ `@[macro shortcut_h] def helpMacro` ➤ `syntax (name := default_h)` ➤ `@[command_elab default_h] def helpElab` route.  
 If we write `#help "#explode"`, Lean will travel the `syntax (name := default_h)` ➤ `@[command_elab default_h] def helpElab` route.
 
-Note how the matching between **syntax rules**, **macros**, and **elabs** is done via the `name` attribute. If we used `macro_rules` or other syntax sugars, Lean would figure out the appropriate `name` attributes on its own.
+Note how the matching between **syntax rules**, **macros**, and **elabs** is done via the `name` argument. If we used `macro_rules` or other syntax sugars, Lean would figure out the appropriate `name` arguments on its own.
 
 If we were defining something other than a command, instead of `: command` we could write `: term`, or `: tactic`, or any other syntax category.  
 The elab function can also be of different types - the `CommandElab` we used to implement `#help` - but also `TermElab` and `Tactic`:  
@@ -180,8 +180,8 @@ example : True := by -- `example` is underlined in blue, outputting:
 Since the objects defined in the meta-level are not the ones we're most
 interested in proving theorems about, it can sometimes be overly tedious to
 prove that they are type correct. For example, we don't care about proving that
-a recursive function to traverse an expression is well founded. Thus, we can
+a recursive function to traverse an expression is well-founded. Thus, we can
 use the `partial` keyword if we're convinced that our function terminates. In
-the worst case scenario, our function gets stuck in a loop, Lean server crashes
-in VSCode, but the soundness of the underlying type theory implemented in kernel
+the worst-case scenario, our function gets stuck in a loop, causing the Lean server to crash
+in VSCode, but the soundness of the underlying type theory implemented in the kernel
 isn't affected.