Skip to content

[Merged by Bors] - feat: isUnit_iff_eq_one #37124

[Merged by Bors] - feat: isUnit_iff_eq_one

[Merged by Bors] - feat: isUnit_iff_eq_one #37124

name: Detect changes to header SHAs
on:
pull_request:
jobs:
build:
name: Add annotations
runs-on: ubuntu-latest
env:
GH_TOKEN: ${{ github.token }}
steps:
- name: "Checkout mathlib4"
uses: actions/checkout@v3
- name: "Checkout mathlib3"
uses: actions/checkout@v3
with:
repository: leanprover-community/mathlib
path: port-repos/leanprover-community/mathlib
- name: "Checkout lean3"
uses: actions/checkout@v3
with:
repository: leanprover-community/lean
path: port-repos/leanprover-community/lean
- name: Fetch merge base SHA from API
run: |
my_merge_base_cmd="gh api repos/${{ github.repository }}/compare/${{ github.event.pull_request.base.sha }}...${{ github.event.pull_request.head.sha }} | jq -r '.merge_base_commit.sha'"
echo $my_merge_base_cmd
my_merge_base=$(eval $my_merge_base_cmd)
echo "MY_MERGE_BASE_SHA=$my_merge_base" >> $GITHUB_ENV
- name: Fetch merge base SHA
run: |
git fetch \
--no-tags \
--prune \
--progress \
--no-recurse-submodules \
--depth=1 \
origin $MY_MERGE_BASE_SHA
- name: install Python
uses: actions/setup-python@v4
with:
python-version: 3.8
- name: install script dependencies
run: |
pip install gitpython
- name: run the script
run: |
python scripts/detect_sha_changes.py "$MY_MERGE_BASE_SHA" "HEAD"