push_pr.yml

on:
  pull_request:

jobs:
  build_project:
    runs-on: ubuntu-latest
    name: Build project
    concurrency:
      group: ${{ github.workflow }}-${{ github.ref }}
      cancel-in-progress: true
    steps:
      - name: checkout project
        uses: actions/checkout@v2
        with:
          fetch-depth: 0

      - name: check case sensitivity
        uses: credfeto/action-case-checker@v1.3.0

      - name: look for ignored files
        uses: credfeto/action-no-ignored-files@v1.1.0

      - name: check for lean files with the executable bit set
        shell: bash
        run: |
          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
          if [[ -n "$executable_files" ]]
          then
            echo "ERROR: The following Lean files have the executable bit set."
            echo "$executable_files"
            exit 1
          fi

      - name: install elan
        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:nightly-2023-08-15

      - name: get cache
        run: ~/.elan/bin/lake exe cache get

      - name: check ConNF.lean
        run: ~/.elan/bin/lake -Kenv=dev exe mk_all --lib ConNF --check

      - name: build project
        run: ~/.elan/bin/lake build ConNF