lean4.yml

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@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"
      - 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"
          # 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-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

          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