Merge pull request #131 from Seasawher/using-check-failure

use `#check_failure` command to erase errors

Author: Julian

.github/workflows/ci.yml

@@ -0,0 +1,31 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: install elan
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain $(cat lean-toolchain)
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Cache dependencies
+        uses: actions/cache@v3
+        with:
+          path: .lake
+          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: lake build
+        run: lake build --quiet

lake-manifest.json

@@ -4,10 +4,19 @@
  [{"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
-   "rev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "rev": "2c641fe54d48a5d4adff3a78dbc4a50c5f76b0c0",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c501f6b8fa2502362bf94678d404857e46e2b65d",
+   "inputRev": "v1.3.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.7.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«lean4-metaprogramming-book»",

lakefile.lean

@@ -4,12 +4,15 @@ open Lake DSL
 package «lean4-metaprogramming-book» where
   srcDir := "lean"
 
+@[default_target]
 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"
+  "https://github.com/Seasawher/mdgen" @ "v1.3.0"
+
+require std from git "https://github.com/leanprover/std4" @ "v4.7.0"
 
 def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   let out ← IO.Process.output {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.7.0

lean/main/01_intro.lean

@@ -128,8 +128,13 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
       logInfo "success"
     catch | _ => throwError "failure"
 
-#assertType 5  : Nat -- success
-#assertType [] : Nat -- failure
+/-- info: success -/
+#guard_msgs in --#
+#assertType 5  : Nat
+
+/-- error: failure -/
+#guard_msgs in --#
+#assertType [] : Nat
 
 /-! We started by using `elab` to define a `command` syntax. When parsed
 by the compiler, it will trigger the incoming computation.

lean/main/04_metam.lean

@@ -127,7 +127,7 @@ assigns `?b := f a`. Assigned metavariables are not considered open goals, so
 the only goal that remains is `?m3`.
 
 Now the third `apply` comes in. Since `?b` has been assigned, the target of
-`?m3` is now `f (f a) = a`. Again, the application of `h` succeeds and the
+`?m3` is now `f a = a`. Again, the application of `h` succeeds and the
 tactic assigns `?m3 := h a`.
 
 At this point, all metavariables are assigned as follows:
@@ -1235,9 +1235,9 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
       ...
     ```
-4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.  
-  **a)** What would be the `type` and `userName` of metavariable `mvarId`?  
-  **b)** What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?  
+4. [**Metavariables**] Consider the theorem `red`, and tactic `explore` below.
+  **a)** What would be the `type` and `userName` of metavariable `mvarId`?
+  **b)** What would be the `type`s and `userName`s of all local declarations in this metavariable's local context?
   Print them all out.
 
     ```lean
@@ -1256,17 +1256,17 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       sorry
     ```
 5. [**Metavariables**] Write a tactic `solve` that proves the theorem `red`.
-6. [**Computation**] What is the normal form of the following expressions:  
-  **a)** `fun x => x` of type `Bool → Bool`  
-  **b)** `(fun x => x) ((true && false) || true)` of type `Bool`  
+6. [**Computation**] What is the normal form of the following expressions:
+  **a)** `fun x => x` of type `Bool → Bool`
+  **b)** `(fun x => x) ((true && false) || true)` of type `Bool`
   **c)** `800 + 2` of type `Nat`
 7. [**Computation**] Show that `1` created with `Expr.lit (Lean.Literal.natVal 1)` is definitionally equal to an expression created with `Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])`.
-8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.  
-  **a)** `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`  
-  **b)** `2 + 1 =?= 1 + 2`  
-  **c)** `?a =?= 2`, where `?a` has a type `String`  
-  **d)** `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type  
-  **e)** `2 + ?a =?= 3`  
+8. [**Computation**] Determine whether the following expressions are definitionally equal. If `Lean.Meta.isDefEq` succeeds, and it leads to metavariable assignment, write down the assignments.
+  **a)** `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`
+  **b)** `2 + 1 =?= 1 + 2`
+  **c)** `?a =?= 2`, where `?a` has a type `String`
+  **d)** `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type
+  **e)** `2 + ?a =?= 3`
   **f)** `2 + ?a =?= 2 + 1`
 9. [**Computation**] Write down what you expect the following code to output.
 
@@ -1300,14 +1300,14 @@ Notice that changing the type of the metavariable from `Nat` to, for example, `S
       let reducedExpr ← Meta.reduce constantExpr
       dbg_trace (← ppExpr reducedExpr) -- ...
     ```
-10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:  
-  **a)** not idiomatically, with loose bound variables  
-  **b)** idiomatically.  
+10. [**Constructing Expressions**] Create expression `fun x, 1 + x` in two ways:
+  **a)** not idiomatically, with loose bound variables
+  **b)** idiomatically.
   In what version can you use `Lean.mkAppN`? In what version can you use `Lean.Meta.mkAppM`?
 11. [**Constructing Expressions**] Create expression `∀ (yellow: Nat), yellow`.
-12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:  
-  **a)** not idiomatically, with loose bound variables  
-  **b)** idiomatically.  
+12. [**Constructing Expressions**] Create expression `∀ (n : Nat), n = n + 1` in two ways:
+  **a)** not idiomatically, with loose bound variables
+  **b)** idiomatically.
   In what version can you use `Lean.mkApp3`? In what version can you use `Lean.Meta.mkEq`?
 13. [**Constructing Expressions**] Create expression `fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)` idiomatically.
 14. [**Constructing Expressions**] What would you expect the output of the following code to be?

lean/main/05_syntax.lean

@@ -154,10 +154,12 @@ We can now write `MyTerm` in place of things like `1 + 1` and it will be
 it just means that the Lean parser can understand it:
 -/
 
-def Playground1.test := MyTerm
+#check_failure MyTerm
 -- elaboration function for 'termMyTerm' has not been implemented
 --   MyTerm
 
+/-! Note: `#check_failure` command allows incorrectly typed terms to be indicated without error. -/
+
 /-!
 Implementing this so-called "elaboration function", which will actually
 give meaning to this syntax in terms of Lean's fundamental `Expr` type,
@@ -182,7 +184,7 @@ scoped syntax "⊥" : term -- ⊥ for false
 scoped syntax "⊤" : term -- ⊤ for true
 scoped syntax:40 term " OR " term : term
 scoped syntax:50 term " AND " term : term
-#check ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
+#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
 
 end Playground2
 
@@ -203,9 +205,11 @@ syntax:50 boolean_expr " AND " boolean_expr : boolean_expr
 Now that we are working in our own syntax category, we are completely
 disconnected from the rest of the system. And these cannot be used in place of
 terms anymore:
--/
 
+```lean
 #check ⊥ AND ⊤ -- expected term
+```
+-/
 
 /-!
 In order to integrate our syntax category into the rest of the system we will
@@ -214,7 +218,7 @@ will re-embed it into the `term` category:
 -/
 
 syntax "[Bool|" boolean_expr "]" : term
-#check [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
+#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ### Syntax combinators
@@ -272,23 +276,25 @@ syntax binNumber := binDigit,+
 /-!
 Since we can just use named parsers in place of syntax categories, we can now easily
 add this to the `term` category:
--/
 
+```lean
 syntax "bin(" binNumber ")" : term
 #check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 #check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z'
+```
+-/
 
 syntax binNumber' := binDigit,* -- note the *
 syntax "emptyBin(" binNumber' ")" : term
-#check emptyBin() -- elaboration function hasn't been implemented but parsing passes
+#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 Note that nothing is limiting us to only using one syntax combinator per parser,
 we could also have written all of this inline:
 -/
 
 syntax "binCompact(" ("Z" <|> "O"),+ ")" : term
-#check binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 As a final feature, let's add an optional string comment that explains the binary
@@ -297,8 +303,8 @@ literal being declared:
 
 -- The (...)? syntax means that the part in parentheses is optional
 syntax "binDoc(" (str ";")? binNumber ")" : term
-#check binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
-#check binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ## Operating on Syntax
@@ -559,15 +565,15 @@ the bound variables, we refer the reader to the macro chapter.
 
 1. Create an "urgent minus 💀" notation such that `5 * 8 💀 4` returns `20`, and `8 💀 6 💀 1` returns `3`.
 
-    **a)** Using `notation` command.  
-    **b)** Using `infix` command.  
-    **c)** Using `syntax` command.  
+    **a)** Using `notation` command.
+    **b)** Using `infix` command.
+    **c)** Using `syntax` command.
 
     Hint: multiplication in Lean 4 is defined as `infixl:70 " * " => HMul.hMul`.
 
 2. Consider the following syntax categories: `term`, `command`, `tactic`; and 3 syntax rules given below. Make use of each of these newly defined syntaxes.
 
-    ```
+    ```lean
       syntax "good morning" : term
       syntax "hello" : command
       syntax "yellow" : tactic

lean/main/06_macros.lean

@@ -35,7 +35,7 @@ to indicate that "it doesn't feel responsible for this syntax". In this case
 it's merely used to fill a wildcard pattern that should never be reached anyways.
 
 However we can in fact register multiple macros for the same syntax this way
-if we desire, they will be tried one after another (the later registered ones have 
+if we desire, they will be tried one after another (the later registered ones have
 higher priority)  -- is "higher" correct?
 until one throws either a real error using `Macro.throwError` or succeeds, that
 is it does not `Macro.throwUnsupported`. Let's see this in action:
@@ -169,7 +169,7 @@ for example macro creating macros, we can escape the anti quotation using: `` `(
 If we want to specify the syntax kind we wish `x` to be interpreted as
 we can make this explicit using: `` `($x:term) `` where `term` can be
 replaced with any other valid syntax category (e.g. `command`) or parser
-(e.g. `ident`). 
+(e.g. `ident`).
 
 So far this is only a more formal explanation of the intuitive things
 we've already seen in the syntax chapter and up to now in this chapter,
@@ -198,11 +198,11 @@ For example:
 -/
 
 -- syntactically cut away the first element of a tuple if possible
-syntax "cut_tuple " "(" term ", " term,+ ")" : term 
+syntax "cut_tuple " "(" term ", " term,+ ")" : term
 
 macro_rules
   -- cutting away one element of a pair isn't possible, it would not result in a tuple
-  | `(cut_tuple ($x, $y)) => `(($x, $y)) 
+  | `(cut_tuple ($x, $y)) => `(($x, $y))
   | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*))
 
 #check cut_tuple (1, 2) -- (1, 2) : Nat × Nat
@@ -225,7 +225,7 @@ we know so far we'd have to write two `macro_rules` now, one for the case
 with, one for the case without the optional argument. However the rest
 of the syntactic translation works exactly the same with and without
 the optional argument so what we can do using a splice here is to essentially
-define both cases at once: 
+define both cases at once:
 -/
 
 macro_rules
@@ -410,8 +410,8 @@ macro_rules
   -- in this case `error_position`, giving it the name `tk`
   | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh")
 
-#eval error_position all -- the error is indicated at `error_position all`
-#eval error_position first -- the error is only indicated at `error_position`
+#check_failure error_position all -- the error is indicated at `error_position all`
+#check_failure error_position first -- the error is only indicated at `error_position`
 
 /-
 Obviously controlling the positions of errors in this way is quite important

lean/main/07_elaboration.lean

@@ -173,7 +173,7 @@ elab "#findCElab " c:command : command => do
 /-!
 TODO: Maybe we should also add a mini project that demonstrates a
 non # style command aka a declaration, although nothing comes to mind right now.
-TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that 
+TODO:  Define a `conjecture` declaration, similar to `lemma/theorem`, except that
 it is automatically sorried.  The `sorry` could be a custom one, to reflect that
 the "conjecture" might be expected to be true.
 -/
@@ -260,7 +260,7 @@ this information to complete elaboration.
 We can also easily provoke cases where this does not work out. For example:
 -/
 
-#check set_option trace.Elab.postpone true in List.foldr .add
+#check_failure set_option trace.Elab.postpone true in List.foldr .add
 -- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
 -- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
   -- ?m.5808 → ?m.5809 → ?m.5809
@@ -316,7 +316,7 @@ def myanonImpl : TermElab := fun stx typ? => do
   -- Term elaborators can only postpone execution once, so the elaborator
   -- doesn't end up in an infinite loop. Hence, we only try to postpone it,
   -- otherwise we may cause an error.
-  tryPostponeIfNoneOrMVar typ? 
+  tryPostponeIfNoneOrMVar typ?
   -- If we haven't found the type after postponing just error
   let some typ := typ? | throwError "expected type must be known"
   if typ.isMVar then
@@ -328,17 +328,17 @@ def myanonImpl : TermElab := fun stx typ? => do
   elabTerm stx typ -- call term elaboration recursively
 
 #check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
-#check ⟨⟨1, sorry⟩⟩ -- expected type must be known
-#check (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
-#check (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
+#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known
+#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
+#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
 
 /-!
 As a final note, we can shorten the postponing act by using an additional
 syntax sugar of the `elab` syntax instead:
 -/
 
 -- This `t` syntax will effectively perform the first two lines of `myanonImpl`
-elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do 
+elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
   sorry
 
 
@@ -377,8 +377,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **a)** using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`.
+    **b)** using `syntax` + `elab_rules`.
     **c)** using `elab`.
 
 3. Here is some syntax taken from a real mathlib tactic `nth_rewrite`.
@@ -392,8 +392,8 @@ elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
 
     Please add these semantics:
 
-    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.  
-    **b)** using `syntax` + `elab_rules`.  
+    **a)** using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
+    **b)** using `syntax` + `elab_rules`.
     **c)** using `elab`.
 
 -/