chore: Fix warnings

.github/workflows/ci.yml

@@ -23,16 +23,18 @@ jobs:
 
       # Installs the toolchain pinned in `lean-toolchain` and runs `lake build`,
       # i.e. the `defaultTargets`: the `Lean4Lean` library, the `lean4lean` exe,
-      # `Lean4Lean.Theory`, `Lean4Lean.Verify` and `Lean4Lean.Tests`. The proofs
-      # in `Verify` deliberately contain `sorry`s, so warnings must not fail the
-      # build. `Lean4Lean.Experimental` is WIP and is not a default target.
+      # `Lean4Lean.Theory`, `Lean4Lean.Verify` and `Lean4Lean.Tests`. `--wfail`
+      # keeps that surface warning-free for consumers that build it that way;
+      # the frontier `sorry`s are annotated at their declarations, so they no
+      # longer count. `Lean4Lean.Experimental` is not a default target.
       - name: Build
         uses: leanprover/lean-action@v1
         with:
-          use-mathlib-cache: false
+          build-args: --wfail
 
       # `Lean4Lean.Experimental` is WIP and deliberately not a default target, but it still has to
-      # compile. `sorry`s here are expected, as in `Verify`.
+      # compile. No `--wfail`: this is parked proof work outside the audited surface, so its
+      # `sorry`s are unannotated on purpose and stay visible as warnings.
       - name: Build Lean4Lean.Experimental
         run: lake build Lean4Lean.Experimental
 
@@ -43,7 +45,7 @@ jobs:
       # literals the way a source grep can. Not a default target, so it is built
       # explicitly here; the surface it imports is already built above.
       - name: Check sorry frontier
-        run: lake build Lean4Lean.Audit.SorryFrontier
+        run: lake build --wfail Lean4Lean.Audit.SorryFrontier
 
       # `lake build` only establishes that lean4lean compiles; these check that it still
       # *works*. The two modes exercise different code paths, so both are worth running.

Lean4Lean/Audit/SorryFrontier.lean

@@ -105,6 +105,15 @@ is intentionally not imported.
 
 Runs as a build-time `run_cmd`, not an executable: `lake build` of this module
 is the whole check.
+
+Because this audit is what guards the frontier, every allowlisted declaration
+that would log Lean's "declaration uses `sorry`" warning carries `set_option
+warn.sorry false in` at its definition, which keeps `lake build --wfail` clean
+for downstream consumers. (The `#guard_msgs`-pinned fixtures below need no
+annotation: their warning is captured by the pinned message.) Suppressing the
+warning costs no safety here, since the check reads `sorryAx` out of the
+environment: a sorry that is new, moved, or renamed still fails this build, and
+one added without the annotation also still fails `--wfail`.
 -/
 
 open Lean Lean.Elab.Command

Lean4Lean/Inductive/Add.lean

@@ -264,13 +264,10 @@ theorem checkInductiveTypes_singleton_zero_of_whnf_sort
   cases hfuel_eq : context.fuel.inductiveFuel with
   | zero => omega
   | succ fuel =>
-    simp [checkInductiveTypes, checkInductiveTypes.loopInd,
-      checkInductiveTypes.loopInd.loop, singletonInductiveStats,
-      readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read,
-      ReaderT.bind, Bind.bind, Pure.pure, ReaderT.pure,
-      Except.bind, Except.pure, liftTypeChecker_apply,
-      hclosed, hcheck, hwhnf, hensure, hfuel_eq,
-      InductiveStats.initial, Expr.sortLevel!]
+    simp [checkInductiveTypes, checkInductiveTypes.loopInd, checkInductiveTypes.loopInd.loop,
+      singletonInductiveStats, readThe, MonadReader.read, MonadReaderOf.read, ReaderT.read,
+      ReaderT.bind, Bind.bind, Pure.pure, Except.bind, Except.pure, liftTypeChecker_apply, hclosed,
+      hcheck, hwhnf, hensure, hfuel_eq, InductiveStats.initial, Expr.sortLevel!]
 
 /-- Transparent occurrence test for constants in the inductive block.
 
@@ -1241,8 +1238,7 @@ theorem checkInductiveTypes_singleton_of_candidate
       (List.map Level.param context.lparams)).indConsts).isEmpty = true from
     rfl)]
   simp only [Expr.sortLevel!, InductiveStats.initial, Nat.zero_add]
