[Merged by Bors] - CI: merge `bot_fix_style` actions by adomani · Pull Request #20789 · leanprover-community/mathlib4

adomani · 2025-01-16T08:40:33Z

This PR continues the series of merging CI actions that are triggered by comments, reviews and review_comments.

Specifically, we merge here the 3 bot fix style actions into a single one.

#20791 tests that the new action works as intended.

github-actions · 2025-01-16T08:41:30Z

messageFile.md

…ixes

github-actions · 2025-01-16T08:44:09Z

messageFile.md

github-actions · 2025-01-16T08:46:23Z

PR summary 2a0f773d55

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

jcommelin · 2025-01-16T09:52:23Z

.github/workflows/bot_fix_style.yaml

+          COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}"
+          # we strip `\r` since line endings from GitHub contain this character
+          COMMENT="${COMMENT//$'\r'/}"
+          # for debugging, we print some information
+          printf '%s' "${COMMENT}" | hexdump -cC
+          printf 'Comment:"%s"\n' "${COMMENT}"
+          bot_fix_style="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bot fix style$=bot-fix-style=p' | head -1)"
+
+          printf $'"bot fix style"? \'%s\'\n' "${bot_fix_style}"
+          printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
+          printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
+          printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
+
+          printf $'bot_fix_style=%s\n' "${bot_fix_style}" >> "${GITHUB_OUTPUT}"
+          # these final variables are probably not relevant for the bot_fix_style action
+          if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
+             [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
+          then
+            printf $'bot=true\n'
+            printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
+          else
+            printf $'bot=false\n'
+            printf $'bot=false\n' >> "${GITHUB_OUTPUT}"
+          fi


For me and other reviewers: this is a bit of new logic. The rest of the file is almost verbatim taken from the other 3 files, with minor changes.

It is also the same logic that is used by the maintainer_bors/merge workflows: I copied it, with little effort of removing parts that were not necessary for this PR, since I have a view of unifying all actions that are triggered by comments.

jcommelin · 2025-01-16T09:52:35Z

.github/workflows/bot_fix_style.yaml

+          # we strip `\r` since line endings from GitHub contain this character
+          COMMENT="${COMMENT//$'\r'/}"
+          # for debugging, we print some information
+          printf '%s' "${COMMENT}" | hexdump -cC


What is the purpose of the hexdump?

I had it for debugging: the previous line strips \r and I only noticed that those were there thanks to hexdump.

(In case it is useful, hexdump produces an output where every character is visible, even the non-printing ones and that is its main use here.)

jcommelin · 2025-01-16T09:55:20Z

.github/workflows/bot_fix_style.yaml

+          bot_fix_style="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bot fix style$=bot-fix-style=p' | head -1)"
+
+          printf $'"bot fix style"? \'%s\'\n' "${bot_fix_style}"


What exactly does this do?
Do I understand correctly that it checks whether the comment contains a line that exactly matches "bot fix style", with nothing before or after it?
If so, that seems good. Because we don't want to run the rest of the workflow if a comment only contains "bot fix style" somewhere in the middle of a line. After all, such a comment is probably a reviewer explaining the functionality to a contributor.

The sed line checks that the comment contains a line that consists only and exactly of bot fix style. If it finds it, then it returns bot_fix_style exactly once, even if the comment contains it several times (that is ensured by the head pipe).

jcommelin · 2025-01-16T11:31:06Z

Thanks 🎉

bors merge

This PR continues the series of merging CI actions that are triggered by `comment`s, `review`s and `review_comment`s. Specifically, we merge here the 3 `bot fix style` actions into a single one. #20791 tests that the new action works as intended.

mathlib-bors · 2025-01-16T12:00:07Z

Build failed (retrying...):

Build

This PR continues the series of merging CI actions that are triggered by `comment`s, `review`s and `review_comment`s. Specifically, we merge here the 3 `bot fix style` actions into a single one. #20791 tests that the new action works as intended.

mathlib-bors · 2025-01-16T12:10:48Z

Pull request successfully merged into master.

Build succeeded:

* polynomial-sequences: (149 commits) Aha, here's how to get Lean to stop showing S.elems' in the infoview. Try satisfying the linter gods again. Probably enough initial tidying to send the PR. Kill more temporary names. Touch more natDegree. Does protected satisfy the docstring linter? Bit shorter. More Quiet linters. Remove redundant imports. Copyright header and more twiddling. Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out feat(Polynomial): polynomial sequences are bases for R[X] chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765) chore(Associated): split out `Ring` results (#20737) feat(AlgebraicGeometry): flat morphisms of schemes (#19790) feat(AlgebraicGeometry): scheme-theoretic fibre (#19427) chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785) doc: typo (#20829) feat(CategoryTheory): condition for an induced functor between comma categories to be final (#20139) feat(1000.yaml): allow statements of theorems also (#20637) feat(Algebra/Homology/Embedding): homology of truncGE' (#19570) chore: cleanup many porting notes in Combinatorics (#20823) chore: eliminate porting notes about `deriving Fintype` (#20820) feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808) feat: define bases of root pairings (#20667) feat(Tactic): basic ConcreteCategory support for elementwise (#20811) feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783) chore(yaml_check.py): re-format (#20807) feat: elementary estimate for Real.log (#20766) feat: definition of linear topologies (#14990) feat(RingTheory): flatness over a semiring (#19115) feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550) feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203) feat(Algebra/Ring): `RingEquiv.piUnique` (#20794) feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801) chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) chore: restore `def` to `adicCompletion` (#20796) refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) chore(Mathlib/Computability/TuringMachine): split file (#20790) feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753) feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752) feat(Set/Finite): a set is finite if its image and fibers are finite (#20751) chore: cleanup .gitignore files (#20795) feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) CI: merge `bot_fix_style` actions (#20789) ...

adomani added 2 commits January 16, 2025 08:36

add merged file

390deb2

remove old bot_fix_style workflow files

a022eb6

adomani requested review from bryangingechen and jcommelin January 16, 2025 08:40

comment indentation

2dcd84e

github-actions bot added the CI Modifies the continuous integration setup or other automation label Jan 16, 2025

adomani added 2 commits January 16, 2025 08:42

Merge remote-tracking branch 'origin/master' into adomani/merge_bot_f…

da6235e

…ixes

indent later

b77a3b7

adomani added 7 commits January 16, 2025 08:51

de-indent

e7b074b

re-indent

28aedeb

more indent

d36c297

remove line break

48c2776

more attempts

a12fb6a

comment elsewhere

be63871

remove references to old action files

dda9d8e

adomani mentioned this pull request Jan 16, 2025

test: merge bot fixes #20791

Closed

jcommelin reviewed Jan 16, 2025

View reviewed changes

fix to work with review comments

2a0f773

adomani marked this pull request as ready for review January 16, 2025 11:20

ghost added the ready-to-merge This PR has been sent to bors. label Jan 16, 2025

mathlib-bors bot changed the title ~~CI: merge bot_fix_style actions~~ [Merged by Bors] - CI: merge bot_fix_style actions Jan 16, 2025

mathlib-bors bot closed this Jan 16, 2025

mathlib-bors bot deleted the adomani/merge_bot_fixes branch January 16, 2025 12:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - CI: merge `bot_fix_style` actions#20789

[Merged by Bors] - CI: merge `bot_fix_style` actions#20789
adomani wants to merge 13 commits intomasterfrom
adomani/merge_bot_fixes

adomani commented Jan 16, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 16, 2025

Uh oh!

github-actions bot commented Jan 16, 2025

Uh oh!

github-actions bot commented Jan 16, 2025 •

edited

Loading

Uh oh!

jcommelin Jan 16, 2025

Uh oh!

adomani Jan 16, 2025

Uh oh!

jcommelin Jan 16, 2025

Uh oh!

adomani Jan 16, 2025

Uh oh!

jcommelin Jan 16, 2025

Uh oh!

adomani Jan 16, 2025

Uh oh!

jcommelin commented Jan 16, 2025

Uh oh!

mathlib-bors bot commented Jan 16, 2025

Uh oh!

mathlib-bors bot commented Jan 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

adomani commented Jan 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 16, 2025

Uh oh!

github-actions bot commented Jan 16, 2025

Uh oh!

github-actions bot commented Jan 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2a0f773d55

Import changes for modified files

Declarations diff

Uh oh!

jcommelin Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

adomani Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

jcommelin Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

adomani Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

jcommelin Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

adomani Jan 16, 2025

Choose a reason for hiding this comment

Uh oh!

jcommelin commented Jan 16, 2025

Uh oh!

mathlib-bors bot commented Jan 16, 2025

Uh oh!

mathlib-bors bot commented Jan 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

adomani commented Jan 16, 2025 •

edited

Loading

github-actions bot commented Jan 16, 2025 •

edited

Loading