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"