Skip to content

Commit

Permalink
separate action
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Jun 22, 2024
1 parent b3198ac commit 78d5753
Showing 1 changed file with 20 additions and 0 deletions.
20 changes: 20 additions & 0 deletions .github/workflows/Lean_decl_diff.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
on:

Check failure on line 1 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

"jobs" section is missing in workflow
workflow_run:
workflows: ["Build"]
types:
- completed

Lean_decl_diff:

Check failure on line 7 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

unknown Webhook event "Lean_decl_diff". see https://docs.github.com/en/actions/learn-github-actions/events-that-trigger-workflows#webhook-events for list of all Webhook event names
if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'

Check failure on line 8 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

unexpected key "if" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"
name: summarize_declarations

Check failure on line 9 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

unexpected key "name" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"
runs-on: ubuntu-latest

Check failure on line 10 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

unexpected key "runs-on" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"
steps:

Check failure on line 11 in .github/workflows/Lean_decl_diff.yaml

View workflow job for this annotation

GitHub Actions / actionlint

unexpected key "steps" for "Lean_decl_diff" section. expected one of "branches", "branches-ignore", "paths", "paths-ignore", "tags", "tags-ignore", "types", "workflows"
- 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/decls_diff_hybrid.sh "${{ github.sha }}" "$(git merge-base master ${{ github.sha }})"

0 comments on commit 78d5753

Please sign in to comment.