From 7d5888a0cdd384e0b21ce8609840d8749ded8f8e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 13 Nov 2026 09:57:00 +0000
Subject: [PATCH] fix: bump TauCeti and Mathlib to a Mathlib with a complete
 cache

Mathlib b63f6e8's cache lacks Mathlib.Tactic.CategoryTheory.BicategoryCoherence,
so the evaluator's cache-only TauCeti restore found it out of date and failed
every submission. Move to TauCeti 0535b3bf5a, the newest TauCeti commit on
v4.35.0-rc3, and its Mathlib 3b531c3, whose cache is complete. TauCeti has
published its outputs for this revision. This Mathlib warns when non-module
files import it, so allow non-module files as lean-eval#670 does.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 lake-manifest.json | 8 ++++----
 lakefile.toml      | 6 ++++--
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index be874ffb..47a2f3a0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24",
+   "rev": "3b531c35df33d6bbe64b4e87dec056211d3a5676",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24",
+   "inputRev": "3b531c35df33d6bbe64b4e87dec056211d3a5676",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/TauCetiProject/TauCeti",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380",
+   "rev": "0535b3bf5a083a09c92f18f3f8aa2017f32a803c",
    "name": "TauCeti",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380",
+   "inputRev": "0535b3bf5a083a09c92f18f3f8aa2017f32a803c",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/Vilin97/lean-pool.git",
diff --git a/lakefile.toml b/lakefile.toml
index b54b07d7..857e759f 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,7 @@
 name = "lean-eval"
 defaultTargets = ["LeanEval"]
+# Generated benchmark statements retain legacy visibility rules.
+allowNonModules = true
 
 [leanOptions]
 autoImplicit = false
@@ -20,12 +22,12 @@ rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f"
 [[require]]
 name = "TauCeti"
 git = "https://github.com/TauCetiProject/TauCeti"
-rev = "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380"
+rev = "0535b3bf5a083a09c92f18f3f8aa2017f32a803c"
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "b63f6e8a68d220e3b3bc4f3792bb53650d375f24"
+rev = "3b531c35df33d6bbe64b4e87dec056211d3a5676"
 
 [[require]]
 name = "lean-eval-generator"