[kim-em]

This PR advances TauCeti to 0535b3bf5a083a09c92f18f3f8aa2017f32a803c and Mathlib to 3b531c35df33d6bbe64b4e87dec056211d3a5676, the newest TauCeti commit on v4.35.0-rc3 and its Mathlib. Mathlib's cache for the previous pin b63f6e8 lacks Mathlib.Tactic.CategoryTheory.BicategoryCoherence, so the evaluator's cache-only lake --no-build build TauCeti found that module out of date and every submission failed (for example https://github.com/leanprover/lean-eval-submissions/actions/runs/43348967927). The Mathlib cache for 3b531c3 is complete (8939 of 8939 files), and TauCeti has published its outputs for the new revision. The other transitive pins already match both manifests, and the toolchain is unchanged.

This Mathlib warns when non-module files import it, so the root lakefile sets allowNonModules = true, as #670 does.

The pin no longer matches the Mathlib that AxiomMath/CFSG 5f8042b uses (chosen in #667).

Checked locally with an empty Lake artifact cache, using the trusted root build script from lean-eval-submissions main: TauCeti restores entirely from its cache with nothing compiled, no Mathlib module is rebuilt, and the full catalog builds with no warnings other than sorry. The Python tests pass, and the pipeline toolchain contract accepts the pin.

🤖 Prepared with Claude Code

[kim-em]

🤖 Claude says: Closing in favour of a lean-eval CI check that rejects Mathlib pins whose cache is incomplete, to follow once #670 lands (it moves these pins anyway).