Skip to content

Commit

Permalink
fix names
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Jun 22, 2024
1 parent 3e4bd50 commit 3d78c26
Show file tree
Hide file tree
Showing 4 changed files with 68 additions and 44 deletions.
28 changes: 17 additions & 11 deletions .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -206,17 +206,6 @@ jobs:
lake build --no-build
fi
- name: Lean-diff
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
- name: build archive
id: archive
run: |
Expand Down Expand Up @@ -313,6 +302,23 @@ jobs:
run: |
scripts/lean-pr-testing-comments.sh
Lean-diff:
name: compute the diff of the declarations
if: github.repository == 'leanprover-community/mathlib4'

Check failure on line 308 in .github/workflows/bors.yml

View workflow job for this annotation

GitHub Actions / actionlint

could not parse as YAML: yaml: line 308: mapping values are not allowed in this context
needs: [build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- name: Lean-diff
run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
Expand Down
28 changes: 17 additions & 11 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -213,17 +213,6 @@ jobs:
lake build --no-build
fi
- name: Lean-diff
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
- name: build archive
id: archive
run: |
Expand Down Expand Up @@ -320,6 +309,23 @@ jobs:
run: |
scripts/lean-pr-testing-comments.sh
Lean-diff:
name: compute the diff of the declarations
if: github.repository == 'leanprover-community/mathlib4'

Check failure on line 315 in .github/workflows/build.yml

View workflow job for this annotation

GitHub Actions / actionlint

could not parse as YAML: yaml: line 315: mapping values are not allowed in this context
needs: [build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- name: Lean-diff
run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
final:
name: Post-CI job
if: github.repository == 'leanprover-community/mathlib4'
Expand Down
28 changes: 17 additions & 11 deletions .github/workflows/build.yml.in
Original file line number Diff line number Diff line change
Expand Up @@ -192,17 +192,6 @@ jobs:
lake build --no-build
fi

- name: Lean-diff
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"

- name: build archive
id: archive
run: |
Expand Down Expand Up @@ -299,6 +288,23 @@ jobs:
run: |
scripts/lean-pr-testing-comments.sh


Lean-diff:
name: compute the diff of the declarations
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
needs: [build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- name: Lean-diff
run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"

final:
name: Post-CI jobJOB_NAME
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
Expand Down
28 changes: 17 additions & 11 deletions .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -210,17 +210,6 @@ jobs:
lake build --no-build
fi
- name: Lean-diff
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
- name: build archive
id: archive
run: |
Expand Down Expand Up @@ -317,6 +306,23 @@ jobs:
run: |
scripts/lean-pr-testing-comments.sh
Lean-diff:
name: compute the diff of the declarations
if: github.repository != 'leanprover-community/mathlib4'

Check failure on line 312 in .github/workflows/build_fork.yml

View workflow job for this annotation

GitHub Actions / actionlint

could not parse as YAML: yaml: line 312: mapping values are not allowed in this context
needs: [build]
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
## fetch the whole repository, useful to find a common fork
fetch-depth: 0
- name: Lean-diff
run: |
git checkout master
git checkout -
./scripts/list_decls.lean "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"
final:
name: Post-CI job (fork)
if: github.repository != 'leanprover-community/mathlib4'
Expand Down

0 comments on commit 3d78c26

Please sign in to comment.