From 3770b3dcb8b1b3340e0252760dc68e8e61daef06 Mon Sep 17 00:00:00 2001 From: Jason Yuen Date: Sat, 4 Apr 2026 00:34:34 -0700 Subject: [PATCH] chore: fix spelling errors (#13274) This PR fixed typos: ``` pip install codespell --upgrade codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex '[A-Z][a-z]*' codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex "\b[a-z']*" ``` --- .../Iterators/Lemmas/Combinators/Monadic/FilterMap.lean | 2 +- src/Init/Data/String/Lemmas/Iterate.lean | 4 ++-- src/Init/Data/String/Subslice.lean | 2 +- src/Lean/Compiler/LCNF/ResetReuse.lean | 2 +- src/Lean/Compiler/LCNF/SimpCase.lean | 2 +- src/Lean/Compiler/LCNF/ToDecl.lean | 2 +- src/Lean/Elab/Deriving/DecEq.lean | 2 +- src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean | 2 +- src/Lean/Meta/Match/Match.lean | 4 ++-- src/Lean/Meta/Match/Rewrite.lean | 2 +- src/Lean/Meta/Native.lean | 4 ++-- src/Lean/Meta/SameCtorUtils.lean | 2 +- src/Lean/Meta/Tactic/Cbv/ControlFlow.lean | 6 +++--- src/Lean/Meta/Tactic/Cbv/Main.lean | 2 +- src/Lean/Meta/Tactic/Grind/Core.lean | 2 +- src/Lean/Meta/Tactic/Grind/Types.lean | 4 ++-- src/Lean/Server/FileWorker/WidgetRequests.lean | 4 ++-- src/Std/Tactic/BVDecide/Syntax.lean | 2 +- src/kernel/declaration.h | 2 +- src/lake/Lake/Build/Common.lean | 2 +- src/lake/Lake/Build/Trace.lean | 2 +- src/lake/Lake/CLI/Help.lean | 8 ++++---- src/lake/Lake/Config/Env.lean | 2 +- src/lake/Lake/Load/Resolve.lean | 2 +- tests/README.md | 2 +- tests/bench/mvcgen/sym/lib/VCGen.lean | 2 +- tests/compile_bench/iterators.lean | 2 +- tests/elab/10984.lean | 2 +- tests/elab/casesOnSameCtor.lean | 2 +- tests/elab/cbv_classical.lean | 2 +- tests/elab/grind_9856.lean | 4 ++-- tests/elab/issue11665.lean | 2 +- tests/elab/lcnf_export_borrow_error.lean | 4 ++-- tests/elab/match1.lean | 2 +- .../{mvcgenUnkownIdent.lean => mvcgenUnknownIdent.lean} | 0 tests/elab/newdo.lean | 2 +- tests/elab/simple_ground_extraction.lean | 2 +- tests/elab/sparseCasesOn.lean | 2 +- tests/elab_bench/cbv_aes.lean | 2 +- tests/elab_fail/10488.lean | 2 +- tests/lake/tests/module/test.sh | 2 +- 41 files changed, 52 insertions(+), 52 deletions(-) rename tests/elab/{mvcgenUnkownIdent.lean => mvcgenUnknownIdent.lean} (100%) diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index df469f2ce1..0f091c08bb 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β : Sort u_2} /-- Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`. -This lemma is useful for simplifying the second computation, which often involes `match` expressions +This lemma is useful for simplifying the second computation, which often involves `match` expressions that use `pbind`'s proof term. -/ private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) : diff --git a/src/Init/Data/String/Lemmas/Iterate.lean b/src/Init/Data/String/Lemmas/Iterate.lean index d436445458..32bd888af7 100644 --- a/src/Init/Data/String/Lemmas/Iterate.lean +++ b/src/Init/Data/String/Lemmas/Iterate.lean @@ -31,7 +31,7 @@ namespace Slice /-- A list of all positions starting at {name}`p`. -This function is not meant to be used in actual progams. Actual programs should use +This function is not meant to be used in actual programs. Actual programs should use {name}`Slice.positionsFrom` or {name}`Slice.positions`. -/ protected def Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := @@ -206,7 +206,7 @@ end Slice /-- A list of all positions starting at {name}`p`. -This function is not meant to be used in actual progams. Actual programs should use +This function is not meant to be used in actual programs. Actual programs should use {name}`Slice.positionsFrom` or {name}`Slice.positions`. -/ protected def Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos } := diff --git a/src/Init/Data/String/Subslice.lean b/src/Init/Data/String/Subslice.lean index 2dd001ce0e..193e7ec99f 100644 --- a/src/Init/Data/String/Subslice.lean +++ b/src/Init/Data/String/Subslice.lean @@ -23,7 +23,7 @@ Given a {name}`Slice` {name}`s`, the type {lean}`s.Subslice` is the type of half in {name}`s` delineated by a valid position on both sides. This type is useful to track regions of interest within some larger slice that is also of interest. -In contrast, {name}`Slice` is used to track regions of interest whithin some larger string that is +In contrast, {name}`Slice` is used to track regions of interest within some larger string that is not or no longer relevant. Equality on {name}`Subslice` is somewhat better behaved than on {name}`Slice`, but note that there diff --git a/src/Lean/Compiler/LCNF/ResetReuse.lean b/src/Lean/Compiler/LCNF/ResetReuse.lean index 1d751824d8..fc120590a9 100644 --- a/src/Lean/Compiler/LCNF/ResetReuse.lean +++ b/src/Lean/Compiler/LCNF/ResetReuse.lean @@ -28,7 +28,7 @@ inserts addition instructions to attempt to reuse the memory right away instead allocator. For this the paper defines three functions: -- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be elligible for +- `R` (called `Decl.insertResetReuse` here) which looks for candidates that might be eligible for reuse. For these variables it invokes `D`. - `D` which looks for code regions in which the target variable is dead (i.e. no longer read from), it then invokes `S`. If `S` succeeds it inserts a `reset` instruction to match the `reuse` diff --git a/src/Lean/Compiler/LCNF/SimpCase.lean b/src/Lean/Compiler/LCNF/SimpCase.lean index adb444da26..a5c1d0a9e8 100644 --- a/src/Lean/Compiler/LCNF/SimpCase.lean +++ b/src/Lean/Compiler/LCNF/SimpCase.lean @@ -24,7 +24,7 @@ In particular we perform: - folding of the most common cases arm into the default arm if possible Note: Currently the simplifier still contains almost equivalent simplifications to the ones shown -here. We know that this causes unforseen behavior and do plan on changing it eventually. +here. We know that this causes unforeseen behavior and do plan on changing it eventually. -/ -- TODO: the following functions are duplicated from simp and should be deleted in simp once we diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean index e224952e0b..71494c6f3b 100644 --- a/src/Lean/Compiler/LCNF/ToDecl.lean +++ b/src/Lean/Compiler/LCNF/ToDecl.lean @@ -171,7 +171,7 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do if compiler.ignoreBorrowAnnotation.get (← getOptions) then decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) } if isExport env decl.name && decl.params.any (·.borrow) then - throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration." + throwError m!" Declaration {decl.name} is marked as `export` but some of its parameters have borrow annotations.\n Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type.\n If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration." return decl end Lean.Compiler.LCNF diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 15fd204270..c509e8f588 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -111,7 +111,7 @@ def mkMatchNew (ctx : Context) (header : Header) (indVal : InductiveVal) : TermE let x1 := mkIdent header.targetNames[0]! let x2 := mkIdent header.targetNames[1]! let ctorIdxName := mkCtorIdxName indVal.name - -- NB: the getMatcherInfo? assumes all mathcers are called `match_` + -- NB: the getMatcherInfo? assumes all matchers are called `match_` let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor) mkCasesOnSameCtor casesOnSameCtorName indVal.name let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean index e037ba23db..0b1cd6aa78 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean @@ -36,7 +36,7 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta TacticContext.new lratPath cfg /-- -Prepare an `Expr` that proves `bvExpr.unsat` using native evalution. +Prepare an `Expr` that proves `bvExpr.unsat` using native evaluation. -/ def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index cb754e8e83..a0cd17e1e6 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -33,12 +33,12 @@ The high-level overview of moves are * If there is an alternative, solve its constraints * Else use `contradiction` to prove completeness of the match * Process “independent prefixes” of patterns. These are patterns that can be processed without - affecting the aother alternatives, and without side effects in the sense of updating the `mvarId`. + affecting the other alternatives, and without side effects in the sense of updating the `mvarId`. These are - variable patterns; substitute - inaccessible patterns; add equality constraints - as-patterns: substitute value and equality - After thes have been processed, we use `.inaccessible x` where `x` is the variable being matched + After these have been processed, we use `.inaccessible x` where `x` is the variable being matched to mark them as “done”. * If all patterns start with “done”, drop the first variable * The first alt has only “done” patterns, drop remaining alts (they're overlapped) diff --git a/src/Lean/Meta/Match/Rewrite.lean b/src/Lean/Meta/Match/Rewrite.lean index 5ed78a902c..abf51e233f 100644 --- a/src/Lean/Meta/Match/Rewrite.lean +++ b/src/Lean/Meta/Match/Rewrite.lean @@ -17,7 +17,7 @@ namespace Lean.Meta /-- Tries to rewrite the `ite`, `dite` or `cond` expression `e` with the hypothesis `hc`. -If it fails, it returns a rewrite with `proof? := none` and unchaged expression. +If it fails, it returns a rewrite with `proof? := none` and unchanged expression. -/ def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do match_expr e with diff --git a/src/Lean/Meta/Native.lean b/src/Lean/Meta/Native.lean index 13a36c9408..890d6e446f 100644 --- a/src/Lean/Meta/Native.lean +++ b/src/Lean/Meta/Native.lean @@ -22,9 +22,9 @@ of that computation as an axiom towards the logic. -/ public inductive NativeEqTrueResult where - /-- The given expression `e` evalutes to true. `prf` is a proof of `e = true`. -/ + /-- The given expression `e` evaluates to true. `prf` is a proof of `e = true`. -/ | success (prf : Expr) - /-- The given expression `e` evalutes to false. -/ + /-- The given expression `e` evaluates to false. -/ | notTrue /-- diff --git a/src/Lean/Meta/SameCtorUtils.lean b/src/Lean/Meta/SameCtorUtils.lean index 0e49a11d29..1ee6011087 100644 --- a/src/Lean/Meta/SameCtorUtils.lean +++ b/src/Lean/Meta/SameCtorUtils.lean @@ -14,7 +14,7 @@ This module contains utilities for dealing with equalities between constructor a in particular about which fields must be the same a-priori for the equality to type check. Users include (or will include) the injectivity theorems, the per-constructor no-confusion -construction and deriving type classes lik `BEq`, `DecidableEq` or `Ord`. +construction and deriving type classes like `BEq`, `DecidableEq` or `Ord`. -/ namespace Lean.Meta diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean index 9daf075eb8..ee4ee03c1a 100644 --- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean +++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean @@ -44,7 +44,7 @@ def isCbvNoncomputable (p : Name) : CoreM Bool := do return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p /-- -Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance +Attempts to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance -/ def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none @@ -112,7 +112,7 @@ builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do else if (← isFalseExpr c') then return .step b (mkApp (e.replaceFn ``ite_cond_eq_false) h) (contextDependent := cd) else - -- If we got stuck with simplifying `p` then let's try evaluating the original isntance + -- If we got stuck with simplifying `p` then let's try evaluating the original instance simpAndMatchIteDecidable f α c inst a b do -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'` let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h @@ -317,7 +317,7 @@ public def reduceRecMatcher : Simproc := fun e => do else return .rfl -builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := +builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher def tryMatchEquations (appFn : Name) : Simproc := fun e => do diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index 9b12426155..8d332cb215 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -272,7 +272,7 @@ def handleProj : Simproc := fun e => do let reduced ← Sym.share reduced return .step reduced (← Sym.mkEqRefl reduced) | .none => - -- If we failed to reduce it, we turn to a last resort; we try use heterogenous congruence lemma that we then try to turn into an equality. + -- If we failed to reduce it, we turn to a last resort; we try use heterogeneous congruence lemma that we then try to turn into an equality. unless (← isDefEq struct e') do -- If we rewrote the projection body using something that holds up to propositional equality, then there is nothing we can do. -- TODO: Check if there is a need to report this to a user, or shall we fail silently. diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean index bf4b53bc27..6b77a2e56d 100644 --- a/src/Lean/Meta/Tactic/Grind/Core.lean +++ b/src/Lean/Meta/Tactic/Grind/Core.lean @@ -172,7 +172,7 @@ private partial def addEqStep (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit trueEqFalse := true else let hasHEq := isHEq || lhsRoot.heqProofs || rhsRoot.heqProofs - -- **Note**: We only have to check the types if there are heterogenous equalities. + -- **Note**: We only have to check the types if there are heterogeneous equalities. if (← pure !hasHEq <||> hasSameType lhsRoot.self rhsRoot.self) then valueInconsistency := true if (lhsRoot.interpreted && !rhsRoot.interpreted) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 6b4e740c1f..46ca5ed5bf 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -1973,7 +1973,7 @@ def SolverExtension.markTerm (ext : SolverExtension σ) (e : Expr) : GoalM Unit | .next id' e' sTerms' => if id == id' then -- Skip if `e` and `e'` have different types (e.g., they were merged via `HEq` from `cast`). - -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m` + -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m` if (← pure !root.heqProofs <||> hasSameType e e') then (← solverExtensionsRef.get)[id]!.newEq e e' return sTerms @@ -2056,7 +2056,7 @@ where | .nil => return () | .eq solverId lhs rhs rest => -- Skip if `lhs` and `rhs` have different types (e.g., they were merged via `HEq` from `cast`). - -- This can happen when we have heterogenous equalities in an equivalence class containing types such as `Fin n` and `Fin m` + -- This can happen when we have heterogeneous equalities in an equivalence class containing types such as `Fin n` and `Fin m` let root ← getRootENode lhs if (← pure !root.heqProofs <||> hasSameType lhs rhs) then (← solverExtensionsRef.get)[solverId]!.newEq lhs rhs diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index cdcd967833..46626cb18e 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -192,7 +192,7 @@ private def matchEndPos (query : String) (startPos : String.Pos.Raw) : String.Po startPos + query @[specialize] -private def hightlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw) +private def highlightStringMatches? (query text : String) (matchPositions : Array String.Pos.Raw) (highlight : α) (offset : String.Pos.Raw := ⟨0⟩) (mapIdx : Nat → Nat := id) : Option (TaggedText α) := Id.run do if query.isEmpty || text.isEmpty || matchPositions.isEmpty then @@ -245,7 +245,7 @@ private def advanceTaggedTextHighlightState (text : String) (highlighted : α) : let query := (← get).query let p := (← get).p let ms := (← get).ms - let highlighted? := hightlightStringMatches? query text ms highlighted (offset := p) + let highlighted? := highlightStringMatches? query text ms highlighted (offset := p) (mapIdx := fun i => ms.size - i - 1) updateState text highlighted?.isSome return highlighted?.getD (.text text) diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index 8ee44b66cb..9b06437f69 100644 --- a/src/Std/Tactic/BVDecide/Syntax.lean +++ b/src/Std/Tactic/BVDecide/Syntax.lean @@ -53,7 +53,7 @@ structure BVDecideConfig where /-- Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`. This has synergy potential with embedded constraint substitution. Because embedded constraint - subsitution is the only use case for this feature it is automatically disabled whenever embedded + substitution is the only use case for this feature it is automatically disabled whenever embedded constraint substitution is disabled. -/ andFlattening : Bool := true diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index fdfc1747dd..09d98501fa 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -226,7 +226,7 @@ public: bool is_unsafe() const; /** \brief Only definitions have values for the purpose of reduction and type checking. Theorems used to be like that; now they are treated like - opaque declations. */ + opaque declarations. */ bool has_value() const { return is_definition(); } axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast(cnstr_get_ref(raw(), 0)); } diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index c283fda65b..7e7bc1f76a 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -271,7 +271,7 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`. If up-to-date, replays the saved log from the trace and sets the current build action to `replay`. Otherwise, if the log is empty and trace is synthetic, -or if the trace is not up-to-date, the build action will be set ot `fetch`. +or if the trace is not up-to-date, the build action will be set to `fetch`. -/ public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do if let .ok data := self then diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 656c991fab..891ee54d85 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -151,7 +151,7 @@ public def ofDecimal? (s : String) : Option Hash := @[inline] public def ofString? (s : String) : Option Hash := ofHex? s -/-- Laod a hash from a `.hash` file. -/ +/-- Load a hash from a `.hash` file. -/ public def load? (hashFile : FilePath) : BaseIO (Option Hash) := ofString? <$> IO.FS.readFile hashFile |>.catchExceptions fun _ => pure none diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index aa96ac1b5f..0835e062b4 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -356,9 +356,9 @@ USAGE: COMMANDS: get [] download build outputs into the local Lake cache - put upload build ouptuts to a remote cache + put upload build outputs to a remote cache add add input-to-output mappings to the Lake cache - clean removes ALL froms the local Lake cache + clean removes ALL from the local Lake cache services print configured remote cache services STAGING COMMANDS: @@ -415,7 +415,7 @@ will search the repository's entire history (or as far as Git will allow). By default, Lake will download both the input-to-output mappings and the output artifacts for a package. By using `--mappings-onlys`, Lake will only -download the mappings abd delay downloading artifacts until they are needed. +download the mappings and delay downloading artifacts until they are needed. If a download for an artifact fails or the download process for a whole package fails, Lake will report this and continue on to the next. Once done, @@ -469,7 +469,7 @@ OPTIONS: --scope= the prefix of artifacts within the service --repo= for Reservoir, a GitHub repository scope -Reads a list of input-to-output mapppings from the provided file and adds +Reads a list of input-to-output mappings from the provided file and adds them to the local Lake cache. If `--service` is provided, the output artifacts can then be fetched lazily from that service during a Lake build. The service must either be `reservoir` or be configured through the Lake system diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index eed315c538..f7a684b1c4 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -58,7 +58,7 @@ public structure Env where If `none`, no suitable system directory for the cache exists. -/ lakeSystemCache? : Option Cache := none - /-- The path to the sytem Lake configuration (i.e., `LAKE_CONFIG`). -/ + /-- The path to the system Lake configuration (i.e., `LAKE_CONFIG`). -/ lakeConfig? : Option FilePath /-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/ cacheKey? : Option String diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index ec7c9978ab..9990a1d496 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -220,7 +220,7 @@ private structure ToolchainCandidate where fixed : Bool := false private structure ToolchainState where - /-- The name of depedency which provided the current candidate toolchain. -/ + /-- The name of dependency which provided the current candidate toolchain. -/ src : Name /-- The current candidate toolchain version (if any). -/ tc? : Option ToolchainVer diff --git a/tests/README.md b/tests/README.md index c14adfdaa7..ce2786293b 100644 --- a/tests/README.md +++ b/tests/README.md @@ -203,7 +203,7 @@ Inside a test directory, they receive no arguments. A test succeeds iff the `run_test.sh` script exits with exit code 0. A benchmark additionally must produce a measurements file: -Inside a test pile, `run_bench.sh` is expected to produce a `.measurments.jsonl` file. +Inside a test pile, `run_bench.sh` is expected to produce a `.measurements.jsonl` file. Inside a test directory, `run_bench.sh` is expected to produce a `measurements.jsonl` file. ## The `elab*` test pile diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/tests/bench/mvcgen/sym/lib/VCGen.lean index fde06d03a2..fa914301ca 100644 --- a/tests/bench/mvcgen/sym/lib/VCGen.lean +++ b/tests/bench/mvcgen/sym/lib/VCGen.lean @@ -219,7 +219,7 @@ lemma for the backward rule. It is unnecessary to use the `bind` rule in full generality. It is much more efficient to specialize it for the particular monad, postshape and `WP` instance. In doing so we can also unfold many -`Std.Do` abbrevations, such as `Assertion ps` and `PostCond α ps`. +`Std.Do` abbreviations, such as `Assertion ps` and `PostCond α ps`. We do that by doing `unfoldReducible` on the forall telescope. The type for `StateM Nat` and one excess state arg `s` becomes ``` diff --git a/tests/compile_bench/iterators.lean b/tests/compile_bench/iterators.lean index ea4fa224bf..8f6dd529a0 100644 --- a/tests/compile_bench/iterators.lean +++ b/tests/compile_bench/iterators.lean @@ -10,7 +10,7 @@ The benchmark is run in three settings. * The time taken to interpret the script, including running `main`, is measured in `iterators (interpreted)`. * The time taken to interpret the script, without running `main`, is measured in - `interators (elab)`. + `iterators (elab)`. -/ /- definitions -/ diff --git a/tests/elab/10984.lean b/tests/elab/10984.lean index 48f16cfe6f..f81c19baf6 100644 --- a/tests/elab/10984.lean +++ b/tests/elab/10984.lean @@ -66,7 +66,7 @@ Example of `@` from Floris van Doorn at https://github.com/leanprover/lean4/issu example {α : Type} (f : ∀ {α}, List α → List α) : f (@.nil α) = .nil := sorry /-! -Example of `@` plus universe levels adapated from https://github.com/leanprover/lean4/issues/10984 +Example of `@` plus universe levels adapted from https://github.com/leanprover/lean4/issues/10984 -/ example {α : Type u} (f : ∀ {α}, List α → List α) : f (@.nil.{u} α) = .nil := sorry diff --git a/tests/elab/casesOnSameCtor.lean b/tests/elab/casesOnSameCtor.lean index 6034ecba32..c1a183c2d6 100644 --- a/tests/elab/casesOnSameCtor.lean +++ b/tests/elab/casesOnSameCtor.lean @@ -109,7 +109,7 @@ info: theorem Vec.decEqVec.eq_def.{u_1} : ∀ {α : Type u_1} {a : Nat} [inst : #print sig decEqVec.eq_def --- Incidentially, normal match syntax is able to produce an equivalent matcher +-- Incidentally, normal match syntax is able to produce an equivalent matcher -- (with different implementation): -- (see #10195 for problems with equation generation) diff --git a/tests/elab/cbv_classical.lean b/tests/elab/cbv_classical.lean index 10c32f1ae7..7f7e970036 100644 --- a/tests/elab/cbv_classical.lean +++ b/tests/elab/cbv_classical.lean @@ -4,7 +4,7 @@ when re-synthesizing instances. When `cbv` encounters `decide P`, it simplifies the proposition `P`. If `P` unfolds (e.g. `IsEven 2` → `∃ k, 2 * k = 2`), `simpDecideCbv` tries to -synthetize `Decidable` instance for the *unfolded* form. With `open Classical`, +synthesize `Decidable` instance for the *unfolded* form. With `open Classical`, this was picking up `Classical.propDecidable` (which uses `choice`), replacing the original computable instance with one that cannot be evaluated. diff --git a/tests/elab/grind_9856.lean b/tests/elab/grind_9856.lean index 4679d76f45..ee19484464 100644 --- a/tests/elab/grind_9856.lean +++ b/tests/elab/grind_9856.lean @@ -1,7 +1,7 @@ module inductive T (a:Type) where - | constuctor1: T a - | constuctor2: T a + | constructor1: T a + | constructor2: T a instance : LE (T a) where le := sorry diff --git a/tests/elab/issue11665.lean b/tests/elab/issue11665.lean index 00816ef757..f0a41d7140 100644 --- a/tests/elab/issue11665.lean +++ b/tests/elab/issue11665.lean @@ -10,4 +10,4 @@ def test1 : (n : Nat) → T n → Unit | _, _ => () def eqns := @test1.match_1.eq_1 -- used to fail -def congreqns := @test1.match_1.congr_eq_1 -- used to faile +def congreqns := @test1.match_1.congr_eq_1 -- used to fail diff --git a/tests/elab/lcnf_export_borrow_error.lean b/tests/elab/lcnf_export_borrow_error.lean index 8a4ce2cbeb..18d8a6a8db 100644 --- a/tests/elab/lcnf_export_borrow_error.lean +++ b/tests/elab/lcnf_export_borrow_error.lean @@ -4,8 +4,8 @@ module /-- error: Declaration bar is marked as `export` but some of its parameters have borrow annotations. - Consider using `set_option compiler.ignoreBorrowAnnotation true in` to supress the borrow annotations in its type. - If the declaration is part of an `export`/`extern` pair make sure to also supress the annotations at the `extern` declaration. + Consider using `set_option compiler.ignoreBorrowAnnotation true in` to suppress the borrow annotations in its type. + If the declaration is part of an `export`/`extern` pair make sure to also suppress the annotations at the `extern` declaration. -/ #guard_msgs in @[export foo] diff --git a/tests/elab/match1.lean b/tests/elab/match1.lean index 4b9ca6caf4..a036d50028 100644 --- a/tests/elab/match1.lean +++ b/tests/elab/match1.lean @@ -158,7 +158,7 @@ partial def natToBin' : (n : Nat) → List Bool -- This used to be bad until we used sparse matchers, -- which meant that the `0` pattern does not cause the remaining --- to have `n = .succ _`, whic breaks dependent pattern matching +-- to have `n = .succ _`, which breaks dependent pattern matching partial def natToBinBad (n : Nat) : List Bool := match n, parity n with | 0, _ => [] diff --git a/tests/elab/mvcgenUnkownIdent.lean b/tests/elab/mvcgenUnknownIdent.lean similarity index 100% rename from tests/elab/mvcgenUnkownIdent.lean rename to tests/elab/mvcgenUnknownIdent.lean diff --git a/tests/elab/newdo.lean b/tests/elab/newdo.lean index 6d5a4a8356..50dd974bce 100644 --- a/tests/elab/newdo.lean +++ b/tests/elab/newdo.lean @@ -486,7 +486,7 @@ example (cache : Std.HashMap (Nat × Nat) Bool) : Bool := Id.run do -- Extracted from MathlibTest.random.lean. The problem here is that the `match` elaborator used to -- destructure the `(x, y)` pattern into `x` and `y` caused defaulting of `count` to `Nat`. --- Nowadays, the `match` elaborator does not trigger global defaulting (in constrast to the term +-- Nowadays, the `match` elaborator does not trigger global defaulting (in contrast to the term -- `match` elaborator), fixing this test case. example : IO Bool := do let mut count := 0 diff --git a/tests/elab/simple_ground_extraction.lean b/tests/elab/simple_ground_extraction.lean index a79f7c791e..ef425ac8d1 100644 --- a/tests/elab/simple_ground_extraction.lean +++ b/tests/elab/simple_ground_extraction.lean @@ -1,4 +1,4 @@ -/-! This test asserts that the compiler is able to succesfully extract certain terms as statically +/-! This test asserts that the compiler is able to successfully extract certain terms as statically initializable values. -/ diff --git a/tests/elab/sparseCasesOn.lean b/tests/elab/sparseCasesOn.lean index 3c300e1b3b..879083b139 100644 --- a/tests/elab/sparseCasesOn.lean +++ b/tests/elab/sparseCasesOn.lean @@ -32,7 +32,7 @@ run_meta Lean.logInfo m!"{name}" -/- Check that the compiler is producin good code -/ +/- Check that the compiler is producing good code -/ set_option trace.Compiler.saveBase true diff --git a/tests/elab_bench/cbv_aes.lean b/tests/elab_bench/cbv_aes.lean index a18c53ffca..417c628155 100644 --- a/tests/elab_bench/cbv_aes.lean +++ b/tests/elab_bench/cbv_aes.lean @@ -316,7 +316,7 @@ def AES256KBR : KBR := def KeySchedule : Type := List (BitVec WordSize) -- Declare KeySchedule to be an instance HAppend --- so we can apply `++` to KeySchedules propertly +-- so we can apply `++` to KeySchedules properly instance : HAppend KeySchedule KeySchedule KeySchedule where hAppend := List.append diff --git a/tests/elab_fail/10488.lean b/tests/elab_fail/10488.lean index 0641a7887a..27966445ca 100644 --- a/tests/elab_fail/10488.lean +++ b/tests/elab_fail/10488.lean @@ -41,7 +41,7 @@ def foo {A B} (_: A) (_: B) : Unit := () #check (11.12succ) --- This example (adapted from structInst4.lean) exercises the difference betwee +-- This example (adapted from structInst4.lean) exercises the difference between -- term parsing and LVal parsing; the latter fails if we allow `2.snd` to parse -- as a scientificLit followed by an error token, so this test captures -- that we have to throw the error token right away, positioned before, rather diff --git a/tests/lake/tests/module/test.sh b/tests/lake/tests/module/test.sh index 50aeb17645..47f9127e18 100755 --- a/tests/lake/tests/module/test.sh +++ b/tests/lake/tests/module/test.sh @@ -20,7 +20,7 @@ public def foo : String := "bar" EOF # Test cross-package `import all` -# previosuly prevented by default +# previously prevented by default # test_err 'cannot `import all` the module' build ErrorTest.CrossPackageImportAll # currently allowed test_run build ErrorTest.CrossPackageImportAll