# Clean-room rebuild of the release tree: no Odanorm build products existed before it.
# host: klein01.math.uni-konstanz.de
# date: 2026-09-26T16:07:49+02:00
# toolchain: leanprover/lean4:v4.34.0
# mathlib rev: db00fb3901b1bb4954f8a2373285959a5930bbfa
# sources: final shortened commit 24e362b plus one docstring fix in Odanorm/Completion.lean
#
# The headline axiom sets are #guard_msgs anchors inside Odanorm/Main.lean and are
# therefore checked BY this build.

✔ [8925/8969] Built Odanorm.Defs (9.5s)
✔ [8926/8969] Built Odanorm.Ball.Basic (12s)
✔ [8927/8969] Built Odanorm.PickCore (5.2s)
✔ [8928/8969] Built Odanorm.ParityLens (5.4s)
✔ [8929/8969] Built Odanorm.Farkas (7.5s)
✔ [8930/8969] Built Odanorm.Ball.Bang (6.6s)
✔ [8931/8969] Built Odanorm.S1.Basic (5.3s)
✔ [8932/8969] Built Odanorm.MatrixClassify (10s)
✔ [8933/8969] Built Odanorm.Ball.Symmetrize (8.1s)
✔ [8934/8969] Built Odanorm.Enlargement (7.2s)
✔ [8935/8969] Built Odanorm.Completion (7.3s)
✔ [8936/8969] Built Odanorm.Stabilization (8.1s)
✔ [8937/8969] Built Odanorm.FarkasRational (7.1s)
✔ [8938/8969] Built Odanorm.S1.Doignon (6.0s)
✔ [8939/8969] Built Odanorm.S1.Fan (6.9s)
✔ [8940/8969] Built Odanorm.S1.Chord (7.1s)
✔ [8941/8969] Built Odanorm.Ball.Theorem (6.4s)
✔ [8942/8969] Built Odanorm.S1.Face (5.2s)
✔ [8943/8969] Built Odanorm.MatrixWitness (12s)
✔ [8944/8969] Built Odanorm.CellCore (5.5s)
✔ [8945/8969] Built Odanorm.S1.Main (9.5s)
✔ [8946/8969] Built Odanorm.Cited (5.6s)
✔ [8947/8969] Built Odanorm.Cell_cell101x (7.2s)
✔ [8948/8969] Built Odanorm.Cell_cell0000 (12s)
✔ [8949/8969] Built Odanorm.ContactPolytope (6.6s)
✔ [8950/8969] Built Odanorm.Cell_cell1001 (15s)
✔ [8951/8969] Built Odanorm.Certificate2 (6.1s)
✔ [8952/8969] Built Odanorm.S2.Det (6.2s)
✔ [8953/8969] Built Odanorm.S2.Kernel (5.0s)
✔ [8954/8969] Built Odanorm.S2.Parity (5.2s)
✔ [8955/8969] Built Odanorm.Cell_cell1000high (25s)
✔ [8956/8969] Built Odanorm.S2.Small (6.2s)
✔ [8957/8969] Built Odanorm.S2.Hull (6.8s)
✔ [8958/8969] Built Odanorm.Cell_cell0001 (31s)
✔ [8959/8969] Built Odanorm.S2.Octa (5.6s)
✔ [8960/8969] Built Odanorm.S2.Interface (6.9s)
⚠ [8961/8969] Built Odanorm.NormalForm (8.1s)
warning: Odanorm/NormalForm.lean:58:36: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8962/8969] Built Odanorm.FourStrips (8.5s)
warning: Odanorm/FourStrips.lean:125:40: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8963/8969] Built Odanorm.FacetDepthCore (8.7s)
warning: Odanorm/FacetDepthCore.lean:519:45: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [8964/8969] Built Odanorm.Cell_cell1000low (62s)
✔ [8965/8969] Built Odanorm.MatrixLemma (5.4s)
✔ [8966/8969] Built Odanorm.WidthLemmaCore (13s)
✔ [8967/8969] Built Odanorm.Main (22s)
✔ [8968/8969] Built Odanorm (5.5s)
Build completed successfully (8969 jobs).
