fix(adapters): close the download-wait race against a fast finish - #492
Open
HappyDevs1 wants to merge 1 commit into
Open
fix(adapters): close the download-wait race against a fast finish#492HappyDevs1 wants to merge 1 commit into
HappyDevs1 wants to merge 1 commit into
Conversation
wait_for_download snapshotted "what's already there" fresh at call time, so a download that finished (and dropped .crdownload) before the wait step was actually dispatched was already in that baseline — never seen as new, spinning the step to a timeout despite a real, successful download. The baseline now lives on the driver, snapshotted once at launch before any step runs, and grows by one entry each time a call matches — closing the race while keeping the existing "second call gets the second file" sequential-download contract from #483. Fixes #489
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
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.
Summary
wait_for_download(crates/flowproof-adapters/src/web.rs) snapshotted "what's already there" fresh, at call time, inside the function. A download that finished (and dropped.crdownload) in the gap between the triggering step and the laterWait until the download completes as <name>step actually invokingwait_for_downloadwas already sitting in that baseline — never seen as new, spinning the step to its full timeout and reporting failure despite a real, successful download.WebAppDriverasclaimed_downloads, snapshotted once atlaunch(before any step runs), and grows by one entry each time a call successfully matches a file. This closes the race for fast/small exports while keeping the existing "second call gets the second file" sequential-download contract from feat(driver): pin browser downloads and wait for one to land #483.unclaimed_downloads()— no live browser needed to prove the diff logic.Test plan
cargo test -p flowproof-adapters --features web— 20/20 tests pass, including 5 new: the race case itself (file_present_but_never_claimed_is_new), already-claimed exclusion, sequential second-call, empty input, multiple-at-once.cargo fmt --checkcargo clippy -p flowproof-adapters --features web --all-targets -- -D warningsPer scope agreed at plan time, no live-Chrome integration test was built for this — the unit tests prove the comparison logic; they can't prove the fix against a real browser end-to-end.
Fixes #489
🤖 Generated with Claude Code