feat: Polynomial.map f strictly decreases the degree if f p.leadingCoeff = 0
#33026
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Post PR summary comment | |
| on: | |
| pull_request: | |
| jobs: | |
| build: | |
| name: "post-or-update-summary-comment" | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Set up Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: 3.12 | |
| - name: Install dependencies | |
| run: | | |
| python -m pip install --upgrade pip | |
| sudo apt-get install -y jq | |
| # If you have additional dependencies, install them here | |
| - name: Get changed files | |
| run: | | |
| git fetch origin ${{ github.base_ref }} # fetch the base branch | |
| git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt # get the list of changed files | |
| - name: Compute transitive imports | |
| run: | | |
| # the checkout dance, to avoid a detached head | |
| git checkout master | |
| git checkout - | |
| currentHash="$(git rev-parse HEAD)" | |
| # Compute the counts for the HEAD of the PR | |
| python ./scripts/count-trans-deps.py "Mathlib/" > head.json | |
| # Checkout the merge base | |
| git checkout "$(git merge-base master ${{ github.sha }})" | |
| # Compute the counts for the merge base | |
| python ./scripts/count-trans-deps.py "Mathlib/" > base.json | |
| # switch back to the current branch: the `declarations_diff` script should be here | |
| git checkout "${currentHash}" | |
| - name: Post or update the summary comment | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| BRANCH_NAME: ${{ github.head_ref }} | |
| run: | | |
| PR="${{ github.event.pull_request.number }}" | |
| title="### PR summary" | |
| graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt) | |
| ## Import count comment | |
| importCount=$( | |
| printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q' | |
| ./scripts/import_trans_difference.sh | |
| ) | |
| ## High percentage imports | |
| high_percentages=$( | |
| printf '%s\n' "${graphAndHighPercentReports}" | sed -n '/^Import changes exceeding/,$p' | |
| ) | |
| # if there are files with large increase in transitive imports, then we add the `large-import` label | |
| if [ -n "${high_percentages}" ] | |
| then | |
| high_percentages=$'\n\n'"${high_percentages}" | |
| gh pr edit "${PR}" --add-label large-import | |
| else # otherwise, we remove the label | |
| gh pr edit "${PR}" --remove-label large-import | |
| fi | |
| if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ] | |
| then | |
| importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")" | |
| else | |
| importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")" | |
| fi | |
| ## Declarations' diff comment | |
| declDiff=$(./scripts/declarations_diff.sh) | |
| if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ] | |
| then | |
| declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")" | |
| else | |
| declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")" | |
| fi | |
| git checkout "${BRANCH_NAME}" | |
| currentHash="$(git rev-parse HEAD)" | |
| hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}" | |
| ## Technical debt changes | |
| techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)" | |
| message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}")" | |
| ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}" |