Improve check_examples and pass them

lean4/examples/Branch.lean

@@ -5,7 +5,7 @@ open Lean Meta Elab Command Tactic
 
 /-!
   Inspired by
-  
+
   - [`Lean.Elab.Tactic.focus`](https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Basic.html#Lean.Elab.Tactic.focus)
   - [`Branch` in lean4game](https://github.com/leanprover-community/lean4game/blob/main/server/GameServer/Commands.lean), see also [its doc](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#proof)
   - [`tada` on Zulip`](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Lean.203.20or.204.3F/near/394490716)
@@ -49,7 +49,7 @@ elab (name := proof) "proof" _n:(num)? _desc:interpolatedStr(term)? ":" t:tactic
     -- else use the last proof as the proof
     -- TODO this doesn't guarantee that the whole theorem is proven if any of the proofs are valid
     -- it also doesn't guarantee that the whole theorem is proven only if all of the proofs are valid
-    
+
     pure a
 
 elab (name := QED) "QED" : tactic => do
@@ -73,6 +73,14 @@ example (a b c : ℕ) : a + b * c = c * b + a := by
   proof 2:
     ring
 
+-- to see the colorful effect, comment out #guard_msgs in
+/--
+warning: proof uses 'sorry'
+---
+error: unsolved goals
+⊢ 2 + 1 = 3
+-/
+#guard_msgs in
 theorem ex : 1 + 2 = 3 := by
   proofs 5
   proof "trivial":

lean4/examples/Zulip/Arrow.lean → lean4/examples/NoCI/Arrow.lean

@@ -1,4 +1,5 @@
 import Lean
+import Std.Tactic.GuardMsgs
 open Lean System
 
 /-!
@@ -42,6 +43,12 @@ def works₂ : IO String := do
 /-!
   ### Case `let var := if let` gives `unknown identifier`
 -/
+
+
+/--
+error: unknown identifier 'opt'
+-/
+#guard_msgs in
 def oops₀ : IO String := do
   let var := if let some opt := getOpt "str" then
     let ret := (<- getIO opt)  -- unknown identifier 'opt'
@@ -58,13 +65,27 @@ def oops₀ : IO String := do
 
   #### 1.1 expect `<-`, misuse `:=`, gives `unknown identifier`
 -/
+/--
+error: unknown identifier 'ret'
+-/
+#guard_msgs in
 def oops₁₁ : IO String := do
   let some ret := getOptIO "str"
   ret -- unknown identifier 'ret'
 
 /-!
   #### 1.2 expect `<-`, misuse `:=`, gives `type mismatch`
 -/
+
+/--
+error: type mismatch
+  some ret
+has type
+  Option ?m.2842 : Type
+but is expected to have type
+  IO (Option String) : Type
+-/
+#guard_msgs in
 def oops₁₂ : IO String := do
   let some ret := getOptIO "str" | pure "none" -- type mismatch: `IO (Option String)` got `Option ?m.2842`
   pure ret
@@ -80,13 +101,24 @@ def works₁₃ : IO String := do
 /-!
   ### Variant 2. expect `:=`, misuse `<-`, gives `type mismatch`
 -/
+
+/--
+error: type mismatch
+  io
+has type
+  String : Type
+but is expected to have type
+  IO String : Type
+-/
+#guard_msgs in
 def oops₂ : IO String := do
   let io <- getIO "str"
   io -- type mismatch: expected `IO String`, got `String`
 
 /-!
   ### Variant 3. in `if let`, expect `:=`, misuse `<-`
 -/
+
 def oops₃ : IO String := do
   if let some opt <- getOpt "str" then  -- unexpected token '<-'; expected ':=' or '←'
     let ret := (<- getIO opt)
@@ -99,6 +131,16 @@ def oops₃ : IO String := do
 
   #### 4.1 misuse `:=` gives me type mismatch
 -/
+
+/--
+error: type mismatch
+  some opt
+has type
+  Option ?m.4322 : Type
+but is expected to have type
+  IO (Option String) : Type
+-/
+#guard_msgs in
 def oops₄₁ : IO String := do
   if let some opt := getOptIO "str" then -- type mismatch: expected `IO (Option String)`, got `Option ?m.3586`
     let ret <- getIO opt
@@ -130,10 +172,39 @@ def works₄₃ : IO String := do
 /-!
   ## Cases from https://github.com/leanprover/lean4/pull/2676
 -/
+
+/--
+error: application type mismatch
+  pure true
+argument
+  true
+has type
+  Bool : Type
+but is expected to have type
+  Unit : Type
+---
+error: application type mismatch
+  pure false
+argument
+  false
+has type
+  Bool : Type
+but is expected to have type
+  Unit : Type
+-/
+#guard_msgs in
 example : IO Unit := do
   let x ← if true then pure true else pure false
 
+/--
+error: unknown identifier 'x'
+---
+error: unknown identifier 'x'
+---
+error: unknown identifier 'x'
+-/
+#guard_msgs in
 example : Id Unit := do
   let mut x ← if true then pure true else pure false
   if let .true := x then
-    x := false
+    x := false

lean4/examples/Tactics.lean

@@ -12,7 +12,7 @@ universe u1 u2 u3
 /-
 
   The following follows Lean series on writing tactics
-  
+
   https://www.vladasedlacek.cz/en/posts/lean-02-demo
 
 -/
@@ -80,4 +80,5 @@ theorem length_sum_perm_of_B₂ (Babc : B a b c) :
       . exact ne_12_of_B Babc |> (length_symm a b ▸ len_pos_of_neq)
 
 theorem length_sum_perm_of_B₃ (Babc : B a b c) : 0 < length a b ∧ 0 < length b a := by
-   simp only [ne_eq, ne_12_of_B Babc, len_pos_of_neq, length_symm]
+   simp only [ne_eq, ne_12_of_B Babc, len_pos_of_neq, length_symm, and_self]
+   exact len_pos_of_neq (ne_12_of_B Babc)

lean4/examples/Zulip/Import.lean

@@ -47,12 +47,12 @@ If there is only one candidate, it suggests `import Mathlib.<uniqueCandidate>` a
 Using `imp! <string>` uses fuzzy-matching, rather than exact matching. -/
 elab (name := commandImp!) tk:"imp" fz:("!")? na:(colGt ident) : command => do
   let inp := na.getId.toString
-  let dat := (← IO.FS.lines "lake-packages/mathlib/Mathlib.lean").map (String.drop · 15)
+  let dat := (← IO.FS.lines ".lake/packages/mathlib/Mathlib.lean").map (String.drop · 15)
   let cands := dat.filter <| (if fz.isSome then fuzzyMatch else String.isPrefixOf) inp
 
   liftTermElabM do
     cands.toList.forM fun imp => do
-      let impS ← moduleNameOfFileName ("lake-packages/mathlib/Mathlib/" ++ imp.replace "." "/" ++ ".lean") "lake-packages/mathlib/"
+      let impS ← moduleNameOfFileName (".lake/packages/mathlib/Mathlib/" ++ imp.replace "." "/" ++ ".lean") ".lake/packages/mathlib/"
       let imp : TSyntax `write_me_output_stx ← `(write_me_output_stx| import $(mkIdent impS))
       let stx ← getRef
       Std.Tactic.TryThis.addSuggestion stx imp
@@ -63,4 +63,4 @@ macro "imp!" na:(colGt ident) : command => `(command| imp ! $na)
 
 end Mathlib.Tactic.imp
 
-imp! Ring
+imp! Ring

lean4/lakefile.lean

@@ -16,6 +16,25 @@ lean_lib «Hello» {
 --   root := `Main
 -- }
 
+def check_example (ex : IO.FS.DirEntry) := do
+  let mut failed : Array (FilePath × IO.Process.Output) := #[]
+
+  let r ← timeit s!"Running example: {ex.fileName}\t" (IO.Process.output {
+    cmd := "lake"
+    args := #["env", "lean", ex.path.toString]
+    env := #[] -- #[("LEAN_PATH", searchPath)]
+  })
+
+  if r.exitCode == 0 then
+    IO.println "  Success!🟢"
+  else
+    failed := failed.append #[(ex.path, r)]
+    IO.println "  Failed!🔴"
+    IO.println r.stdout
+    IO.println r.stderr
+
+  return failed
+
 script check_examples (_args) do
   let cwd ← IO.currentDir
 
@@ -25,26 +44,20 @@ script check_examples (_args) do
   for ex in (← (cwd / "examples").readDir) do
     if ex.path.extension == some "lean" then
       total := total + 1
+      let result := (←check_example ex)
+      failed := failed.append result
 
-      let r ← timeit s!"Running example: {ex.fileName}\t" (IO.Process.output {
-        cmd := "lake"
-        args := #["env", "lean", ex.path.toString]
-        env := #[] -- #[("LEAN_PATH", searchPath)]
-      })
-
-      if r.exitCode == 0 then
-        IO.println "  Success!🟢"
-      else
-        failed := failed.append #[(ex.path, r)]
-        IO.println "  Failed!🔴"
-        IO.println r.stdout
-        IO.println r.stderr
-
-  if failed.size != 0 then 
+  for ex in (← (cwd / "examples" / "Zulip").readDir) do
+    if ex.path.extension == some "lean" then
+      total := total + 1
+      let result := (←check_example ex)
+      failed := failed.append result
+
+  if failed.size != 0 then
     IO.println "\nFailed examples:"
     for (ex, _) in failed do
       IO.println s!"  {ex}"
-  
+
   let succeeded := total - failed.size
   let resultMarker := if succeeded == total then "✅" else "❌"