diff --git a/.github/workflows/BuildArtifact.yml b/.github/workflows/BuildArtifact.yml new file mode 100644 index 000000000..8d9b54383 --- /dev/null +++ b/.github/workflows/BuildArtifact.yml @@ -0,0 +1,53 @@ + +on: + push: + branches: + - master + pull_request: + branches: + - master + +name: Style linters + +jobs: + doc_lint: + name: Lean based style linters + runs-on: ubuntu-latest + steps: + + - uses: actions/checkout@v4 + + - name: Install elan + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y + ~/.elan/bin/lean --version + echo "$HOME/.elan/bin" >> $GITHUB_PATH + + - name: check versions + run: | + lean --version + lake --version + elan --version + + - name: build cache + run: | + lake exe cache get + + - name: build PhysLean + id: build + uses: liskin/gh-problem-matcher-wrap@v3 + with: + linters: gcc + run: | + bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log" + - name: copy build data + run: | + mv .lake lake-artifact/.lake + + - name: Upload build artifact + uses: actions/upload-artifact@v4 + with: + name: lake + path: lake-artifact/ + retention-days: 90 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index b3e044c2e..f229b3e19 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -28,6 +28,7 @@ jobs: run: | lean --version lake --version + elan --version - name: build cache run: | @@ -41,6 +42,10 @@ jobs: run: | bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log" + - name: runLinter on PhysLean + run: | + env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean + - name: check file imports run: | bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports" @@ -53,13 +58,6 @@ jobs: run: | bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe sorry_lint" - - name: runLinter on PhysLean - if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }} - id: lint - uses: liskin/gh-problem-matcher-wrap@v3 - with: - linters: gcc - run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter PhysLean style_lint: name: Python based style linter