Skip to content

Conversation

bryangingechen
Copy link
Contributor

This fixes an embarrassing mistake in #30095: the script currently compares lake-manifest.json in the update-dependencies-bot-use-only branch to itself rather than to the changes made in the working directory. This has caused the update workflow to fail to push changes for about a week or so.


Open in Gitpod

@bryangingechen bryangingechen added the CI Modifies the continuous integration setup or other automation label Oct 9, 2025
@bryangingechen bryangingechen requested a review from adomani October 9, 2025 17:25
Copy link

github-actions bot commented Oct 9, 2025

PR summary 724a6cb9d7

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).

@bryangingechen bryangingechen changed the title fix(update_dependencies.yml): compare file in working directory rather than at HEAD ci(update_dependencies.yml): use lake-manifest.json in working directory rather than HEAD Oct 9, 2025
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors r+

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Oct 10, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 10, 2025
…ory rather than HEAD (#30381)

This fixes an embarrassing mistake in #30095: the script currently compares `lake-manifest.json` in the `update-dependencies-bot-use-only` branch to itself rather than to the changes made in the working directory. This has caused the update workflow to fail to push changes for about a week or so.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title ci(update_dependencies.yml): use lake-manifest.json in working directory rather than HEAD [Merged by Bors] - ci(update_dependencies.yml): use lake-manifest.json in working directory rather than HEAD Oct 10, 2025
@mathlib-bors mathlib-bors bot closed this Oct 10, 2025
@mathlib-bors mathlib-bors bot deleted the bryangingechen-patch-1 branch October 10, 2025 13:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants