[Merged by Bors] - chore(deps): bump leanprover/lean-action from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec in /.github/workflows by dependabot[bot] · Pull Request #24510 · leanprover-community/mathlib4

dependabot · 2025-05-01T13:25:43Z

Bumps leanprover/lean-action from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec.

Changelog

Sourced from leanprover/lean-action's changelog.

Changelog

All notable changes to lean-action will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Unreleased

Added

add option to always reinstall lean4-pr-releases toolchains, ensuring CI runs with the latest version

v1.1.2 - 2025-03-28

Fixed

include runner architecture in cache key to avoid reusing .lake across different runner architectures

v1.1.1 - 2024-11-23

Fixed

fix bug with passing multiple arguments to lake build via build-args input

fix false feature flag logic when using auto-config: true

v1.1.0 - 2024-9-16

Added

Windows GitHub runner support

Fixed

replace actions/cache with actions/cache/restore to prevent redundant cache saving previously caused by the combination of actions/cache and actions/cache/save

v1.0.2 - 2024-8-26

Changed

use empty string as default value for status outputs instead of "NOT_RUN" to avoid set-output-parameters final step breaking log group expansion

Fixed

correct typo of in configuration step: "lake check-test failed" -> "lake check-lint failed"

fix log group expansion in failing steps due to set-output-parameters step and removing the end log group command when a step fails

... (truncated)

Commits

