[ci] Set provenance: false in docker/build-push-action#3222
Closed
joshlf wants to merge 4 commits intoG3xo5e4llm76omanefzdnc2lopucwvv3bfrom
Closed
[ci] Set provenance: false in docker/build-push-action#3222joshlf wants to merge 4 commits intoG3xo5e4llm76omanefzdnc2lopucwvv3bfrom
provenance: false in docker/build-push-action#3222joshlf wants to merge 4 commits intoG3xo5e4llm76omanefzdnc2lopucwvv3bfrom
Conversation
This was referenced Apr 8, 2026
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## G3xo5e4llm76omanefzdnc2lopucwvv3b #3222 +/- ##
==================================================================
Coverage 91.85% 91.85%
==================================================================
Files 20 20
Lines 6067 6067
==================================================================
Hits 5573 5573
Misses 494 494 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
G5iiniran72qxcjixnuxghrjo5paoe57n
branch
from
b16c1a8 to
23171d1
Compare
In `autoParam` automatic proofs, insert `unfold` and `grind` tactics in various places. `unfold` is crucial – without it, *only* statements which are universally true for all possible implementations of the function signature can be automatically proven. `grind` is an SMT-like tactic which is able to automatically discharge a wide range of proofs. Closes #3210 Closes #3213 gherrit-pr-id: G5iiniran72qxcjixnuxghrjo5paoe57n
gherrit-pr-id: Gjw64g3i4n2om5ehu57es67buaxfywnqf
It seems as though `Diagnostics.lean` had been causing the Lean compiler to read all of Mathlib into RAM. The default behavior is more optimized, and so this change allows us to lower the RAM footprint estimate for the Lean compiler from 16GB to 2GB (actually from 8GB to 1GB, but we double as a safety margin) in our integration tests. In theory this should let us run ~8x as many tests in parallel as before. gherrit-pr-id: G3xo5e4llm76omanefzdnc2lopucwvv3b
This works around a buggy interaction between this action and the GitHub Actions cache which is caused by uploading provenance information for the SLSA framework. Since we don't publish these Docker images for external consumption, we don't need provenance information. gherrit-pr-id: Gag74v3izqtosz7f5k5mqsawpiskp3yrm
joshlf
force-pushed
the
Gag74v3izqtosz7f5k5mqsawpiskp3yrm
branch
from
df7827b to
e1df673
Compare
joshlf
force-pushed
the
G5iiniran72qxcjixnuxghrjo5paoe57n
branch
from
23171d1 to
5b0cb64
Compare
joshlf
changed the base branch from
G5iiniran72qxcjixnuxghrjo5paoe57n
to
G3xo5e4llm76omanefzdnc2lopucwvv3b
This was referenced Apr 8, 2026
joshlf
force-pushed
the
G3xo5e4llm76omanefzdnc2lopucwvv3b
branch
7 times, most recently
from
14c6ff1 to
b64ab4d
Compare
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This works around a buggy interaction between this action and the GitHub
Actions cache which is caused by uploading provenance information for
the SLSA framework. Since we don't publish these Docker images for
external consumption, we don't need provenance information.
provenance: falseindocker/build-push-action#3222Diagnostics.leanwithlean --json#3224known_flakytests #3223grindin automatic proofs #3215Latest Update: v2 — Compare vs v1
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gag74v3izqtosz7f5k5mqsawpiskp3yrm && git checkout -b pr-Gag74v3izqtosz7f5k5mqsawpiskp3yrm FETCH_HEADCheckout
git fetch origin refs/heads/Gag74v3izqtosz7f5k5mqsawpiskp3yrm && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gag74v3izqtosz7f5k5mqsawpiskp3yrm && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.