diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 208fc1f..907f711 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -5,3 +5,58 @@ On top of Mathlib's contribution guidelines, we also enforce the following: Precisely, declarations that belong in an existing Mathlib file `Mathlib.X` will be located in `AlgoLib.Mathlib.X`. We aim to preserve the property that `AlgoLib.Mathlib.X` only imports `Mathlib.X` and files of the form `AlgoLib.Mathlib.Y` where `Mathlib.X` (transitively) imports `Mathlib.Y`. Prerequisites that do not belong in any existing Mathlib file should be located outside the `AlgoLib.Mathlib` folder. + +## Lean version updates + +The `Upgrade stable Lean` workflow checks daily for the latest stable Lean 4 +release. It waits until Mathlib and CSLib both have matching version tags whose +`lean-toolchain` files agree. Missing tags or different toolchains are retried +on later runs. Release candidates and nightlies are excluded. + +Once ready, it updates the toolchain, both dependency pins and current README +version examples, regenerates the manifest, and runs the build, public-import, +declaration-checker and style checks. If all pass, it opens an upgrade PR and +starts CI on that branch. It never merges automatically. If the attempt fails, +it opens an issue naming the failed stage and linking to the logs. If `main` +advances during validation, the attempt also stops so an untested base is not +silently included in the PR. + +An existing upgrade PR is left untouched, including any maintainer fixes. A +closed PR is not recreated. An existing upgrade issue stops daily attempts for +that version; use **Actions → Upgrade stable Lean → Run workflow → Retry an +upgrade with an existing issue** to try again. A failed retry adds a comment to +the same issue; a successful retry opens a PR that closes it when merged. + +For breaking changes, create a manual upgrade branch from current `main` and +link the issue in your PR. Update `lean-toolchain` and the Mathlib and CSLib +requirements in `lakefile.toml`, then regenerate the manifest and check the +library: + +```sh +lake update +lake exe cache get +lake build +lake env lean tests/Import.lean +lake build checkdecls +``` + +Fix any breaking changes before merging. Commit `lake-manifest.json` with the +toolchain and dependency changes, and update the README's version examples and +migration notes. Review changes to the public API even when the build passes. +Configure branch protection on `main` to require **Build project** and +**Lint style**, with branches up to date before merging. + +Under **Settings → Actions → General → Workflow permissions**, enable **Allow +GitHub Actions to create and approve pull requests**. The updater explicitly +dispatches CI on the published branch using the built-in token, so an extra +bot token is not required. Publication or CI-dispatch failures are also reported +in an issue; check whether a PR was already created before retrying. + +After a push to `main` passes both jobs, CI creates the stable Lean version tag +and a GitHub release at that exact tested commit. Release dates provide the +timestamp. Existing tags, including tags made before this workflow, are left +unchanged. Each Lean version gets one automatic tag; use a tested commit hash +for later fixes on the same Lean version. Keeping a tag available does not +automatically backport future fixes to it. Publishing uses the built-in +`GITHUB_TOKEN`; the updater uses it to publish PRs, report failures and dispatch +CI. No extra secret or dependency-update service is needed. diff --git a/.github/scripts/lean-upgrade.cjs b/.github/scripts/lean-upgrade.cjs new file mode 100644 index 0000000..b9f5137 --- /dev/null +++ b/.github/scripts/lean-upgrade.cjs @@ -0,0 +1,146 @@ +const { readFileSync, writeFileSync } = require('node:fs'); +const { join } = require('node:path'); + +const stable = /^v4\.\d+\.\d+$/; +const dependencies = [ + { owner: 'leanprover-community', repo: 'mathlib4', name: 'mathlib' }, + { owner: 'leanprover', repo: 'cslib', name: 'cslib' }, +]; +const marker = version => ``; + +function compareVersions(a, b) { + const left = a.slice(1).split('.').map(Number); + const right = b.slice(1).split('.').map(Number); + for (let i = 0; i < left.length; i++) { + if (left[i] !== right[i]) return left[i] - right[i]; + } + return 0; +} + +async function findIssue(github, repo, version) { + const issues = await github.paginate(github.rest.issues.listForRepo, { + ...repo, state: 'all', creator: 'github-actions[bot]', per_page: 100, + }); + return issues.find(issue => !issue.pull_request && issue.body?.includes(marker(version))); +} + +async function selectUpgrade({ github, context, core, retry = false, + toolchain = readFileSync('lean-toolchain', 'utf8').trim() }) { + core.setOutput('ready', 'false'); + const current = /^leanprover\/lean4:(v4\.\d+\.\d+)(-rc\d+)?$/.exec(toolchain); + if (!current) throw new Error(`Unexpected project toolchain: ${toolchain}`); + const { data: release } = await github.rest.repos.getLatestRelease({ + owner: 'leanprover', repo: 'lean4', + }); + const version = release.tag_name; + if (release.draft || release.prerelease || !stable.test(version)) { + throw new Error('Latest release does not identify a stable Lean 4 version.'); + } + const order = compareVersions(version, current[1]); + if (order < 0 || (order === 0 && !current[2])) { + core.info(`Already using ${version} or a newer toolchain.`); + return 'current'; + } + + const branch = `automation/lean-${version}`; + const prs = await github.paginate(github.rest.pulls.list, { + ...context.repo, state: 'all', base: 'main', + head: `${context.repo.owner}:${branch}`, per_page: 100, + }); + if (prs.length) { + core.info(`An upgrade PR for ${version} already exists; preserving it and its branch.`); + return 'tracked'; + } + const issue = await findIssue(github, context.repo, version); + if (issue && !retry) { + core.info(`Upgrade tracked in #${issue.number}; use manual retry to attempt it again.`); + return 'tracked'; + } + core.setOutput('version', version); + core.setOutput('branch', branch); + core.setOutput('issue', issue?.number ?? ''); + core.setOutput('issue-reference', issue ? `Closes #${issue.number}` : ''); + + const target = `leanprover/lean4:${version}`; + for (const { owner, repo, name } of dependencies) { + let data; + try { + ({ data } = await github.rest.repos.getContent({ + owner, repo, path: 'lean-toolchain', ref: `refs/tags/${version}`, + })); + } catch (error) { + if (error.status !== 404) throw error; + core.info(`Waiting for ${name} tag ${version} and its lean-toolchain.`); + return 'waiting'; + } + if (data.encoding !== 'base64' || typeof data.content !== 'string') { + throw new Error(`Unexpected lean-toolchain response from ${name}.`); + } + if (Buffer.from(data.content, 'base64').toString('utf8').trim() !== target) { + core.info(`Waiting: ${name} ${version} uses a different Lean toolchain.`); + return 'waiting'; + } + } + core.setOutput('ready', 'true'); + return 'ready'; +} + +function updateLakefile(source, version) { + const seen = new Set(); + const updated = source.split(/(?=^\[)/m).map(section => { + if (!section.startsWith('[[require]]')) return section; + const name = /^name[ \t]*=[ \t]*"([^"\n]+)"[ \t]*(?:#.*)?$/m.exec(section)?.[1]; + const dependency = dependencies.find(dep => dep.name === name); + if (!dependency) return section; + const scope = /^scope[ \t]*=[ \t]*"([^"\n]+)"[ \t]*(?:#.*)?$/m.exec(section)?.[1]; + const revision = /^rev([ \t]*=[ \t]*)"[^"\n]*"([^\n]*)$/gm; + if (seen.has(name) || scope !== dependency.owner || [...section.matchAll(revision)].length !== 1) { + throw new Error(`Expected one scoped, pinned requirement for ${name}.`); + } + seen.add(name); + return section.replace(revision, (_match, spacing, comment) => `rev${spacing}"${version}"${comment}`); + }).join(''); + if (seen.size !== dependencies.length) throw new Error('Expected both Mathlib and CSLib requirements.'); + return updated; +} + +function prepareUpgrade({ version, root = '.' }) { + if (!stable.test(version)) throw new Error('Expected a stable Lean 4 version.'); + const toolchain = readFileSync(join(root, 'lean-toolchain'), 'utf8').trim(); + const current = /^leanprover\/lean4:(v4\.\d+\.\d+)(-rc\d+)?$/.exec(toolchain); + if (!current || compareVersions(version, current[1]) < 0 || + (version === current[1] && !current[2])) throw new Error('Expected a newer stable toolchain.'); + + // Validate every edit before writing any file. Lake regenerates the manifest next. + const lakefile = updateLakefile(readFileSync(join(root, 'lakefile.toml'), 'utf8'), version); + const oldVersion = current[1] + (current[2] ?? ''); + const readme = readFileSync(join(root, 'README.md'), 'utf8') + .replaceAll(oldVersion, version) + .replaceAll(`Lean ${oldVersion.slice(1)}`, `Lean ${version.slice(1)}`); + writeFileSync(join(root, 'lean-toolchain'), `leanprover/lean4:${version}\n`); + writeFileSync(join(root, 'lakefile.toml'), lakefile); + writeFileSync(join(root, 'README.md'), readme); +} + +async function reportFailure({ github, context, core, version, steps }) { + if (!stable.test(version)) throw new Error('Cannot report an unknown upgrade version.'); + const failed = Object.entries(steps).filter(([, step]) => step.outcome === 'failure').map(([name]) => name); + const run = `https://github.com/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`; + const details = `Automatic upgrade to ${version} failed at: **${failed.join(', ') || 'unknown stage'}**.\n\n` + + `[Inspect the failed steps and logs](${run}). No upgrade is merged automatically.\n\n` + + 'Fix the dependency/proof conflict in a manual upgrade PR, or rerun **Upgrade stable Lean** with ' + + '**Retry an upgrade with an existing issue** after resolving the failure.\n\n' + + 'A build failure may also come from tooling or network errors; check the linked log before changing proofs.'; + const existing = await findIssue(github, context.repo, version); + if (existing) { + await github.rest.issues.createComment({ ...context.repo, issue_number: existing.number, body: details }); + core.notice(`Retry failed; details added to #${existing.number}.`); + return 'commented'; + } + const { data: issue } = await github.rest.issues.create({ ...context.repo, + title: `Lean ${version} upgrade needs attention`, body: `${marker(version)}\n\n${details}` }); + core.notice(`Upgrade needs attention: ${issue.html_url}`); + return 'created'; +} + +module.exports = { selectUpgrade, prepareUpgrade, reportFailure }; diff --git a/.github/scripts/lean-upgrade.test.cjs b/.github/scripts/lean-upgrade.test.cjs new file mode 100644 index 0000000..a085c8f --- /dev/null +++ b/.github/scripts/lean-upgrade.test.cjs @@ -0,0 +1,222 @@ +const assert = require('node:assert/strict'); +const test = require('node:test'); +const { mkdtempSync, readFileSync, writeFileSync, rmSync } = require('node:fs'); +const { tmpdir } = require('node:os'); +const { join } = require('node:path'); +const { selectUpgrade, prepareUpgrade, reportFailure } = require('./lean-upgrade.cjs'); + +function fixture(options = {}) { + const version = options.version ?? 'v4.36.0'; + const requests = [], created = [], comments = [], outputs = {}; + const github = { + rest: { + repos: { + getLatestRelease: async () => ({ data: { + tag_name: version, draft: false, prerelease: false, ...options.release, + } }), + getContent: async request => { + requests.push(request); + if (request.repo === options.missing) throw { status: 404 }; + if (options.error) throw options.error; + return { data: { + encoding: 'base64', + content: Buffer.from(request.repo === options.mismatched + ? 'leanprover/lean4:v4.35.0\n' : `leanprover/lean4:${version}\n`).toString('base64'), + } }; + }, + }, + pulls: { list: () => {} }, + issues: { + listForRepo: () => {}, + create: async issue => { + created.push(issue); + return { data: { html_url: 'https://github.com/example/AlgoLib/issues/1' } }; + }, + createComment: async comment => { comments.push(comment); }, + }, + }, + paginate: async (method, args) => { + assert.equal(args.state, 'all'); + if (method === github.rest.pulls.list) { + assert.equal(args.head, `example:automation/lean-${version}`); + return options.prs ?? []; + } + assert.equal(args.creator, 'github-actions[bot]'); + return options.issues ?? []; + }, + }; + const args = { github, context: { repo: { owner: 'example', repo: 'AlgoLib' }, runId: 42 }, + core: { info() {}, notice() {}, setOutput(key, value) { outputs[key] = value; } } }; + return { + requests, created, comments, outputs, + select: () => selectUpgrade({ ...args, retry: options.retry, + toolchain: options.toolchain ?? 'leanprover/lean4:v4.35.0' }), + report: steps => reportFailure({ ...args, version, steps }), + }; +} + +test('prepares only when both matching tagged toolchains are available', async () => { + const f = fixture(); + assert.equal(await f.select(), 'ready'); + assert.deepEqual(f.requests.map(r => [r.owner, r.repo, r.ref]), [ + ['leanprover-community', 'mathlib4', 'refs/tags/v4.36.0'], + ['leanprover', 'cslib', 'refs/tags/v4.36.0'], + ]); + assert.equal(f.outputs.ready, 'true'); + assert.equal(f.outputs.branch, 'automation/lean-v4.36.0'); + assert.equal(f.created.length, 0); // Readiness itself is not a failure notification. +}); + +test('does not upgrade the current version or downgrade a newer toolchain', async () => { + for (const toolchain of ['v4.36.0', 'v4.37.0', 'v4.37.0-rc1']) { + const f = fixture({ toolchain: `leanprover/lean4:${toolchain}` }); + assert.equal(await f.select(), 'current'); + assert.equal(f.requests.length, 0); + assert.equal(f.outputs.ready, 'false'); + } +}); + +test('compares versions numerically and accepts the stable successor to an RC', async () => { + for (const [current, version] of [['v4.9.0', 'v4.10.0'], ['v4.35.0', 'v4.35.1'], + ['v4.36.0-rc2', 'v4.36.0']]) { + const f = fixture({ toolchain: `leanprover/lean4:${current}`, version }); + assert.equal(await f.select(), 'ready'); + } +}); + +test('waits quietly for missing or mismatched dependencies and retries later', async () => { + for (const repo of ['mathlib4', 'cslib']) { + for (const condition of ['missing', 'mismatched']) { + const options = { [condition]: repo }; + const f = fixture(options); + assert.equal(await f.select(), 'waiting'); + assert.equal(f.outputs.ready, 'false'); + assert.equal(f.created.length, 0); + delete options[condition]; + assert.equal(await f.select(), 'ready'); + } + } +}); + +test('preserves existing open or closed upgrade PRs even on manual retry', async () => { + for (const state of ['open', 'closed']) { + const f = fixture({ prs: [{ state }], retry: true }); + assert.equal(await f.select(), 'tracked'); + assert.equal(f.outputs.ready, 'false'); + assert.equal(f.requests.length, 0); + } +}); + +test('an issue stops repeated scheduled builds but allows an explicit retry', async () => { + for (const state of ['open', 'closed']) { + const options = { issues: [{ number: 17, state, body: '' }] }; + const f = fixture(options); + assert.equal(await f.select(), 'tracked'); + options.retry = true; + assert.equal(await f.select(), 'ready'); + assert.equal(f.outputs['issue-reference'], 'Closes #17'); + } +}); + +test('previous-version issues do not suppress a new upgrade', async () => { + const f = fixture({ issues: [{ body: '' }] }); + assert.equal(await f.select(), 'ready'); +}); + +test('rejects draft, prerelease and unexpected release responses', async () => { + for (const release of [{ draft: true }, { prerelease: true }, + { tag_name: 'v4.36.0-rc2' }, { tag_name: 'nightly' }]) { + const f = fixture({ release }); + await assert.rejects(f.select(), /stable Lean 4 version/); + assert.equal(f.outputs.ready, 'false'); + } +}); + +test('reports API failures instead of treating them as missing dependencies', async () => { + for (const status of [403, 429, 500]) { + const error = Object.assign(new Error('API failure'), { status }); + const f = fixture({ error }); + await assert.rejects(f.select(), error); + assert.equal(f.outputs.ready, 'false'); + } +}); + +test('failed resolve, build, or base validation creates an issue with the run log', async () => { + for (const stage of ['resolve', 'build', 'base']) { + const f = fixture(); + assert.equal(await f.report({ [stage]: { outcome: 'failure' }, checks: { outcome: 'skipped' } }), 'created'); + assert.equal(f.created.length, 1); + assert.match(f.created[0].body, new RegExp(`\\*\\*${stage}\\*\\*`)); + assert.match(f.created[0].body, /actions\/runs\/42/); + assert.match(f.created[0].body, /algolib-lean-upgrade:v4\.36\.0/); + } +}); + +test('a failed manual retry adds details to the existing issue without replacing its body', async () => { + const issue = { number: 17, body: '\nMaintainer notes' }; + const f = fixture({ issues: [issue] }); + assert.equal(await f.report({ resolve: { outcome: 'failure' } }), 'commented'); + assert.equal(f.created.length, 0); + assert.equal(f.comments[0].issue_number, 17); + assert.match(issue.body, /Maintainer notes/); +}); + +const lakefile = `name = "AlgoLib" +version = "0.1.0" +[[require]] +name = "cslib" +scope = "leanprover" +rev = "v4.35.0" # keep this comment +[[require]] +name = "checkdecls" +scope = "PatrickMassot" +rev = "checker-commit" +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "v4.35.0" +[[lean_lib]] +name = "AlgoLib" +`; + +function project(t, overrides = {}) { + const root = mkdtempSync(join(tmpdir(), 'algolib-upgrade-test-')); + t.after(() => rmSync(root, { recursive: true, force: true })); + const files = { + 'lean-toolchain': 'leanprover/lean4:v4.35.0\n', + 'lakefile.toml': lakefile, + 'README.md': 'Use v4.35.0 with Lean 4.35.0. Older releases: v4.27.0.\n', + 'lake-manifest.json': '{"regenerated": "by lake update"}\n', + ...overrides, + }; + for (const [name, content] of Object.entries(files)) writeFileSync(join(root, name), content); + return { root, files, read: name => readFileSync(join(root, name), 'utf8') }; +} + +test('updates both pinned requirements and current README examples without touching the checker', t => { + const p = project(t); + prepareUpgrade({ root: p.root, version: 'v4.36.0' }); + assert.equal(p.read('lean-toolchain'), 'leanprover/lean4:v4.36.0\n'); + assert.equal(p.read('lakefile.toml'), lakefile.replaceAll('v4.35.0', 'v4.36.0')); + assert.equal(p.read('README.md'), 'Use v4.36.0 with Lean 4.36.0. Older releases: v4.27.0.\n'); + assert.equal(p.read('lake-manifest.json'), p.files['lake-manifest.json']); +}); + +test('invalid or missing requirements leave every file untouched', t => { + for (const broken of [lakefile.replace('name = "cslib"', 'name = "other"'), + lakefile.replace('scope = "leanprover"', 'scope = "other"'), + lakefile.replace('rev = "v4.35.0" # keep this comment', ''), + lakefile + '\n[[require]]\nname = "mathlib"\nscope = "leanprover-community"\nrev = "old"\n']) { + const p = project(t, { 'lakefile.toml': broken }); + assert.throws(() => prepareUpgrade({ root: p.root, version: 'v4.36.0' }), /Expected/); + for (const [name, original] of Object.entries(p.files)) assert.equal(p.read(name), original); + } +}); + +test('preparing an already current, older, or prerelease target is rejected without edits', t => { + for (const version of ['v4.35.0', 'v4.34.0', 'v4.36.0-rc1']) { + const p = project(t); + assert.throws(() => prepareUpgrade({ root: p.root, version }), /Expected/); + for (const [name, original] of Object.entries(p.files)) assert.equal(p.read(name), original); + } +}); diff --git a/.github/workflows/lean-release-tag.yml b/.github/workflows/lean-release-tag.yml deleted file mode 100644 index 0878e44..0000000 --- a/.github/workflows/lean-release-tag.yml +++ /dev/null @@ -1,19 +0,0 @@ -on: - push: - branches: - - 'main' - - 'master' - paths: - - 'lean-toolchain' - -jobs: - lean-release-tag: - name: Add Lean release tag - runs-on: ubuntu-latest - permissions: - contents: write - steps: - - name: lean-release-tag action - uses: leanprover-community/lean-release-tag@9ca7ed09e240259871327bfc3a3a8d8c4bcb41aa - with: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 3e24181..1cb66db 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -27,6 +27,9 @@ jobs: run: | ! (find AlgoLib -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^(public )?(meta )?import Mathlib$') + - name: Test the Lean upgrade automation + run: node --test .github/scripts/*.test.cjs + build: name: Build project runs-on: ubuntu-latest @@ -62,3 +65,36 @@ jobs: # website/ is plain static HTML, not a Jekyll site. The action still copies # the API docs and blueprint into website/, then uploads that folder directly. build-page: false + + release: + name: Release tested Lean version + needs: [style_lint, build] + if: github.event_name == 'push' && github.ref == 'refs/heads/main' + runs-on: ubuntu-latest + concurrency: + group: lean-release + cancel-in-progress: false + permissions: + contents: write + steps: + - uses: actions/checkout@v6 + - name: Publish a new stable version once + env: + GH_TOKEN: ${{ github.token }} + shell: bash + run: | + set -euo pipefail + toolchain=$(cat lean-toolchain) + if [[ ! "$toolchain" =~ ^leanprover/lean4:(v[0-9]+\.[0-9]+\.[0-9]+)$ ]]; then + echo "Skipping non-stable toolchain: $toolchain" + exit 0 + fi + tag="${BASH_REMATCH[1]}" + existing=$(git ls-remote --tags origin "refs/tags/$tag") + if [[ -n "$existing" ]]; then + echo "Keeping existing tag $tag unchanged." + exit 0 + fi + # Tag the commit that passed this run, including all upgrade fixes. + gh release create "$tag" --target "$GITHUB_SHA" \ + --title "AlgoLib for Lean $tag" --generate-notes diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 2629d9e..e1ce8bb 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -1,42 +1,147 @@ -name: Update Dependencies +name: Upgrade stable Lean on: schedule: - - cron: "37 */6 * * *" # Check for updates 37 minutes past every six hours + - cron: '37 5 * * *' # Daily at 05:37 UTC workflow_dispatch: + inputs: + retry: + description: Retry an upgrade with an existing issue + type: boolean + default: false + +permissions: + contents: write + pull-requests: write + issues: write + actions: write + +concurrency: + group: stable-lean-upgrade + cancel-in-progress: false jobs: - bump: + upgrade: runs-on: ubuntu-latest - permissions: - contents: write - pull-requests: write steps: - uses: actions/checkout@v6 + with: + ref: main - - name: Bump to latest mathlib - id: bump - uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main + - name: Select a matching stable release + id: select + uses: actions/github-script@v9 + with: + script: | + const { selectUpgrade } = require('./.github/scripts/lean-upgrade.cjs'); + await selectUpgrade({ github, context, core, + retry: context.eventName === 'workflow_dispatch' && context.payload.inputs?.retry === 'true' }); - - name: Open or update PR - if: steps.bump.outputs.updated == 'true' - uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main + - name: Update toolchain, dependency pins and README + id: prepare + if: steps.select.outputs.ready == 'true' + uses: actions/github-script@v9 + env: + TARGET_VERSION: ${{ steps.select.outputs.version }} with: - title: ${{ steps.bump.outputs.pr-title }} - message: ${{ steps.bump.outputs.bump-description }} - commit-message: ${{ steps.bump.outputs.commit-message }} + script: | + const { prepareUpgrade } = require('./.github/scripts/lean-upgrade.cjs'); + prepareUpgrade({ version: process.env.TARGET_VERSION }); - open-issue: - runs-on: ubuntu-latest - permissions: - issues: write - contents: write - pull-requests: write - steps: - - uses: actions/checkout@v6 + - name: Install Lean tooling + id: tooling + if: steps.select.outputs.ready == 'true' + uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0 + with: + auto-config: 'false' + build: 'false' + test: 'false' + lint: 'false' + use-mathlib-cache: 'false' + use-github-cache: 'false' + + - name: Resolve and lock dependencies + id: resolve + if: steps.select.outputs.ready == 'true' + env: + MATHLIB_NO_CACHE_ON_UPDATE: '1' + run: lake update + + - name: Build the upgrade + id: build + if: steps.select.outputs.ready == 'true' + uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # v1.2.0 + + - name: Check imports, declaration checker and style + id: checks + if: steps.select.outputs.ready == 'true' + shell: bash + run: | + lake env lean tests/Import.lean + lake build checkdecls + if (find AlgoLib -name '*.lean' -type f -print0 | xargs -0 grep -E -n '^(public )?(meta )?import Mathlib$'); then + echo 'Use precise Mathlib imports before upgrading.' + exit 1 + fi + node --test .github/scripts/*.test.cjs + git diff --check + + - name: Ensure main did not change during validation + id: base + if: steps.select.outputs.ready == 'true' + run: | + git fetch origin main + if [ "$(git rev-parse HEAD)" != "$(git rev-parse FETCH_HEAD)" ]; then + echo 'Main advanced during validation; retry against the updated base.' + exit 1 + fi + + - name: Open the tested upgrade PR + id: pr + if: >- + steps.select.outputs.ready == 'true' && + steps.resolve.outcome == 'success' && + steps.build.outcome == 'success' && + steps.checks.outcome == 'success' && + steps.base.outcome == 'success' + uses: peter-evans/create-pull-request@v8 + with: + base: main + branch: ${{ steps.select.outputs.branch }} + add-paths: | + lean-toolchain + lakefile.toml + lake-manifest.json + README.md + title: 'chore: upgrade Lean and dependencies to ${{ steps.select.outputs.version }}' + commit-message: 'chore: upgrade Lean and dependencies to ${{ steps.select.outputs.version }}' + body: | + Upgrade Lean, Mathlib and CSLib to the matching stable release. + Dependency resolution, the build, public imports, declaration-checker tooling and style checks passed. + The manifest was regenerated and current README version examples were updated. + + Review public API changes and migration notes before merging. This PR is never merged automatically. + Subsequent scheduled runs leave this PR and any maintainer fixes untouched. + + Validation: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }} + ${{ steps.select.outputs.issue-reference }} + + - name: Run CI on the published PR branch + id: ci + if: steps.pr.outputs.pull-request-number != '' + env: + GH_TOKEN: ${{ github.token }} + PR_BRANCH: ${{ steps.select.outputs.branch }} + run: gh workflow run push.yml --ref "$PR_BRANCH" - - name: Open or update incompatibility issue and PR - uses: leanprover-community/downstream-reports/.github/actions/track-incompatibility@main + - name: Report an unsuccessful upgrade + if: failure() && steps.select.outputs.version != '' + uses: actions/github-script@v9 + env: + TARGET_VERSION: ${{ steps.select.outputs.version }} + STEP_RESULTS: ${{ toJSON(steps) }} with: - open-issue: false - open-pr: true + script: | + const { reportFailure } = require('./.github/scripts/lean-upgrade.cjs'); + await reportFailure({ github, context, core, version: process.env.TARGET_VERSION, + steps: JSON.parse(process.env.STEP_RESULTS) }); diff --git a/README.md b/README.md index 9f75602..23ca37a 100644 --- a/README.md +++ b/README.md @@ -45,14 +45,14 @@ Add the following to your project's `lakefile.toml`: [[require]] name = "AlgoLib" git = "https://github.com/cslib-community/AlgoLib" -rev = "main" +rev = "v4.35.0" ``` Alternatively, if your project uses `lakefile.lean`, add: ```lean require AlgoLib from git - "https://github.com/cslib-community/AlgoLib" @ "main" + "https://github.com/cslib-community/AlgoLib" @ "v4.35.0" ``` Use the configuration format your project already uses. The package name is @@ -105,10 +105,20 @@ toolchain and dependencies. ### Pinning a revision -The examples above follow `main` when you run `lake update AlgoLib`. For a -reproducible project, replace `main` with the full commit hash of a revision you -have tested, and commit the generated `lake-manifest.json`. Use the -`lean-toolchain` from that same AlgoLib revision. +The examples above use the fixed `v4.35.0` tag for Lean 4.35.0. To use an older +Lean version, choose an available matching [tag](https://github.com/cslib-community/AlgoLib/tags) +and use the `lean-toolchain` from that revision. Only versions with a published +tag are supported this way. + +You can also pin a full commit hash you have tested. Commit the generated +`lake-manifest.json` to keep the resolved dependency versions reproducible. +Use `main` instead of a tag only if you want to follow ongoing development when +running `lake update AlgoLib`. + +New stable Lean versions receive a tag and a dated +[GitHub release](https://github.com/cslib-community/AlgoLib/releases) after CI +passes on `main`. Existing tags stay fixed; later fixes can be selected by their +commit hash. There is no need to put a timestamp in the dependency name. ### Upgrading an existing project @@ -136,6 +146,14 @@ The checkout includes its toolchain and dependency manifest. Keep these files when reproducing a build. See the [contribution guide](.github/CONTRIBUTING.md) before making changes. +CI checks daily for new stable Lean releases and waits for matching Mathlib and +CSLib tags using the same toolchain. It attempts the upgrade and opens a PR if +dependency resolution and build checks pass. If the attempt fails, it opens an +issue with the failed stage and logs. Maintainers review PRs and handle breaking +changes; merging remains manual. CI publishes version tags after successful +merges. See the +[maintenance notes](.github/CONTRIBUTING.md#lean-version-updates) for the process. + ## Repository layout ```text