# Clean-room rebuild of the release tree: no Odanorm build products existed before it.
# host: klein01.math.uni-konstanz.de
# date: 2026-09-25T22:23:08+02:00
# toolchain: leanprover/lean4:v4.34.0
# mathlib rev: db00fb3901b1bb4954f8a2373285959a5930bbfa
#
# The headline axiom sets are #guard_msgs anchors inside Odanorm/Main.lean and are
# therefore checked BY this build.

✔ [8925/8974] Built Odanorm.Defs (5.5s)
✔ [8926/8974] Built Odanorm.MatrixClassify (7.9s)
⚠ [8927/8974] Built Odanorm.Ball.Basic (8.0s)
warning: Odanorm/Ball/Basic.lean:146:30: This simp argument is unused:
  Matrix.mul_neg

Hint: Omit it from the simp argument list.
  [apply] simp only [add_mul, mul_add, Matrix.one_mul, Matrix.mul_one, Matrix.smul_mul, Matrix.mul_smul, smul_neg,
    Matrix.neg_mul, gP_mul_gP hij, gP_mul_gJ hij, gJ_mul_gP hij, gJ_mul_gJ hij, smul_smul]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8928/8974] Built Odanorm.ParityLens (5.1s)
✔ [8929/8974] Built Odanorm.PickCore (5.5s)
✔ [8930/8974] Built Odanorm.Projection (7.1s)
✔ [8931/8974] Built Odanorm.Farkas (9.7s)
⚠ [8932/8974] Built Odanorm.Ball.Bang (7.0s)
warning: Odanorm/Ball/Bang.lean:32:61: This simp argument is unused:
  mulVec_single_one

Hint: Omit it from the simp argument list.
  [apply] simp

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8933/8974] Built Odanorm.S1.Basic (5.0s)
warning: Odanorm/S1/Basic.lean:32:49: Variable name `hst` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hst

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Odanorm/S1/Basic.lean:62:10: `dif_pos` has been deprecated: Use `dite_eq_left` instead
warning: Odanorm/S1/Basic.lean:67:10: `dif_pos` has been deprecated: Use `dite_eq_left` instead
warning: Odanorm/S1/Basic.lean:72:10: `dif_pos` has been deprecated: Use `dite_eq_left` instead
✔ [8934/8974] Built Odanorm.Certificate (5.7s)
✔ [8935/8974] Built Odanorm.Stabilization (11s)
⚠ [8936/8974] Built Odanorm.Ball.Symmetrize (7.9s)
warning: Odanorm/Ball/Symmetrize.lean:60:2: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: Odanorm/Ball/Symmetrize.lean:139:2: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: Odanorm/Ball/Symmetrize.lean:234:27: This simp argument is unused:
  Finset.mul_sum

Hint: Omit it from the simp argument list.
  [apply] simp only [hlp, hlogc]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8937/8974] Built Odanorm.Enlargement (6.6s)
✔ [8938/8974] Built Odanorm.Completion (7.1s)
✔ [8939/8974] Built Odanorm.FarkasRational (6.4s)
⚠ [8940/8974] Built Odanorm.S1.Doignon (6.7s)
warning: Odanorm/S1/Doignon.lean:28:0: automatically included section variable(s) unused in theorem `Odanorm.S1.mem_sol`:
  [DecidableEq ι]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq ι] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
✔ [8941/8974] Built Odanorm.S1.Fan (7.3s)
✔ [8942/8974] Built Odanorm.MatrixBridge (5.8s)
⚠ [8943/8974] Built Odanorm.S1.HDesc (7.0s)
warning: Odanorm/S1/HDesc.lean:50:48: Variable name `hA` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hA

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [8944/8974] Built Odanorm.Ball.Theorem (7.4s)
✔ [8945/8974] Built Odanorm.S1.Chord (10s)
✔ [8946/8974] Built Odanorm.S1.HFull (5.4s)
✔ [8947/8974] Built Odanorm.S1.Face (4.7s)
✔ [8948/8974] Built Odanorm.MatrixWitness (16s)
✔ [8949/8974] Built Odanorm.CellCore (5.4s)
✔ [8950/8974] Built Odanorm.S1.Main (11s)
ℹ [8951/8974] Built Odanorm.Cell_cell101x (6.2s)
info: Odanorm/Cell_cell101x.lean:255:0: Odanorm.Cell101x.cell101x : ∀ (L : Odanorm.MatrixWitness.NF),
  L.Dom → 0 ≤ L.f → L.f < L.e → 0 ≤ Odanorm.MatrixLemma.J2f L → L.Goal
✔ [8952/8974] Built Odanorm.Cited (5.6s)
✔ [8953/8974] Built Odanorm.Cell_cell1001 (14s)
ℹ [8954/8974] Built Odanorm.Cell_cell0000 (14s)
info: Odanorm/Cell_cell0000.lean:224:0: Odanorm.Cell0000.cell0000 : ∀ (L : Odanorm.MatrixWitness.NF),
  L.Dom → 0 ≤ L.e → L.e < L.f → Odanorm.MatrixLemma.Jf L ≤ 0 → Odanorm.MatrixLemma.K2f L ≤ 0 → L.Goal
✔ [8955/8974] Built Odanorm.ContactPolytope (6.9s)
✔ [8956/8974] Built Odanorm.S2.Det (5.8s)
✔ [8957/8974] Built Odanorm.Cell_cell1000high (22s)
✔ [8958/8974] Built Odanorm.S2.Parity (4.6s)
✔ [8959/8974] Built Odanorm.S2.Kernel (5.1s)
✔ [8960/8974] Built Odanorm.S2.Small (6.1s)
✔ [8961/8974] Built Odanorm.S2.Hull (6.7s)
✔ [8962/8974] Built Odanorm.Cell_cell0001 (29s)
✔ [8963/8974] Built Odanorm.Certificate2 (14s)
✔ [8964/8974] Built Odanorm.S2.Octa (6.1s)
⚠ [8965/8974] Built Odanorm.NormalForm (6.6s)
warning: Odanorm/NormalForm.lean:395:48: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Odanorm/NormalForm.lean:401:46: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8966/8974] Built Odanorm.Cell_cell1000low (44s)
✔ [8967/8974] Built Odanorm.MatrixLemma (5.9s)
✔ [8968/8974] Built Odanorm.S2.Interface (22s)
⚠ [8969/8974] Built Odanorm.FourStrips (9.3s)
warning: Odanorm/FourStrips.lean:729:40: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8970/8974] Built Odanorm.FacetDepthCore (9.9s)
✔ [8971/8974] Built Odanorm.WidthLemmaCore (15s)
✔ [8972/8974] Built Odanorm.Main (6.0s)
✔ [8973/8974] Built Odanorm (5.1s)
Build completed successfully (8974 jobs).
