From dfe82086e9904edfc04eb0f5205c85647956897d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 1 Jun 2024 08:53:46 +0100 Subject: [PATCH 1/5] chore: align `isInternalName` with upstream version (#796) * chore: align isInternalName with upstream version * doc-string --- Batteries/Lean/Name.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Batteries/Lean/Name.lean b/Batteries/Lean/Name.lean index b3705e6a2e..b5530e49d1 100644 --- a/Batteries/Lean/Name.lean +++ b/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) From ee879174c5d5fc6cbff0cfbc12be85550ed2e583 Mon Sep 17 00:00:00 2001 From: FR Date: Tue, 4 Jun 2024 06:16:12 +0800 Subject: [PATCH 2/5] chore: remove `binder_predicate` (#817) It has been upstreamed to Lean4. --- Batteries/Util/ExtendedBinder.lean | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/Batteries/Util/ExtendedBinder.lean b/Batteries/Util/ExtendedBinder.lean index 33629b7cc0..d577e1d785 100644 --- a/Batteries/Util/ExtendedBinder.lean +++ b/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" From 63d7c6fad69f119fac842b4f7b77e6c2796b1251 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 5 Jun 2024 01:43:24 +0200 Subject: [PATCH 3/5] fix: typos in docstrings (#822) --- Batteries/Util/Cache.lean | 2 +- Batteries/Util/CheckTactic.lean | 2 +- Batteries/WF.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Batteries/Util/Cache.lean b/Batteries/Util/Cache.lean index 1c25bb163c..edfac4fe97 100644 --- a/Batteries/Util/Cache.lean +++ b/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 := {} /-- diff --git a/Batteries/Util/CheckTactic.lean b/Batteries/Util/CheckTactic.lean index cab01de05b..bc97e681cc 100644 --- a/Batteries/Util/CheckTactic.lean +++ b/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 diff --git a/Batteries/WF.lean b/Batteries/WF.lean index 8fef8ad188..7a702665ae 100644 --- a/Batteries/WF.lean +++ b/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: ``` From 7110da53bf6da84198dba69ca90221c4798ade35 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 5 Jun 2024 02:46:27 +0100 Subject: [PATCH 4/5] chore: manifest out of date doesn't count as test noise (#818) * chore: manifest out of date doesn't count as test noise * still print manifest warning --- scripts/test.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/scripts/test.lean b/scripts/test.lean index 43df619246..0a488eabd4 100644 --- a/scripts/test.lean +++ b/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 From 51e6e0d24db9341fb031288c298b7e6b56102253 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 5 Jun 2024 04:46:51 +0100 Subject: [PATCH 5/5] chore: bump toolchain to v4.8.0 (#824) --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 78f39e211a..ef1f67e9e6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.8.0