pin provers to better support replication; (this is only partial: nixpkgs allows easy pinning of z3 down to minor only, and cvc4 is pinned only by virtue of no longer being maintained).
The pinning upgrades all provers to their maximum version supported by why3 1.6.0, stopping short of upgrading cvc4 to cvc5 due to clear instability in cvc5 and its interactions with why3 (50/50 chance of High failure). A minor refinement is needed in the case of one SMT call which fails with z3 4.12.2 and all other solvers, but succeeds with z3 <= 4.12.1.
The pinning of alt-ergo to 2.4.2 works, but leaves paths and derivation names unchanged, so alt-ergo-2.4.2 appears in paths as alt-ergo-2.4.3. Avoiding this might require vendoring a derivation for alt-ergo. (@vbgl , do you have a suggestion for this? alt-ergo is internally split into 3 separate derivations and that level of override-based surgery is beyond the effort I'm willing to put into pinning an SMT solver.)
If we decide the pins need more work, it should be fine to only keep the first commit, and at least make it easier and safer to later improve our derivations.
This reworks the nix configuration to:
z3down to minor only, andcvc4is pinned only by virtue of no longer being maintained).The pinning upgrades all provers to their maximum version supported by
why31.6.0, stopping short of upgradingcvc4tocvc5due to clear instability incvc5and its interactions withwhy3(50/50 chance of High failure). A minor refinement is needed in the case of one SMT call which fails withz34.12.2 and all other solvers, but succeeds withz3<= 4.12.1.The pinning of
alt-ergoto 2.4.2 works, but leaves paths and derivation names unchanged, soalt-ergo-2.4.2appears in paths asalt-ergo-2.4.3. Avoiding this might require vendoring a derivation foralt-ergo. (@vbgl , do you have a suggestion for this?alt-ergois internally split into 3 separate derivations and that level of override-based surgery is beyond the effort I'm willing to put into pinning an SMT solver.)If we decide the pins need more work, it should be fine to only keep the first commit, and at least make it easier and safer to later improve our derivations.