Skip to content

ci(dependencies): remove automatic updater #116

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
quangvdao merged 2 commits into from
Aug 8, 2026
Merged

ci(dependencies): remove automatic updater #116

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2ddb9ab
ci(dependencies): remove automatic updater
quangvdao Aug 8, 2026
42f8ca9
docs(workflows): remove updater references
quangvdao Aug 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 0 additions & 38 deletions .github/workflows/update.yml
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion docs/wiki/generated-files.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
16 changes: 7 additions & 9 deletions docs/wiki/quickstart.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Loading