diff --git a/.github/workflows/check-imports.yml b/.github/workflows/check-imports.yml index 5535e2c6..e58b7b1d 100644 --- a/.github/workflows/check-imports.yml +++ b/.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 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 75dcdca0..cfd37c42 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,18 +15,15 @@ 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 @@ -34,12 +31,12 @@ jobs: 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,12 +63,12 @@ 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') }} @@ -79,7 +76,7 @@ jobs: ${{ 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,12 +99,12 @@ 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') }} @@ -115,7 +112,7 @@ jobs: ${{ 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 diff --git a/.github/workflows/docs-integrity.yml b/.github/workflows/docs-integrity.yml index e1163f49..f4d29b0b 100644 --- a/.github/workflows/docs-integrity.yml +++ b/.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 diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml new file mode 100644 index 00000000..1961e259 --- /dev/null +++ b/.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 diff --git a/.github/workflows/linting.yml b/.github/workflows/linting.yml index 384e8eb5..636d2dae 100644 --- a/.github/workflows/linting.yml +++ b/.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 }} diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index ddac789a..c71de54e 100644 --- a/.github/workflows/release-tag.yml +++ b/.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 }} diff --git a/.github/workflows/review.yml b/.github/workflows/review.yml index 784271c6..d1628071 100644 --- a/.github/workflows/review.yml +++ b/.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 }} diff --git a/.github/workflows/summary.yml b/.github/workflows/summary.yml deleted file mode 100644 index 61d069c8..00000000 --- a/.github/workflows/summary.yml +++ /dev/null @@ -1,53 +0,0 @@ -name: 'PR Summary' - -# Summary runs on every PR update (open + each new commit). It is SAFE under -# pull_request_target — the OpenRouter secret and write token are in scope even -# for fork PRs — because it never builds or executes PR code: it reads the diff -# and committed source as data, and reads its policy file from the BASE ref (S4). -on: - pull_request_target: - types: [opened, synchronize, reopened] - -concurrency: - group: ${{ github.workflow }}-${{ github.event.pull_request.number }} - cancel-in-progress: true - -permissions: - contents: read - pull-requests: write - issues: read - -jobs: - check-openrouter-key: - name: Check OpenRouter key - runs-on: ubuntu-latest - outputs: - configured: ${{ steps.openrouter.outputs.configured }} - steps: - - name: Check OpenRouter API key - id: openrouter - env: - OPENROUTER_KEY: ${{ secrets.OPENROUTER_KEY }} - run: | - if [[ -z "$OPENROUTER_KEY" ]]; then - echo "configured=false" >> "$GITHUB_OUTPUT" - echo "::warning::OPENROUTER_KEY is not configured; PR summary will be skipped." - else - echo "configured=true" >> "$GITHUB_OUTPUT" - fi - - summarize: - needs: check-openrouter-key - if: needs.check-openrouter-key.outputs.configured == 'true' - runs-on: ubuntu-latest - steps: - - name: Generate PR Summary - uses: alexanderlhicks/lean4repo-utils/summary@0.3 - with: - github_token: ${{ secrets.GITHUB_TOKEN }} - api_key: ${{ secrets.OPENROUTER_KEY }} - github_repository: ${{ github.repository }} - pr_number: ${{ github.event.pull_request.number }} - validate_title: 'true' - # Default model (deepseek/deepseek-v4-flash). additional_instructions_path - # defaults to CONTRIBUTING.md (read from the base ref) when unset. diff --git a/AGENTS.md b/AGENTS.md index fd4b2b3b..3bac8b20 100644 --- a/AGENTS.md +++ b/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 diff --git a/PolyFun/Control/Monad/Equiv.lean b/PolyFun/Control/Monad/Equiv.lean index 3cf217ae..5581fe4d 100644 --- a/PolyFun/Control/Monad/Equiv.lean +++ b/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 diff --git a/PolyFun/Control/Monad/Hom.lean b/PolyFun/Control/Monad/Hom.lean index d1c07fe9..435ea8f0 100644 --- a/PolyFun/Control/Monad/Hom.lean +++ b/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 diff --git a/PolyFun/IPFunctor/Equiv/Basic.lean b/PolyFun/IPFunctor/Equiv/Basic.lean index 8e788b3a..506adc91 100644 --- a/PolyFun/IPFunctor/Equiv/Basic.lean +++ b/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 diff --git a/PolyFun/PFunctor/Equiv/Basic.lean b/PolyFun/PFunctor/Equiv/Basic.lean index 1ca56272..c47cf389 100644 --- a/PolyFun/PFunctor/Equiv/Basic.lean +++ b/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₁})) ≃ₚ diff --git a/README.md b/README.md index c96c2427..40e9166d 100644 --- a/README.md +++ b/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- diff --git a/docs/wiki/gotchas.md b/docs/wiki/gotchas.md index 118dabfd..52a76ef8 100644 --- a/docs/wiki/gotchas.md +++ b/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 diff --git a/docs/wiki/quickstart.md b/docs/wiki/quickstart.md index 0b74905f..3922481a 100644 --- a/docs/wiki/quickstart.md +++ b/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