chore(repository): improve documentation and CI

.github/workflows/check-imports.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
 
       - name: Check that all files are imported
         run: ./scripts/check-imports.sh

.github/workflows/ci.yml

@@ -15,31 +15,28 @@ jobs:
   build:
     runs-on: ubuntu-latest
     permissions:
-      actions: read
       contents: read
-      issues: write
-      pull-requests: write
 
     steps:
-      - uses: actions/checkout@v7
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
           fetch-depth: 0
 
       - name: Restore Lean cache
-        uses: actions/cache/restore@v6
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
         id: lake-cache
         with:
           path: ./.lake
           key: ${{ runner.os }}-lean-ci-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             ${{ runner.os }}-lean-ci-
 
-      - uses: actions/setup-python@v7
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
         with:
           python-version: "3.12"
 
       - name: Set up Lean environment
-        uses: leanprover/lean-action@v1.5.0
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           auto-config: false
           build: false
@@ -56,7 +53,7 @@ jobs:
 
       - name: Save Lean cache
         if: success() && steps.lake-cache.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v6
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
         with:
           path: ./.lake
           key: ${{ runner.os }}-lean-ci-${{ hashFiles('lake-manifest.json') }}
@@ -66,20 +63,20 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v7
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
           fetch-depth: 0
 
       - name: Restore Lean cache
-        uses: actions/cache/restore@v6
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
         with:
           path: ./.lake
           key: ${{ runner.os }}-lean-ci-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             ${{ runner.os }}-lean-ci-
 
       - name: Set up Lean environment
-        uses: leanprover/lean-action@v1.5.0
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           auto-config: false
           build: false
@@ -102,20 +99,20 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v7
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
           fetch-depth: 0
 
       - name: Restore Lean cache
-        uses: actions/cache/restore@v6
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
         with:
           path: ./.lake
           key: ${{ runner.os }}-lean-ci-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
             ${{ runner.os }}-lean-ci-
 
       - name: Set up Lean environment
-        uses: leanprover/lean-action@v1.5.0
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
         with:
           auto-config: false
           build: false

.github/workflows/docs-integrity.yml

@@ -14,8 +14,8 @@ jobs:
     name: Check Docs Integrity
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v7
-      - uses: actions/setup-python@v7
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
         with:
           python-version: "3.12"
       - name: Check docs integrity

.github/workflows/docs.yml

@@ -0,0 +1,38 @@
+name: API Docs
+
+on:
+  push:
+    branches: [main]
+
+concurrency:
+  group: github-pages
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+  id-token: write
+  pages: write
+
+jobs:
+  docs:
+    name: Build and publish API docs
+    runs-on: ubuntu-latest
+    environment:
+      name: github-pages
+      url: https://verified-zkevm.github.io/PolyFun/docs/
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+        with:
+          fetch-depth: 0
+
+      - name: Build project
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          build-args: --log-level=warning
+
+      - name: Build and publish documentation
+        id: docs
+        uses: leanprover-community/docgen-action@10db47458f91456d87804787d3dfcd914b9a19e3 # main, 2026-08-08
+        with:
+          build-page: false

.github/workflows/linting.yml

@@ -3,20 +3,8 @@ name: Lint Style
 on:
   pull_request:
     types: [opened, synchronize, reopened]
-    paths:
-      - "PolyFun/**/*.lean"
-      - "PolyFun.lean"
-      - "lakefile.toml"
-      - "scripts/nolints-style.txt"
-      - ".github/workflows/linting.yml"
   push:
     branches: [main]
-    paths:
-      - "PolyFun/**/*.lean"
-      - "PolyFun.lean"
-      - "lakefile.toml"
-      - "scripts/nolints-style.txt"
-      - ".github/workflows/linting.yml"
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}

.github/workflows/release-tag.yml

@@ -16,7 +16,7 @@ jobs:
       contents: write
     steps:
     - name: lean-release-tag action
-      uses: leanprover-community/lean-release-tag@v4.18804.0
+      uses: leanprover-community/lean-release-tag@e3858bd52f5d8e45dc5a0166ae18334bf7d23c76 # v4.18804.0
       with:
         do-release: true
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/review.yml

@@ -46,7 +46,7 @@ jobs:
           } >> "$GITHUB_OUTPUT"
         shell: bash
 
-      - uses: alexanderlhicks/lean4repo-utils/review@0.3
+      - uses: alexanderlhicks/lean4repo-utils/review@9404cc0f9aa10d65e4a08d3741a1d41638fb590f # 0.3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           api_key: ${{ secrets.OPENROUTER_KEY }}

AGENTS.md

@@ -205,8 +205,8 @@ listed declaration-by-declaration in `scripts/nolints.json`; regenerate that
 file with the Batteries `runLinter --update` driver when this surface changes,
 and review every new entry rather than treating the file as a blanket waiver.
 
-Lean toolchain, Mathlib, and cslib stay in sync (all currently `v4.32.0`).
-Files should stay under 1500 lines.
+Lean, Mathlib, and cslib stay in sync. The current versions are recorded in
+`lean-toolchain` and `lakefile.toml`. Files should stay under 1500 lines.
 
 ## Further Reading
 

PolyFun/Control/Monad/Equiv.lean

@@ -13,8 +13,6 @@ public import Mathlib.Logic.Function.Defs
 
 This file defines equivalences or isomorphisms between monads, which consists of a pair of monad
 morphisms that are inverses of each other.
-
-TODO: extends the hierarchy with type classes such as `{Nat/Pure/Bind/Monad}EquivClass`
 -/
 
 @[expose] public section

PolyFun/Control/Monad/Hom.lean

@@ -15,9 +15,6 @@ public import Mathlib.CategoryTheory.Monad.Types
 Basic definitions of maps between monads parameterized over any possible output type.
 This is implemented with more constrained universes as `m ⟶ n` in mathlib category theory,
 but this gives definitions more standardized to a cs context.
-
-TODO: Evaluate more fine-grained `PureHom`/`BintHom`/etc, with `Class` versions as well.
-Probably should be in the context of upstreaming things.
 -/
 
 @[expose] public section

PolyFun/IPFunctor/Equiv/Basic.lean

@@ -16,9 +16,7 @@ equivalence of `B`-types compatible with the `A`-equivalence, and a source-index
 law `src_eq`.
 
 This is the indexed analogue of [`PFunctor.Equiv`](../../PFunctor/Equiv/Basic.lean). Like the
-non-indexed version, it is strictly stronger than the lens / chart equivalence: every
-`IPFunctor.Equiv` yields both an `IPFunctor.Lens.Equiv` and an `IPFunctor.Chart.Equiv` (those
-bridges are TODO and live alongside the operations they unblock).
+non-indexed version, it is strictly stronger than lens or chart equivalence.
 -/
 
 @[expose] public section

PolyFun/PFunctor/Equiv/Basic.lean

@@ -167,9 +167,7 @@ def sumProdDistrib (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₁}) (
   equivB := fun
     | ⟨.inl _, _⟩ | ⟨.inr _, _⟩ => _root_.Equiv.refl _
 
-/-- Product distributes over sum: `P * (Q + R) ≃ₚ (P * Q) + (P * R)`
-
-TODO: define in terms of `sumProdDistrib` -/
+/-- Product distributes over sum: `P * (Q + R) ≃ₚ (P * Q) + (P * R)` -/
 @[simps]
 def prodSumDistrib (R : PFunctor.{uA₃, uB₂}) :
     (P * (Q + R) : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂}) ≃ₚ
@@ -414,8 +412,6 @@ def uliftUliftEquiv : P.ulift.ulift ≃ₚ P.ulift :=
     }
   }
 
--- TODO: find better ways to annotate universe levels
-
 /-- Universe lifting commutes with sum -/
 def uliftSumEquiv (Q : PFunctor.{uA₂, uB₁}) :
     (PFunctor.ulift.{_, _, u, v} (P + Q : PFunctor.{max uA₁ uA₂, uB₁})) ≃ₚ

README.md

@@ -42,11 +42,34 @@ lake exe cache get
 lake build
 ```
 
-Requires the toolchain pinned in [`lean-toolchain`](lean-toolchain), along with
-[`mathlib v4.32.0`](https://github.com/leanprover-community/mathlib4) and [`cslib v4.32.0`](https://github.com/leanprover/cslib).
+The repository pins Lean in [`lean-toolchain`](lean-toolchain) and pins Mathlib
+and cslib in [`lakefile.toml`](lakefile.toml). Keep all three versions in sync.
+
+## Example
+
+The following file defines a constant polynomial functor and checks one of its
+basic laws:
+
+```lean
+import PolyFun.PFunctor.Basic
+
+open scoped PFunctor
+
+#check PFunctor.C Nat
+
+example : PFunctor.C PUnit = 1 := PFunctor.C_unit
+```
+
+Save it as `Main.lean` in the repository root and run:
+
+```bash
+lake env lean Main.lean
+```
 
 ## Documentation
 
+- [Generated API documentation](https://verified-zkevm.github.io/PolyFun/docs/):
+  searchable documentation for public declarations.
 - [`AGENTS.md`](AGENTS.md), [`CLAUDE.md`](CLAUDE.md): one-screen guide for
   human and AI contributors. Symlinked.
 - [`CONTRIBUTING.md`](CONTRIBUTING.md): style, naming, attribution, and large-

docs/wiki/gotchas.md

@@ -206,9 +206,10 @@ checks that it is up to date. Stage new files first;
 
 ### 17. Lean toolchain and Mathlib version must stay in sync
 
-Both currently `v4.29.0`. When upgrading, update both
-[`lean-toolchain`](../../lean-toolchain) and the `require mathlib` line
-in [`lakefile.toml`](../../lakefile.toml) simultaneously.
+Lean, Mathlib, and cslib must use the same release. When upgrading, update
+[`lean-toolchain`](../../lean-toolchain) and both dependency pins in
+[`lakefile.toml`](../../lakefile.toml). Then run `lake update` and validate the
+result.
 
 ### 18. Use public references in shared docs
 

docs/wiki/quickstart.md

@@ -118,10 +118,8 @@ deliberately outside the `lake lint` scope.
   runs the community `leanprover-community/lint-style-action` (the Lean-based
   Mathlib text style linter: copyright headers, line length, module
   docstrings).
-- [`../../.github/workflows/summary.yml`](../../.github/workflows/summary.yml):
-  optional AI-generated PR summary; gated on the `OPENROUTER_KEY` repository
-  secret. A preflight check emits a workflow warning if the secret is not set,
-  and the summary job is marked skipped without blocking the PR.
+- [`../../.github/workflows/docs.yml`](../../.github/workflows/docs.yml):
+  builds and publishes searchable API documentation from `main`.
 - [`../../.github/workflows/release-tag.yml`](../../.github/workflows/release-tag.yml)
   and [`../../.github/workflows/review.yml`](../../.github/workflows/review.yml):
   release tagging and review helper workflows ported from