chore: merge main

Author: fgdorais

Batteries/Lean/Name.lean

@@ -16,8 +16,13 @@ Generally, user code should not explicitly use internal names.
 def isInternalDetail : Name → Bool
   | .str p s     =>
     s.startsWith "_"
-      || s.startsWith "match_"
-      || s.startsWith "proof_"
+      || matchPrefix s "eq_"
+      || matchPrefix s "match_"
+      || matchPrefix s "proof_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum
+where
+  /-- Check that a string begins with the given prefix, and then is only digit characters. -/
+  matchPrefix (s : String) (pre : String) :=
+    s.startsWith pre && (s |>.drop pre.length |>.all Char.isDigit)

Batteries/Util/Cache.lean

@@ -132,7 +132,7 @@ the second will store declarations from imports (and will hopefully be "read-onl
 -/
 @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α)
 
-/-- Discrimation tree settings for the `DiscrTreeCache`. -/
+/-- Discrimination tree settings for the `DiscrTreeCache`. -/
 def DiscrTreeCache.config : WhnfCoreConfig := {}
 
 /--

Batteries/Util/CheckTactic.lean

@@ -9,7 +9,7 @@ import Lean.Elab.Term
 /-
 This file is the home for commands to tactics behave as expected.
 
-It currently includes two tactixs:
+It currently includes two tactics:
 
 #check_tactic t ~> res
 

Batteries/Util/ExtendedBinder.lean

@@ -52,22 +52,3 @@ macro_rules -- TODO: merging the two macro_rules breaks expansion
   | `(∀ᵉ _ : $ty:term, $b) => `(∀ _ : $ty:term, $b)
   | `(∀ᵉ $x:ident : $ty:term, $b) => `(∀ $x:ident : $ty:term, $b)
   | `(∀ᵉ $x:binderIdent $p:binderPred, $b) => `(∀ $x:binderIdent $p:binderPred, $b)
-
-open Parser.Command in
-/--
-Declares a binder predicate.  For example:
-```
-binder_predicate x " > " y:term => `($x > $y)
-```
--/
-syntax (name := binderPredicate) (docComment)? (Parser.Term.attributes)? (attrKind)?
-  "binder_predicate" optNamedName optNamedPrio ppSpace ident (ppSpace macroArg)* " => "
-    term : command
-
-open Linter.MissingDocs Parser Term in
-/-- Missing docs handler for `binder_predicate` -/
-@[missing_docs_handler binderPredicate]
-def checkBinderPredicate : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
-    if stx[4].isNone then lint stx[3] "binder predicate"
-    else lintNamed stx[4][0][3] "binder predicate"

Batteries/WF.lean

@@ -91,7 +91,7 @@ end Acc
 namespace WellFounded
 
 /-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
-This can be used in recursive function definitions to explicitly use a differerent relation
+This can be used in recursive function definitions to explicitly use a different relation
 than the one inferred by default:
 
 ```

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.8.0

scripts/test.lean

@@ -36,16 +36,20 @@ def main (args : List String) : IO Unit := do
           args := #["env", "lean", t.toString],
           env := #[("LEAN_ABORT_ON_PANIC", "1")] }
       let mut exitCode := out.exitCode
+      let stdout := out.stdout
+      let stderr := "\n".intercalate <|
+        -- We don't count manifest out of date warnings as noise.
+        out.stderr.splitOn "\n" |>.filter (!·.startsWith "warning: manifest out of date: ")
       if exitCode = 0 then
-        if out.stdout.isEmpty && out.stderr.isEmpty then
+        if stdout.isEmpty && stderr.isEmpty then
           IO.println s!"Test succeeded: {t}"
         else
           IO.println s!"Test succeeded with noisy output: {t}"
           unless allowNoisy do exitCode := 1
       else
         IO.eprintln s!"Test failed: `lake env lean {t}` produced:"
-      unless out.stdout.isEmpty do IO.eprintln out.stdout
-      unless out.stderr.isEmpty do IO.eprintln out.stderr
+      unless stdout.isEmpty do IO.eprintln stdout
+      unless out.stderr.isEmpty do IO.eprintln out.stderr -- We still print the manifest warning.
       pure exitCode
   -- Wait on all the jobs and exit with 1 if any failed.
   let mut exitCode : UInt8 := 0