-  simp only [ReaderT.bind, Bind.bind, ReaderT.pure, Pure.pure, Except.pure,
-    Except.bind]
+  simp only [ReaderT.bind, Bind.bind, Except.pure, Except.bind]
   rw [checkInductiveTypes.loopInd.eq_1]
   have hdone : ¬1 < #[indType].size := by simp
   rw [dif_neg hdone]
@@ -1320,7 +1316,7 @@ def isDefEqSteps :
       domainCandidate.isDefEqSteps ++ bodyCandidate.isDefEqSteps
 
 /-- Every retained WHNF observation is an exact checker execution. -/
-def allValid : (candidate : CandidateExprTrace context source) →
+theorem allValid : (candidate : CandidateExprTrace context source) →
     ∀ step ∈ candidate.steps, step.Valid
   | .terminal context source _ result _ valid, step, h => by
     simp only [steps, List.mem_singleton] at h
@@ -1334,7 +1330,7 @@ def allValid : (candidate : CandidateExprTrace context source) →
     · exact body.allValid step h
 
 /-- Every retained full-check observation is an exact checker execution. -/
-def allChecksValid : (candidate : CandidateExprTrace context source) →
+theorem allChecksValid : (candidate : CandidateExprTrace context source) →
     ∀ step ∈ candidate.checkSteps, step.Valid
   | .terminal context source inferred _ checked _, step, h => by
     simp only [checkSteps, List.mem_singleton] at h
@@ -1349,7 +1345,7 @@ def allChecksValid : (candidate : CandidateExprTrace context source) →
 
 /-- Every retained binder-domain equality is an exact successful checker
 execution. -/
-def allIsDefEqValid : (candidate : CandidateExprTrace context source) →
+theorem allIsDefEqValid : (candidate : CandidateExprTrace context source) →
     ∀ step ∈ candidate.isDefEqSteps, step.Valid
   | .terminal .., step, h => by simp [isDefEqSteps] at h
   | .forallE _ _ _ _ _ _ _ _ _ annotationsEq _ _ domain body,

Lean4Lean/Inductive/EliminationTrace.lean

@@ -104,8 +104,7 @@ theorem run
       rw [isLargeEliminator.loop.eq_2, withLocalDecl_apply]
       have notField : ¬ argIdx ≥ stats.params.size :=
         Nat.not_le.mpr isParameter
-      simp only [notField, if_false, ReaderT.pure, Pure.pure,
-        ReaderT.bind, Bind.bind, Except.bind, Except.pure]
+      simp only [notField, if_false, Bind.bind]
       exact ih
   | proofField context fuel argIdx toCheck name domain body binderInfo
       sortResult isField ensureStep isProp tail ih =>
@@ -114,8 +113,7 @@ theorem run
       simp only [isField, if_true, ReaderT.bind, Bind.bind,
         liftTypeChecker_apply]
       rw [ensureStep]
-      simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true,
-        if_false, Pure.pure]
+      simp only [Except.bind, isProp, Bool.not_true, Bool.false_eq_true, if_false]
       exact ih
   | dataField context fuel argIdx toCheck name domain body binderInfo
       sortResult isField ensureStep isProp tail ih =>
@@ -124,7 +122,7 @@ theorem run
       simp only [isField, if_true, ReaderT.bind, Bind.bind,
         liftTypeChecker_apply]
       rw [ensureStep]
-      simp only [Except.bind, isProp, Bool.not_false, if_true, Pure.pure]
+      simp only [Except.bind, isProp, Bool.not_false, if_true]
       exact ih
   | terminal context source fuel argIdx toCheck notForall =>
       cases source <;>

Lean4Lean/Theory/Inductive.lean

@@ -2110,7 +2110,7 @@ def NormalizedFamily.generationShape (np : Nat)
     family.ctorPairs.all (NormalizedCtor.generationShape np)
 
 def NormalizedCheckedBlock.rawParams {source : VInductDecl}
-    (block : NormalizedCheckedBlock source) : List VExpr :=
+    (_block : NormalizedCheckedBlock source) : List VExpr :=
   blockParams source.nparams source.types
 
 def NormalizedCheckedBlock.familyPairs {source : VInductDecl}
@@ -2727,7 +2727,7 @@ def NormalizedBlockCtor.rawResult {source : VInductDecl}
 
 /-- Normalized constructor result reconstructed with the stored owner name. -/
 def NormalizedBlockCtor.resultTarget {source : VInductDecl}
