Fix concurrent downloads of the Apalache distribution - #2026
Merged
Merged
Conversation
The Apalache distribution was unpacked directly into ~/.quint/apalache-dist-<version>, and a download is considered done as soon as `bin/apalache-mc` exists. So a quint process started while another one was still unpacking would use a partial distribution, and TLC would fail with "Could not find or load main class tlc2.TLC". This made the examples dashboard fail on main, where the TLC examples weakFairness and strongFairness run in parallel and download Apalache. Unpack into a temporary directory and move the distribution into place once complete. If another process moved its own copy first, use it. With a fresh QUINT_HOME and 8 concurrent TLC runs (3 rounds), 9 of 24 runs failed with the error above before this change, and none after.
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.
The Examples Dashboard is failing on
mainsince #2025, onlanguage-features/weakFairness.qnt(verify). The logging added in #2025 shows why:Seems like this is only happening after that PR because I added way more TLC tests, so the chances of this race condition have increased.
This PR unpacks the distribution into a temporary directory and moves it into place once complete. If another process moved its own copy first, that one is used. The temporary directory is always removed. This also applies to users running several
quint verifycommands in parallel on a fresh machine.QUINT_HOMEand 8 concurrent TLC runs (3 rounds), 9 of 24 runs failed withClassNotFoundException: tlc2.TLCbefore this change, and none after, with no temporary directories left behindCHANGELOG.mdfor any new functionality