Skip to content

upgrade to why3 1.9.0 - #1220

Merged
strub merged 1 commit into
mainfrom
why3-1.9
Oct 28, 2026
Merged

strub merged 1 commit into
mainfrom
why3-1.9

Conversation

@fdupress

@fdupress fdupress commented Oct 26, 2026 •

Copy link
Copy Markdown
Member

Please feel free to ignore (and close) this if a better upgrade is possible.
In particular, why3 1.9 seems to bring new features that could be of use if we choose to adopt them...

@fdupress
fdupress requested a review from strub October 26, 2026 17:08
@fdupress fdupress self-assigned this Oct 26, 2026
@fdupress fdupress added the chore Ungrateful tasks that need done but that nobody wants to do label Oct 26, 2026
@fdupress

Copy link
Copy Markdown
Member Author

The result from running nix flake update is a lock file pointing to a 6-month old commit in opam-repository, unlikely to have the why3 release from last week. Is the right way to go about this to simply rebuild and relock from scratch? I don't know.

@fdupress

Copy link
Copy Markdown
Member Author

OK. The flake is fixed.

This PR could possibly be split into one that fixes the flake (by pinning a version of opam-repository that makes sense) and possibly also updates the stable (not done here) and alt-ergo (which I should have done when I bumped it), and then one that bumps why3.

I'm enclined to not bother.

Comment thread src/ecSmt.ml Resolved
@strub

strub commented Oct 28, 2026

Copy link
Copy Markdown
Member

I amended the commit with two small changes: flake.nix now asks for nixpkgs/26.05 for stable, which is what flake.lock already records (the lock and the flake disagreed), and the %r special case passes ~is_neg:false with an assertion, since f_int never builds a negative Fint (negative integers are [-] n), and why3 1.9 rejects a negative mantissa anyway.

@strub
strub enabled auto-merge October 28, 2026 15:53
@strub
strub added this pull request to the merge queue Oct 28, 2026
Merged via the queue into main with commit 1445c70 Oct 28, 2026
20 checks passed
@strub
strub deleted the why3-1.9 branch October 28, 2026 16:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

chore Ungrateful tasks that need done but that nobody wants to do

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants