Skip to content

[Merged by Bors] - feat: BoundedMul class to generalize multiplication of bounded continuous functions. #53610

[Merged by Bors] - feat: BoundedMul class to generalize multiplication of bounded continuous functions.

[Merged by Bors] - feat: BoundedMul class to generalize multiplication of bounded continuous functions. #53610

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@v4
- name: "Checkout mathlib3"
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib
path: port-repos/leanprover-community/mathlib
- name: "Checkout lean3"
uses: actions/checkout@v4
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}")"
printf 'MY_MERGE_BASE_SHA=%s\n' "${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"