Add VersoXp, use lakefile.toml and reservoir require for the first time #233
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Lean 4 CI | |
| on: | |
| # Triggers the workflow on push or pull request events but only for the "main" branch and "v4*" branches | |
| push: | |
| branches: | |
| - main | |
| - 'v4*' | |
| paths: | |
| - '.github/workflows/lean4.yml' | |
| - 'lean4*/**' | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| jobs: | |
| # This workflow contains a single job called "lean4" | |
| lean4: | |
| name: Lean 4 Projects | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest, windows-latest] | |
| fail-fast: false | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - uses: extractions/setup-just@v2 | |
| with: | |
| just-version: 1.35.0 | |
| # - name: install elan on Ubuntu and macOS | |
| # if: matrix.os != 'windows-latest' | |
| # run: | | |
| # set -o pipefail | |
| # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y | |
| # echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| # - name: install elan on Windows | |
| # if: matrix.os == 'windows-latest' | |
| # run: | | |
| # curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | |
| # .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain none | |
| # echo "$HOME\.elan\bin" >> $env:GITHUB_PATH | |
| - uses: dorny/paths-filter@v2 | |
| id: filter | |
| with: | |
| list-files: shell | |
| filters: | | |
| shared: | |
| - added|modified: '.github/workflows/lean4.yml' | |
| - added|modified: 'lean4-xp-kit/**/*' | |
| lean4: | |
| - added|modified: 'lean4/**/*' | |
| duper: | |
| - added|modified: 'lean4-duper-xp/**/*' | |
| verso: | |
| - added|modified: 'lean4-verso-xp/**/*' | |
| - name: Should annotate | |
| id: annotate | |
| # annotation is enabled conditionally | |
| if: >- | |
| matrix.os == 'ubuntu-latest' && ( | |
| startsWith(github.ref, 'refs/heads/v4') || | |
| contains(github.event.head_commit.message, '[annotate]') | |
| ) | |
| run: echo "annotate=true" >> "$GITHUB_OUTPUT" | |
| - name: Cache github-pages | |
| if: >- | |
| steps.annotate.outputs.annotate == 'true' | |
| uses: actions/cache@v4 | |
| with: | |
| path: github-pages | |
| key: github-pages-${{ github.run_id }} | |
| restore-keys: | | |
| github-pages | |
| - name: check Lean 4 Playground | |
| if: >- | |
| steps.filter.outputs.shared == 'true' || | |
| steps.filter.outputs.lean4 == 'true' || | |
| steps.annotate.outputs.annotate == 'true' | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: "lean4" | |
| - name: check DuperXp | |
| if: >- | |
| steps.filter.outputs.shared == 'true' || | |
| steps.filter.outputs.duper == 'true' || | |
| steps.annotate.outputs.annotate == 'true' | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: "lean4-duper-xp" | |
| - name: check VersoXp | |
| if: >- | |
| steps.filter.outputs.shared == 'true' || | |
| steps.filter.outputs.verso == 'true' || | |
| steps.annotate.outputs.annotate == 'true' | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: "lean4-verso-xp" | |
| - name: Install Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.11" | |
| # cache: 'pip' # caching pip dependencies | |
| - name: annotate Lean 4 projects | |
| if: >- | |
| steps.annotate.outputs.annotate == 'true' | |
| run: | | |
| pushd lean4 | |
| just annotate Playground | |
| popd | |
| pushd lean4-duper-xp | |
| just annotate DuperXp | |
| popd | |
| just pages lean4 | |
| just pages lean4-duper-xp | |
| # - name: Try mk_all | |
| # shell: bash | |
| # run: | | |
| # cd lean4 | |
| # rm -f .lake/packages/mathlib/lakefile.lean | |
| # mv lakefile-for-mathlib.lean .lake/packages/mathlib/lakefile.lean | |
| # lake -R exe mk_all || true | |
| - name: Try check NoCI examples | |
| shell: bash | |
| run: | | |
| cd lean4 | |
| ./check_noci.sh || true | |