Try add Verso doc to pages; add mechanism to trigger all CI [annotate] #245
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*/**' | |
| - '.allci' | |
| # 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@v3 | |
| 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/**/*' | |
| sci: | |
| - added|modified: 'lean4-sci-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" | |
| use-github-cache: false | |
| - 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" | |
| use-github-cache: false | |
| - 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" | |
| use-github-cache: false | |
| # use-mathlib-cache: true | |
| - name: check SciXp | |
| if: >- | |
| runner.os == 'macos-latest' && ( | |
| steps.filter.outputs.shared == 'true' || | |
| steps.filter.outputs.sci == 'true' || | |
| steps.annotate.outputs.annotate == 'true' | |
| ) | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: "lean4-sci-xp" | |
| use-github-cache: false | |
| use-mathlib-cache: true | |
| - 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 | |
| pushd lean4-verso-xp | |
| just doc | |
| popd | |
| just pages lean4 | |
| just pages lean4-duper-xp | |
| just pages lean4-verso-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 | |