From 2ddb9abf0b130d20003f119aafd0fbef5b14f5a3 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sat, 8 Aug 2026 10:04:36 -0400 Subject: [PATCH 1/2] ci(dependencies): remove automatic updater Stop scheduled Mathlib and Lean upgrade attempts from creating noisy pull requests and failure issues. Dependency upgrades remain deliberate maintainer changes. Closes #115 --- .github/workflows/update.yml | 38 ------------------------------------ 1 file changed, 38 deletions(-) delete mode 100644 .github/workflows/update.yml diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml deleted file mode 100644 index 8c8ee7f1..00000000 --- a/.github/workflows/update.yml +++ /dev/null @@ -1,38 +0,0 @@ -name: Update Dependencies - -on: - schedule: # Sets a schedule to trigger the workflow - - cron: "0 8 */7 * *" # Every 7 days at 08:00 AM UTC - workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface - -jobs: - check-for-updates: # Determines which updates to apply. - runs-on: ubuntu-latest - outputs: - is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }} - new-tags: ${{ steps.check-for-updates.outputs.new-tags }} - steps: - - name: Run the action - id: check-for-updates - uses: leanprover-community/mathlib-update-action@main - with: - intermediate_releases: all - - do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit. - runs-on: ubuntu-latest - permissions: - contents: write # Grants permission to push changes to the repository - issues: write # Grants permission to create or update issues - pull-requests: write # Grants permission to create or update pull requests - needs: check-for-updates - if: ${{ needs.check-for-updates.outputs.is-update-available == 'true' }} - strategy: # Runs for each update discovered by the `check-for-updates` job. - max-parallel: 1 # Ensures that the PRs/issues are created in order. - matrix: - tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }} - steps: - - name: Run the action - id: update-the-repo - uses: leanprover-community/mathlib-update-action/do-update@main - with: - tag: ${{ matrix.tag }} From 42f8ca9888d3aa5dccbd3c2caffe202ebf71f0b3 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sat, 8 Aug 2026 10:08:44 -0400 Subject: [PATCH 2/2] docs(workflows): remove updater references Document the manual dependency upgrade process after removing the scheduled updater. This also removes the broken workflow link from the quickstart guide. --- docs/wiki/generated-files.md | 2 +- docs/wiki/quickstart.md | 16 +++++++--------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/docs/wiki/generated-files.md b/docs/wiki/generated-files.md index a4f2a700..b3b13357 100644 --- a/docs/wiki/generated-files.md +++ b/docs/wiki/generated-files.md @@ -7,7 +7,7 @@ Edit the source of truth, not the output. | `CLAUDE.md` | compatibility symlink | No | Edit `AGENTS.md` | | `PolyFun.lean` | generated module with umbrella public imports | No | `./scripts/update-lib.sh` or `./scripts/check-imports.sh` | | `.lake/` | build artifacts and cache | No | `lake build`, `lake exe cache get` | -| `lake-manifest.json` | resolved dependency lockfile | Manual edits unsafe | `lake update` (or the `update.yml` workflow) | +| `lake-manifest.json` | resolved dependency lockfile | Manual edits unsafe | Update `lean-toolchain` and both dependency pins in `lakefile.toml`, then run `lake update` | ## Important Notes diff --git a/docs/wiki/quickstart.md b/docs/wiki/quickstart.md index 35030850..0b74905f 100644 --- a/docs/wiki/quickstart.md +++ b/docs/wiki/quickstart.md @@ -122,16 +122,14 @@ deliberately outside the `lake lint` scope. 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/release-tag.yml`](../../.github/workflows/release-tag.yml), - [`../../.github/workflows/update.yml`](../../.github/workflows/update.yml), - [`../../.github/workflows/review.yml`](../../.github/workflows/review.yml): - release tagging, dependency-update PRs, and review-helper workflows - ported from +- [`../../.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 [`Verified-zkEVM/ArkLib`](https://github.com/Verified-zkEVM/ArkLib). ## Toolchain -Lean toolchain, Mathlib, and cslib stay in sync. All currently `v4.32.0`. When -upgrading, update [`lean-toolchain`](../../lean-toolchain) and the -`require mathlib` / `require cslib` pins in -[`lakefile.toml`](../../lakefile.toml) simultaneously. +Lean, Mathlib, and cslib stay in sync. To upgrade them, update +[`lean-toolchain`](../../lean-toolchain) and both dependency pins in +[`lakefile.toml`](../../lakefile.toml). Then run `lake update` and validate the +result before opening a pull request.