Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 53 additions & 0 deletions .github/workflows/BuildArtifact.yml
Original file line number Diff line number Diff line change
@@ -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
12 changes: 5 additions & 7 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
run: |
lean --version
lake --version
elan --version

- name: build cache
run: |
Expand All @@ -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"
Expand All @@ -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
Expand Down
Loading