From 29f56ae3bae2c2a892662b2ca4bc91e1173ab6f5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 08:27:42 -0400 Subject: [PATCH 1/2] chore(deps): advance CSLib to Thompson construction --- docbuild/lake-manifest.json | 4 ++-- guide/lake-manifest.json | 4 ++-- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index 5f688cd48..5a2ef0516 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -73,10 +73,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "rev": "82db31eec215b6843be6df283304cc02e736ddef", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "inputRev": "82db31eec215b6843be6df283304cc02e736ddef", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/guide/lake-manifest.json b/guide/lake-manifest.json index 2c0ddd966..7474b7f1c 100644 --- a/guide/lake-manifest.json +++ b/guide/lake-manifest.json @@ -73,10 +73,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "rev": "82db31eec215b6843be6df283304cc02e736ddef", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "inputRev": "82db31eec215b6843be6df283304cc02e736ddef", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lake-manifest.json b/lake-manifest.json index f513ec635..5ab498d69 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "rev": "82db31eec215b6843be6df283304cc02e736ddef", "name": "cslib", "manifestFile": "lake-manifest.json", - "inputRev": "254e30e6d4299c51323aaeaf5f51a4763b375d4a", + "inputRev": "82db31eec215b6843be6df283304cc02e736ddef", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", diff --git a/lakefile.toml b/lakefile.toml index bfad97b80..4eb6831dc 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -33,7 +33,7 @@ autoImplicit = false [[require]] name = "cslib" git = "https://github.com/leanprover/cslib" -rev = "254e30e6d4299c51323aaeaf5f51a4763b375d4a" +rev = "82db31eec215b6843be6df283304cc02e736ddef" [[lean_lib]] name = "Complexity" From 66c395fa31b1caa1f95a1d358c3dc900e5835d73 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 09:50:31 -0400 Subject: [PATCH 2/2] ci(docs): limit documentation worker pools --- .github/workflows/docs.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index ec877a7a1..8af4daf05 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -34,6 +34,9 @@ jobs: test: "false" lint: "false" - name: Generate API documentation + # Limit Lake/doc-gen4 worker pools to reduce hosted-runner memory pressure. + env: + LEAN_NUM_THREADS: "2" run: DISABLE_EQUATIONS=1 lake -d docbuild build Complexity:docs # Also catches library changes that break one of the guide's examples. - name: Build the guide