[DEV] autosetup: converge the compilation-workaround loop instead of timing out - #145
Merged
Conversation
A contract pinned to an absent compiler was rewritten to whichever compiler was default, regardless of what its pragma allows. For an exact pragma the rewrite cannot compile, so the next pass re-detects the mismatch and re-pins — the two workarounds undo each other until the retry budget or the job timeout ends it. The fallback is now a per-contract plan: each pinned contract is offered only compilers its pragma admits, and an unreadable or unparseable pragma still takes the first candidate. When a contract has no viable substitute the run raises UnsatisfiableSolcPinError naming the contract, its pragma and the binary to install, instead of retrying a substitution that cannot work. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The loop compares each pass against its own starting state, so it only notices a pass that changed nothing. Two workarounds that undo each other each change the conf relative to their own baseline, and alternate across passes, so the loop runs to the retry budget — one full certoraRun per pass. Record every (workaround, conf delta) applied in the run. A pass whose changes have all been made before means something is undoing them, so stop there and name them. A pass that also lands a new change is still converging and continues. missing_library_harness is exempt via progress_outside_conf: regenerating its harness covers one more library each time, which is real progress the conf does not show. Its own _harnessed_libs guard bounds it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Six defects found by review of the two commits below it: - Candidate order put whatever `solc` is on PATH ahead of the project's own default, so a wide pragma could pick an unrelated compiler. The default now comes first and plain solc is the last resort. - A non-UTF-8 source (an accented byte in a header comment) raised out of read_pragma_from_source_file and killed the loop; it now reads as an unknown pragma. - parse_pragma_constraint understands `=X.Y.Z` and `~X.Y.Z`, and reports a disjunction as unknown rather than mis-parsing it. - The terminal raise is gated on a pin the conf actually carries, so a pin seeded from the default compiler no longer fails the run. - certora-fixconf reports the unsatisfiable pin and still writes back the fixes already applied, instead of exiting on a traceback. - The change ledger is scoped to one run of the loop: fixconf runs it twice on one manager, and the second run may legitimately re-apply the first's changes. An exempt workaround no longer vetoes repeat detection for the whole pass — it only keeps its own changes out of the ledger. The note on missing_library_harness now states what its guard keys on and that max_retries is what bounds it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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.
Mirror of #134 onto the
devbleeding-edge branch.Source branch:
shelly/workaround-loop-convergence. This branch is that head merged forward withdev; #134 itself is untouched and still targetsmaster.Per the
devbranch policy this merges without review oncepyrightandpytestare green.