Fix leaderboard deploy not triggering on large pushes - #50
Open
Chenyuan Yang (YangChenyuan) wants to merge 1 commit into
Open
Chenyuan Yang (YangChenyuan) wants to merge 1 commit into
Chenyuan Yang (YangChenyuan) wants to merge 1 commit into
Conversation
The merge of PR microsoft#48 changed 468 files (463 under benchmarks/, 5 under leaderboard/). GitHub's push path filtering only inspects the first 300 changed files, which were all benchmarks/ entries, so the leaderboard/** filter never matched and the Pages deploy was silently skipped. The deploy is a cheap static upload, so run it on every push to main instead. Merging this also triggers the deploy that picks up the no-lemma leaderboard changes already on main.
Chenyuan Yang (YangChenyuan)
force-pushed
the
fix-deploy-trigger
branch
from
July 3, 2026 03:59
55affac to
988cd99
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
1 participant
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.
Problem
The leaderboard at https://microsoft.github.io/verus-proof-synthesis/ was not updated after PR #48 merged, even though that PR changed
leaderboard/**files and the deploy workflow triggers onpaths: ['leaderboard/**'].Root cause: GitHub only evaluates push path filters against the first 300 changed files. The PR #48 merge changed 468 files — 463 under
benchmarks/and 5 underleaderboard/. The alphabetically-first 300 were allbenchmarks/files, so the filter never matched and the deploy was silently skipped (last successful deploy run: Jan 22, PR #42).Fix
Drop the
paths:filter and deploy on every push tomain. The deploy is a cheap static upload (~30s), and this repo routinely lands leaderboard changes alongside hundreds of benchmark files, so the same silent skip would keep recurring.Merging this PR will itself trigger a deploy that picks up the no-lemma leaderboard track already on
main.