-    (gen : BlockGenerationChecked source)
+    (_gen : BlockGenerationChecked source)
     (constructor : NormalizedBlockCtor) : VExpr :=
   VExpr.appN
     (.const constructor.familyName (VLevel.params source.uvars))

Lean4Lean/Theory/NestedInductive.lean

@@ -385,7 +385,7 @@ namespace NestedBlockChecked
 variable {source : VInductDecl}
 
 /-- The main family name owning the restored recursor inventory. -/
-def mainName (nested : NestedBlockChecked source) : Name :=
+def mainName (_nested : NestedBlockChecked source) : Name :=
   match source.types with
   | ty :: _ => ty.name
   | [] => .anonymous

Lean4Lean/Theory/Projection.lean

@@ -356,7 +356,7 @@ private theorem VExpr.instRevAt_appN_projection
   | cons arg args ih =>
       simp only [VExpr.instRevAt, VExpr.instN_appN]
       rw [ih]
-      simp only [List.map_map, Function.comp_def, VExpr.instRevAt]
+      simp only [List.map_map, Function.comp_def]
 
 private theorem VExpr.map_instRevAt_closedN (args es : List VExpr)
     (k : Nat) (hclosed : ∀ e ∈ es, e.ClosedN k) :
@@ -902,8 +902,7 @@ def projectionMinorType (view : VStructureView)
     (view.structureType levels params).instL ls =
       view.structureType (levels.map (VLevel.inst ls))
         (params.map (VExpr.instL ls)) := by
-  simp [structureType, VExpr.instL_appN, VExpr.instL,
-    VLevel.inst_inst, Function.comp_def]
+  simp [structureType, VExpr.instL_appN, VExpr.instL]
 
 @[simp] theorem structureType_liftN (view : VStructureView)
     (levels : List VLevel) (params : List VExpr) (n k : Nat) :
@@ -924,8 +923,7 @@ def projectionMinorType (view : VStructureView)
     (view.specializedFields levels params).map (VExpr.instL ls) =
       view.specializedFields (levels.map (VLevel.inst ls))
         (params.map (VExpr.instL ls)) := by
-  simp [specializedFields, VExpr.instL_instRevAt,
-    VExpr.instL_instL, VLevel.inst_inst, Function.comp_def]
+  simp [specializedFields, VExpr.instL_instRevAt, VExpr.instL_instL, Function.comp_def]
 
 private def projectionCode (view : VStructureView)
     (levels : List VLevel) (params allFields : List VExpr)
@@ -1070,10 +1068,8 @@ private theorem projectionCode_instN (view : VStructureView)
   · simp [projectionCode, ProjectionCode.instN, VExpr.inst,
       VExpr.instN_lamN_projection, VExpr.instTelN_length,
       hminorVar]
-  · simp [projectionCode, ProjectionCode.instN, VExpr.inst,
-      VExpr.instN_appN, VExpr.instN_lamN_projection,
-      VExpr.instTelN_length, ← VExpr.lift_instN_lo,
-      VExpr.instTelN_lift_projection, List.map_append,
+  · simp [projectionCode, ProjectionCode.instN, VExpr.inst, VExpr.instN_appN,
+      VExpr.instN_lamN_projection, VExpr.instTelN_length, ← VExpr.lift_instN_lo, List.map_append,
       List.map_map, Function.comp_def, hmotive, hminorVar]
 
 private def projectionCodes.go (view : VStructureView)
@@ -1347,8 +1343,7 @@ private theorem projectionCodes.go_get?_typeFn (view : VStructureView)
                       (projectionCodes.go view levels params allFields structType
                         fields fieldSorts (i + 1)
                           (previous ++ [head])).take j := by
-                simp [head, projectionCodes.go, List.take,
-                  List.append_assoc]
+                simp [head, projectionCodes.go, List.append_assoc]
               rw [hpref]
               simpa only [Nat.add_assoc, Nat.add_comm,
                 Nat.add_left_comm] using htypeFn
@@ -1999,7 +1994,7 @@ private theorem WF.motiveLevel_projectionLevels
   rw [← structureType_liftN]
   apply projectionCodes.go_liftN
   · rfl
-  · simp [VExpr.liftTelN_length]
+  · simp
 
 @[simp] theorem WF.projectionCodes_instN
     (self : VStructureView.WF view env) (henv : env.Ordered)
@@ -2014,7 +2009,7 @@ private theorem WF.motiveLevel_projectionLevels
   rw [← structureType_instN]
   apply projectionCodes.go_instN
   · rfl
-  · simp [VExpr.instTelN_length]
+  · simp
 
 /-- The exact lower-layer structure-eta descriptor generated by a checked
 structure view.  Its projector syntax is the deterministic projector program
@@ -2131,7 +2126,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.constructorParamsSpine
     (self : VStructureView.WF view env) (henv : env.Ordered)
     {U : Nat} {Γ : List VExpr} (levels : List VLevel)
     (hlevels : ∀ level ∈ levels, level.WF U)
-    (hlevelsLength : levels.length = view.uvars)
+    (_hlevelsLength : levels.length = view.uvars)
     (params : List VExpr) (hparamsLength : params.length = view.nparams)
     (paramsSpine : ∃ resultLevel,
       env.SpineWF U Γ (view.familyType.instL levels)
@@ -2228,7 +2223,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.familyParamsSpine_of_constructor
     (self : VStructureView.WF view env) (henv : env.Ordered)
     {U : Nat} {Γ : List VExpr} (levels : List VLevel)
     (hlevels : ∀ level ∈ levels, level.WF U)
-    (hlevelsLength : levels.length = view.uvars)
+    (_hlevelsLength : levels.length = view.uvars)
     (params : List VExpr) (hparamsLength : params.length = view.nparams)
     {target cursor : VExpr}
     (constructorSpine : env.SpineWF U Γ
@@ -2321,7 +2316,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.specializedFields_onSortTel
     (self : VStructureView.WF view env) (henv : env.Ordered)
     {U : Nat} {Γ : List VExpr} (levels : List VLevel)
     (hlevels : ∀ level ∈ levels, level.WF U)
-    (hlevelsLength : levels.length = view.uvars)
+    (_hlevelsLength : levels.length = view.uvars)
     (params : List VExpr) (hparamsLength : params.length = view.nparams)
     (paramsSpine : ∃ resultLevel,
       env.SpineWF U Γ (view.familyType.instL levels)
@@ -2505,7 +2500,7 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType
     (hmotiveLevel :
       view.generation.motiveLevel.inst
           (view.projectionLevels fieldSort levels) = fieldSort)
-    (structIsType : env.IsType U Γ
+    (_structIsType : env.IsType U Γ
       (view.structureType levels params))
     {typeFn minor major : VExpr}
     (typeFnType : env.HasType U Γ typeFn
@@ -2623,31 +2618,17 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType
             (view.specializedFields levels params) typeFn)
           (.forallE (view.structureType levels params).lift
             (.app (typeFn.liftN 2) (.bvar 0))) := by
-    simp [gen, pLevels, recRest, k, ni,
-      VInductDecl.GenerationChecked.minorTypes,
-      VInductDecl.GenerationChecked.minorTypesAux,
-      VInductDecl.GenerationChecked.minorType,
-      VInductDecl.GenerationChecked.idxTel,
-      VInductDecl.NormalizedCtor.fieldsR,
-      VInductDecl.NormalizedCtor.recArgsR,
-      VInductDecl.NormalizedCtor.resultIndicesR,
-      VInductDecl.ihsFromRecArgs,
-      VStructureView.projectionMinorType,
-      VStructureView.projectionConstructorApp,
-      view.constructor_eq, view.raw_indices_eq,
-      hresultIndices, view.recursive_eq,
-      VExpr.instL_forallN, VExpr.instL_appN,
-      VExpr.liftTelN_instL,
-      VExpr.instL_instL, VExpr.instN_forallN,
-      VExpr.instTelN,
-      VExpr.instRevAt_forallN_projection,
-      VExpr.instRevAt_forallE_projection,
-      VExpr.instN_appN, VExpr.instRev,
-      VExpr.instRev_appN, List.map_append,
-      VExpr.bvarRevRange, List.map_append,
+    simp [gen, pLevels, recRest, k, ni, VInductDecl.GenerationChecked.minorTypes,
+      VInductDecl.GenerationChecked.minorTypesAux, VInductDecl.GenerationChecked.minorType,
+      VInductDecl.GenerationChecked.idxTel, VInductDecl.NormalizedCtor.fieldsR,
+      VInductDecl.NormalizedCtor.recArgsR, VInductDecl.NormalizedCtor.resultIndicesR,
+      VInductDecl.ihsFromRecArgs, VStructureView.projectionMinorType,
+      VStructureView.projectionConstructorApp, view.constructor_eq, view.raw_indices_eq,
+      hresultIndices, view.recursive_eq, VExpr.instL_forallN, VExpr.instL_appN,
+      VExpr.liftTelN_instL, VExpr.instL_instL, VExpr.instN_forallN, VExpr.instTelN,
+      VExpr.instRevAt_forallN_projection, List.map_append, VExpr.bvarRevRange, List.map_append,
       List.map_map, Function.comp_def,
-      VStructureView.sourceLevels_projectionLevels view fieldSort levels
-        hlevelsLength, hparamsLength]
+      VStructureView.sourceLevels_projectionLevels view fieldSort levels hlevelsLength]
     change VExpr.forallE _ _ = VExpr.forallE _ _
     congr 1
     · have hfieldTel :=
@@ -2685,9 +2666,8 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType
             (view.constructor.rawFields view.source.nparams).length := by
         simp [VStructureView.specializedFields,
           VStructureView.fields]
-      simp only [VExpr.forallN, VExpr.instL,
-        VExpr.bvarRevRange_map_instL,
-        hliftedLength, hspecializedLength, hparamsLength]
+      simp only [VExpr.forallN, VExpr.instL, VExpr.bvarRevRange_map_instL, hliftedLength,
+        hspecializedLength]
       rw [hsourceLevels]
       have hbody :=
         VExpr.projectionMinorBody_shape view.constructorName levels
@@ -2702,10 +2682,8 @@ theorem _root_.Lean4Lean.VStructureView.WF.recursorProjection_hasType
         (VLevel.params' view.source.uvars
             view.generation.elimination.offset).map
               (VLevel.inst pLevels) = levels at hsourceLevels
-      simp only [VExpr.forallN, VExpr.liftTelN, List.zipIdx_nil,
-        List.map_nil, VExpr.instTelN, Nat.add_zero,
-        VExpr.instL, VExpr.instL_appN,
-        VExpr.bvarRevRange_map_instL, VExpr.instL]
+      simp only [VExpr.forallN, VExpr.liftTelN, List.zipIdx_nil, List.map_nil, VExpr.instTelN,
+        VExpr.instL, VExpr.instL_appN, VExpr.bvarRevRange_map_instL, VExpr.instL]
       rw [hsourceLevels]
       simpa [gen, hparamsLength, VStructureView.structureType] using
         (VExpr.projectionMajorTail_shape view.name levels params typeFn)
@@ -3294,7 +3272,7 @@ theorem TrProj.mono {env env' : VEnv} (henv : env ≤ env')
   params_length := self.params_length
   paramsSpine := self.paramsSpine.imp fun _ h => h.monoProjection henv
   majorType := self.majorType.mono henv
-  program := self.program.imp fun code ⟨hcode, hresult, htype⟩ =>
+  program := self.program.imp fun _ ⟨hcode, hresult, htype⟩ =>
     ⟨hcode, hresult, htype.mono henv⟩
 
 /-- Weakening acts pointwise on the explicit parameters, major, and computed
@@ -3511,6 +3489,7 @@ structure RegisteredStructureHeadInversion (env : VEnv) : Prop where
       Nonempty (ProjectionConstructorAlignment env U Γ view levels params idx
         code constructorName runtimeMajor runtimeField)
 
+set_option warn.sorry false in
 /-- Public Tier-R registered-head inversion statement.  L4L-16/17 discharge
 the underlying constant-head theorem; projection structural laws consume only
 this stable interface and therefore shed `sorryAx` automatically when it is

Lean4Lean/Theory/Typing/ChurchRosser.lean

@@ -1845,6 +1845,7 @@ theorem StructEq.parRed_right (H : StructEq Γ e₁ e₂)
   have ⟨_, heq⟩ := H.defeq hΓ
   exact H.trans_right hΓ ⟨_, R.defeq hΓ heq.hasType.2⟩
 
+set_option warn.sorry false in
 variable! (hΓ : OnCtx Γ (IsType env univs)) in
 theorem NormalEq.parRed (H1 : Γ ⊢ e₁ ≡ₚ e₂) (H2 : Γ ⊢ e₂ ≫ e₂') :
     ∃ e₁', Γ ⊢ e₁ ≫* e₁' ∧ Γ ⊢ e₁' ≡ₚ e₂' := by