f807b33 Clarify and fix typo in changelog (#123)
See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

@dependabot rebase will rebase this PR
@dependabot recreate will recreate this PR, overwriting any edits that have been made to it
@dependabot merge will merge this PR after your CI passes on it
@dependabot squash and merge will squash and merge this PR after your CI passes on it
@dependabot cancel merge will cancel a previously requested merge and block automerging
@dependabot reopen will reopen this PR if it is closed
@dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
@dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
@dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
@dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
@dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

Bumps [leanprover/lean-action](https://github.com/leanprover/lean-action) from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec. - [Release notes](https://github.com/leanprover/lean-action/releases) - [Changelog](https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md) - [Commits](leanprover/lean-action@e18f2df...f807b33) --- updated-dependencies: - dependency-name: leanprover/lean-action dependency-version: f807b338d95de7813c5c50d018f1c23c9b93b4ec dependency-type: direct:production ... Signed-off-by: dependabot[bot] <support@github.com>

.github/workflows/add_label_from_diff.yaml

.github/workflows/bench_summary_comment.yml

.github/workflows/bors.yml

.github/workflows/bot_fix_style.yaml

.github/workflows/lint_and_suggest_pr.yml

.github/workflows/nightly_merge_master.yml

.github/workflows/nolints.yml

.github/workflows/update_dependencies.yml

github-actions · 2025-05-01T14:25:20Z

PR summary 4cc2835e91

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 · 2025-05-01T14:25:25Z

bors r+

…3bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec in /.github/workflows (#24510) Bumps [leanprover/lean-action](https://github.com/leanprover/lean-action) from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec. <details> <summary>Changelog</summary> <p><em>Sourced from <a href="https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md">leanprover/lean-action's changelog</a>.</em></p> <blockquote> <h1>Changelog</h1> <p>All notable changes to <code>lean-action</code> will be documented in this file.</p> <p>The format is based on <a href="https://keepachangelog.com/en/1.1.0/">Keep a Changelog</a>, and this project adheres to <a href="https://semver.org/spec/v2.0.0.html">Semantic Versioning</a>.</p> <h2>Unreleased</h2> <h3>Added</h3> <ul> <li>add option to always reinstall <code>lean4-pr-releases</code> toolchains, ensuring CI runs with the latest version</li> </ul> <h2>v1.1.2 - 2025-03-28</h2> <h3>Fixed</h3> <ul> <li>include runner architecture in cache key to avoid reusing <code>.lake</code> across different runner architectures</li> </ul> <h2>v1.1.1 - 2024-11-23</h2> <h3>Fixed</h3> <ul> <li>fix bug with passing multiple arguments to <code>lake build</code> via <code>build-args</code> input</li> <li>fix false feature flag logic when using <code>auto-config: true</code></li> </ul> <h2>v1.1.0 - 2024-9-16</h2> <h3>Added</h3> <ul> <li>Windows GitHub runner support</li> </ul> <h3>Fixed</h3> <ul> <li>replace <code>actions/cache</code> with <code>actions/cache/restore</code> to prevent redundant cache saving previously caused by the combination of <code>actions/cache</code> and <code>actions/cache/save</code></li> </ul> <h2>v1.0.2 - 2024-8-26</h2> <h3>Changed</h3> <ul> <li>use empty string as default value for status outputs instead of "NOT_RUN" to avoid <code>set-output-parameters</code> final step breaking log group expansion</li> </ul> <h3>Fixed</h3> <ul> <li>correct typo of in configuration step: "lake check-test failed" -> "lake check-lint failed"</li> <li>fix log group expansion in failing steps due to <code>set-output-parameters</code> step and removing the end log group command when a step fails</li> </ul>  </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/leanprover/lean-action/commit/f807b338d95de7813c5c50d018f1c23c9b93b4ec"><code>f807b33</code></a> Clarify and fix typo in changelog (<a href="https://redirect.github.com/leanprover/lean-action/issues/123">#123</a>)</li> <li>See full diff in <a href="https://github.com/leanprover/lean-action/compare/e18f2df7f0d4f30d11a4b963bff9b1140999480c...f807b338d95de7813c5c50d018f1c23c9b93b4ec">compare view</a></li> </ul> </details> <br /> Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

mathlib-bors · 2025-05-01T14:32:56Z

Pull request successfully merged into master.

Build succeeded:

dependabot · 2025-05-01T14:32:59Z

OK, I won't notify you again about this release, but will get in touch when a new version is available. You can also ignore all major, minor, or patch releases for a dependency by adding an ignore condition with the desired update_types to your config file.

If you change your mind, just re-open this PR and I'll resolve any conflicts on it.

…3bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec in /.github/workflows (#24510) Bumps [leanprover/lean-action](https://github.com/leanprover/lean-action) from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec. <details> <summary>Changelog</summary> <p><em>Sourced from <a href="https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md">leanprover/lean-action's changelog</a>.</em></p> <blockquote> <h1>Changelog</h1> <p>All notable changes to <code>lean-action</code> will be documented in this file.</p> <p>The format is based on <a href="https://keepachangelog.com/en/1.1.0/">Keep a Changelog</a>, and this project adheres to <a href="https://semver.org/spec/v2.0.0.html">Semantic Versioning</a>.</p> <h2>Unreleased</h2> <h3>Added</h3> <ul> <li>add option to always reinstall <code>lean4-pr-releases</code> toolchains, ensuring CI runs with the latest version</li> </ul> <h2>v1.1.2 - 2025-03-28</h2> <h3>Fixed</h3> <ul> <li>include runner architecture in cache key to avoid reusing <code>.lake</code> across different runner architectures</li> </ul> <h2>v1.1.1 - 2024-11-23</h2> <h3>Fixed</h3> <ul> <li>fix bug with passing multiple arguments to <code>lake build</code> via <code>build-args</code> input</li> <li>fix false feature flag logic when using <code>auto-config: true</code></li> </ul> <h2>v1.1.0 - 2024-9-16</h2> <h3>Added</h3> <ul> <li>Windows GitHub runner support</li> </ul> <h3>Fixed</h3> <ul> <li>replace <code>actions/cache</code> with <code>actions/cache/restore</code> to prevent redundant cache saving previously caused by the combination of <code>actions/cache</code> and <code>actions/cache/save</code></li> </ul> <h2>v1.0.2 - 2024-8-26</h2> <h3>Changed</h3> <ul> <li>use empty string as default value for status outputs instead of "NOT_RUN" to avoid <code>set-output-parameters</code> final step breaking log group expansion</li> </ul> <h3>Fixed</h3> <ul> <li>correct typo of in configuration step: "lake check-test failed" -> "lake check-lint failed"</li> <li>fix log group expansion in failing steps due to <code>set-output-parameters</code> step and removing the end log group command when a step fails</li> </ul>  </blockquote> <p>... (truncated)</p> </details> <details> <summary>Commits</summary> <ul> <li><a href="https://github.com/leanprover/lean-action/commit/f807b338d95de7813c5c50d018f1c23c9b93b4ec"><code>f807b33</code></a> Clarify and fix typo in changelog (<a href="https://redirect.github.com/leanprover/lean-action/issues/123">#123</a>)</li> <li>See full diff in <a href="https://github.com/leanprover/lean-action/compare/e18f2df7f0d4f30d11a4b963bff9b1140999480c...f807b338d95de7813c5c50d018f1c23c9b93b4ec">compare view</a></li> </ul> </details> <br /> Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

dependabot bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels May 1, 2025

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

bryangingechen mentioned this pull request May 1, 2025

[Merged by Bors] - chore: make dependabot group updates into a single PR #23549

Closed

bryangingechen reviewed May 1, 2025

View reviewed changes

Apply suggestions from code review

4cc2835

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

mathlib-bors bot closed this May 1, 2025

mathlib-bors bot deleted the dependabot/github_actions/dot-github/workflows/leanprover/lean-action-f807b338d95de7813c5c50d018f1c23c9b93b4ec branch May 1, 2025 14:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(deps): bump leanprover/lean-action from e18f2df7f0d4f30d11a4b963bff9b1140999480c to f807b338d95de7813c5c50d018f1c23c9b93b4ec in /.github/workflows#24510

dependabot bot commented on behalf of github May 1, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 1, 2025

Uh oh!

bryangingechen commented May 1, 2025

Uh oh!

mathlib-bors bot commented May 1, 2025

Uh oh!

dependabot bot commented on behalf of github May 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

dependabot bot commented on behalf of github May 1, 2025

Changelog

Unreleased

Added

v1.1.2 - 2025-03-28

Fixed

v1.1.1 - 2024-11-23

Fixed

v1.1.0 - 2024-9-16

Added

Fixed

v1.0.2 - 2024-8-26

Changed

Fixed

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 1, 2025

PR summary 4cc2835e91

Import changes for modified files

Declarations diff

Uh oh!

bryangingechen commented May 1, 2025

Uh oh!

mathlib-bors bot commented May 1, 2025

Uh oh!

dependabot bot commented on behalf of github May 1, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant