From 42940df1868186335fc3d2d476bb1d364204a59c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 6 Jan 2026 14:46:14 +1100 Subject: [PATCH] feat: add parallel reusable workflow for faster CI MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a new reusable workflow (.github/workflows/ci.yml) that runs test, lint, lean4checker, and reservoir checks in parallel on separate runners after the build job completes. - Build job: elan setup, config, mathlib cache, lake build - Parallel jobs: test, lint, lean4checker, reservoir - Each parallel job restores the build cache - Same inputs/outputs as the existing composite action - Existing action.yml preserved for backward compatibility 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 --- .github/workflows/ci.yml | 314 +++++++++++++++++++++++++++++++++++++++ README.md | 29 ++++ 2 files changed, 343 insertions(+) create mode 100644 .github/workflows/ci.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..e40f1a4 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,314 @@ +name: "Lean CI (Parallel)" + +on: + workflow_call: + inputs: + auto-config: + description: | + Automatically configure based on Lake workspace. + Allowed values: "true" or "false". + type: string + required: false + default: "true" + build: + description: | + Run `lake build`. + Allowed values: "true" | "false" | "default". + type: string + required: false + default: "default" + test: + description: | + Run `lake test`. + Allowed values: "true" | "false" | "default". + type: string + required: false + default: "default" + lint: + description: | + Run `lake lint`. + Allowed values: "true" | "false" | "default". + type: string + required: false + default: "default" + mk_all-check: + description: | + Check all files are imported with `lake exe mk_all --check`. + Allowed values: "true" | "false". + type: string + required: false + default: "false" + build-args: + description: | + Build arguments to pass to `lake build {build-args}`. + type: string + required: false + default: "" + test-args: + description: | + Test arguments to pass to `lake test {test-args}`. + type: string + required: false + default: "" + use-mathlib-cache: + description: | + Override automatic Mathlib detection. + Allowed values: "true" | "false" | "auto". + type: string + required: false + default: "auto" + use-github-cache: + description: | + Enable GitHub caching. + Allowed values: "true" or "false". + type: string + required: false + default: "true" + lake-package-directory: + description: | + Directory containing the Lake package. + type: string + required: false + default: "." + reinstall-transient-toolchain: + description: | + Uninstall lean-pr-release toolchains before running. + Allowed values: "true" | "false". + type: string + required: false + default: "false" + check-reservoir-eligibility: + description: | + Check if repository is eligible for Reservoir. + Allowed values: "true" | "false". + type: string + required: false + default: "false" + lean4checker: + description: | + Check environment with lean4checker. + Allowed values: "true" | "false". + type: string + required: false + default: "false" + outputs: + build-status: + description: "Status of lake build: SUCCESS | FAILURE | ''" + value: ${{ jobs.build.outputs.build-status }} + test-status: + description: "Status of lake test: SUCCESS | FAILURE | ''" + value: ${{ jobs.test.outputs.test-status }} + lint-status: + description: "Status of lake lint: SUCCESS | FAILURE | ''" + value: ${{ jobs.lint.outputs.lint-status }} + mk_all-status: + description: "Status of mk_all --check: SUCCESS | FAILURE | ''" + value: ${{ jobs.build.outputs.mk_all-status }} + detected-mathlib: + description: "Whether Mathlib dependency was detected" + value: ${{ jobs.build.outputs.detected-mathlib }} + +jobs: + build: + runs-on: ubuntu-latest + outputs: + run-lake-test: ${{ steps.config.outputs.run-lake-test }} + run-lake-lint: ${{ steps.config.outputs.run-lake-lint }} + build-status: ${{ steps.build.outputs.build-status }} + mk_all-status: ${{ steps.mk_all.outputs.mk_all-status }} + detected-mathlib: ${{ steps.detect-mathlib.outputs.detected-mathlib }} + steps: + - uses: actions/checkout@v5 + + - name: install elan + run: | + : Install Elan + "${GITHUB_WORKSPACE}/scripts/install_elan.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - name: configure + id: config + env: + AUTO_CONFIG: ${{ inputs.auto-config }} + BUILD: ${{ inputs.build }} + TEST: ${{ inputs.test }} + LINT: ${{ inputs.lint }} + run: | + : Configure Lean Action + "${GITHUB_WORKSPACE}/scripts/config.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - name: reinstall transient toolchain + if: inputs.reinstall-transient-toolchain == 'true' + run: | + : Reinstall Transient Toolchains + if [[ "$(cat lean-toolchain)" =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then + printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)" + elan toolchain uninstall "$(cat lean-toolchain)" + fi + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - name: ensure all files are imported + id: mk_all + if: inputs.mk_all-check == 'true' + run: | + : Ensure all files are imported + "${GITHUB_WORKSPACE}/scripts/mk_all_check.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - uses: actions/cache/restore@v4 + if: inputs.use-github-cache == 'true' + with: + path: ${{ inputs.lake-package-directory }}/.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }} + + - name: detect mathlib + if: inputs.use-mathlib-cache == 'auto' + id: detect-mathlib + run: | + : Detect Mathlib + "${GITHUB_WORKSPACE}/scripts/detect_mathlib.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - name: get mathlib cache + if: steps.detect-mathlib.outputs.detected-mathlib == 'true' || inputs.use-mathlib-cache == 'true' + run: | + : Get Mathlib Cache + echo "::group::Mathlib Cache" + lake exe cache get + echo "::endgroup::" + echo + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - name: build + id: build + if: steps.config.outputs.run-lake-build == 'true' + env: + BUILD_ARGS: ${{ inputs.build-args }} + run: | + : Lake Build + "${GITHUB_WORKSPACE}/scripts/lake_build.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - uses: actions/cache/save@v4 + if: inputs.use-github-cache == 'true' + with: + path: ${{ inputs.lake-package-directory }}/.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }} + + test: + needs: build + if: needs.build.outputs.run-lake-test == 'true' + runs-on: ubuntu-latest + outputs: + test-status: ${{ steps.test.outputs.test-status }} + steps: + - uses: actions/checkout@v5 + + - name: install elan + run: | + : Install Elan + "${GITHUB_WORKSPACE}/scripts/install_elan.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - uses: actions/cache/restore@v4 + if: inputs.use-github-cache == 'true' + with: + path: ${{ inputs.lake-package-directory }}/.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }} + + - name: test + id: test + env: + TEST_ARGS: ${{ inputs.test-args }} + run: | + : Lake Test + "${GITHUB_WORKSPACE}/scripts/lake_test.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + lint: + needs: build + if: needs.build.outputs.run-lake-lint == 'true' + runs-on: ubuntu-latest + outputs: + lint-status: ${{ steps.lint.outputs.lint-status }} + steps: + - uses: actions/checkout@v5 + + - name: install elan + run: | + : Install Elan + "${GITHUB_WORKSPACE}/scripts/install_elan.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - uses: actions/cache/restore@v4 + if: inputs.use-github-cache == 'true' + with: + path: ${{ inputs.lake-package-directory }}/.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }} + + - name: lint + id: lint + run: | + : Lake Lint + "${GITHUB_WORKSPACE}/scripts/lake_lint.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + lean4checker: + needs: build + if: inputs.lean4checker == 'true' + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v5 + + - name: install elan + run: | + : Install Elan + "${GITHUB_WORKSPACE}/scripts/install_elan.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + - uses: actions/cache/restore@v4 + if: inputs.use-github-cache == 'true' + with: + path: ${{ inputs.lake-package-directory }}/.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles(format('{0}/lean-toolchain', inputs.lake-package-directory)) }}-${{ hashFiles(format('{0}/lake-manifest.json', inputs.lake-package-directory)) }} + + - name: lean4checker + run: | + : Check Environment with lean4checker + "${GITHUB_WORKSPACE}/scripts/run_lean4checker.sh" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} + + reservoir: + needs: build + if: inputs.check-reservoir-eligibility == 'true' + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v5 + + - name: check reservoir eligibility + run: | + : Check Reservoir Eligibility + "${GITHUB_WORKSPACE}/scripts/check_reservoir_eligibility.sh" \ + "${{ github.event.repository.private }}" \ + "${{ github.event.repository.stargazers_count }}" \ + "${{ github.event.repository.license.spdx_id }}" + shell: bash + working-directory: ${{ inputs.lake-package-directory }} diff --git a/README.md b/README.md index 3fb88de..e2e4eab 100644 --- a/README.md +++ b/README.md @@ -137,6 +137,35 @@ because `lean-action` may not detect the `test_driver` in the Lake workspace. To be certain `lean-action` runs a step, specify the desire feature with a feature input. +## Parallel Workflow + +For faster CI, `lean-action` provides a reusable workflow that runs test, lint, lean4checker, and reservoir checks in parallel on separate runners: + +```yaml +name: CI + +on: + push: + branches: ["main"] + pull_request: + branches: ["main"] + +jobs: + ci: + uses: leanprover/lean-action/.github/workflows/ci.yml@v1 + with: + test: "true" + lint: "true" + lean4checker: "true" +``` + +The parallel workflow: +- Runs a **build** job first (elan setup, config, mathlib cache, lake build) +- Then runs **test**, **lint**, **lean4checker**, and **reservoir** jobs in parallel +- Each parallel job restores the build cache from the build job + +All inputs from the standard action are supported. The workflow outputs the same status parameters (`build-status`, `test-status`, `lint-status`, `mk_all-status`). + ## Customization `lean-action` provides optional configuration inputs to customize the behavior for your specific workflow.