Skip to content

fix: pin functional test toolchain outside .github/workflows - #176

Merged
austinletson merged 1 commit into
mainfrom
toolchain-pin-outside-workflows
Aug 2, 2026
Merged

fix: pin functional test toolchain outside .github/workflows#176
austinletson merged 1 commit into
mainfrom
toolchain-pin-outside-workflows

Conversation

@austinletson

Copy link
Copy Markdown
Collaborator

The nightly Update Functional Test Toolchain job fails whenever a newer Lean release exists (example run). It detects the release and rewrites .github/workflows/functional_tests.yml correctly, then dies on the push:

! [remote rejected] auto-update/functional-test-toolchain
  (refusing to allow a GitHub App to create or update workflow
   `.github/workflows/functional_tests.yml` without `workflows` permission)

GitHub blocks any token from committing to files under .github/workflows/ unless it carries the workflow scope. The default GITHUB_TOKEN cannot have it — workflows: write is not a grantable key in a workflow's permissions: block — so no permissions change can fix this.

This PR removes the need for such a token by moving the pinned toolchain out of the workflow file:

  • .github/functional_test_toolchain (new) holds leanprover/lean4:v4.32.2, mirroring the format of Lean's own lean-toolchain files.
  • functional_tests.yml gains a resolve-toolchain job that reads that file — or the workflow_dispatch input when one is given — and exposes the result as a job output. The toolchain-consuming jobs take needs: resolve-toolchain and reference ${{ needs.resolve-toolchain.outputs.toolchain }}. The two legacy-leanchecker jobs are unchanged, since nothing auto-edits legacy_toolchain.
  • The updater reads and writes the new file, so it no longer touches .github/workflows/ and the default GITHUB_TOKEN suffices.
  • The new file is added to the paths: filter so a toolchain bump still triggers the functional tests.

Notes

  • The workflow_dispatch input default is now "" rather than a prefilled version; leaving it blank uses the pinned toolchain. The screenshot in CONTRIBUTING.md is slightly stale in that respect.
  • This fixes the push failure only. PRs opened with GITHUB_TOKEN still do not trigger pull_request workflows, so functional tests will not run automatically on the generated PR. Setting TOOLCHAIN_UPDATE_TOKEN — now needing only contents and pull-requests, not workflow — or closing and reopening the PR remains the workaround. That caveat is still documented in the updater's header comment.

🤖 Generated with Claude Code

The nightly `Update Functional Test Toolchain` job fails when a new Lean
release exists, because it edits `.github/workflows/functional_tests.yml`
and GitHub refuses to push changes to files under `.github/workflows/`
without a token holding the `workflows` permission, which the default
`GITHUB_TOKEN` cannot be granted.

Move the pinned toolchain into `.github/functional_test_toolchain`, read
it from a `resolve-toolchain` job that exposes it as a job output, and
point the updater at that file so it no longer writes to a workflow file.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@austinletson
austinletson merged commit 8dd5d09 into main Aug 2, 2026
24 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant