packages for release 1.8.2 of why3 #28511

claudemarche · 2025-09-12T14:16:11Z

new packages for new release 1.8.2 of why3

jmid · 2025-09-12T14:56:27Z

packages/why3-coq/why3-coq.1.8.2/opam

+This package provides the Coq realizations of Why3 theories."""
+
+url {
+  src: "https://why3.gitlabpages.inria.fr/releases/why3-1.8.2.tar.gz"


Thanks!

The URLs are unfortunately giving a 404 not found error.

Oops! Fixed now. Can we restart the CI process?

Regular CI restarted. But the windows one? I don't see how to do it. I even don't know at all if it would compiled under windows...

If you have opened this PR manually, you can just push the commit to claudemarche:master (which I can see it was opened from), and the CI will run once again 👍

(when using opam publish, a rerun will also push to the same existing PR, but I suspect you are not using that)

But there is no more changes to commit, the problem was on the server holding the source archive...

Ah, now I understand: You fixed the receiving URL and made no changes here!
You can just close the PR and the press the 'Reopen PR' button. I believe that should restart the CI.

It seems you've pressed rerun on the opam-ci page.
I don't have permissions to restart the GitHub Actions Windows workflow:
https://github.com/ocaml/opam-repository/actions/runs/17677129714/job/50241947001?pr=28511
Normally in the top right corner one can choose 'rerun failed' there...

I see that the CI reports incompatibilities with a few packages depending on Why3 but I can't do anything about it.

Could you proceed and accept the PR please ?

jmid · 2025-09-12T17:23:16Z

Would you consider adding x-maintenance-intent entries for the packages?
https://github.com/ocaml/opam-repository/blob/master/governance/policies/archiving.md

claudemarche · 2025-09-15T08:00:19Z

Would you consider adding x-maintenance-intent entries for the packages? https://github.com/ocaml/opam-repository/blob/master/governance/policies/archiving.md

Thanks for the suggestion. The dev team of Why3 will definitely consider this for the next minor release 1.9

jmid · 2025-09-15T09:12:46Z

I reopened this, as I expected you closed with the intention of a "close-reopen dance" to retrigger a CI run.
Please let me know if I misunderstood.

Regarding the CI revdeps failures:

I see frama-v.31.0 failing with Error: Unbound value "Why3.Check_ce.select_model_last_non_empty". I can't seem to find any mention of this API change in https://gitlab.inria.fr/why3/why3/-/blob/1.8.2/CHANGES.md?ref_type=tags. Can you help?
why3find.1.2.0 (and 1.1.0) are failing due to an innocent cram test difference when installed with why3.1.8.2. We could require a lower version of it to run their test suite.

On Windows with a retriggered run:

why3-coq.1.8.2 and why3.1.8.2 build succesfully.
why3-ide.1.8.2 is failing during the installation of conf-gtksourceview3 (it is not supported ATM, but on my TODO list)

jmid · 2025-09-15T11:09:42Z

I see frama-v.31.0 failing with Error: Unbound value "Why3.Check_ce.select_model_last_non_empty". I can't seem to find any mention of this API change in https://gitlab.inria.fr/why3/why3/-/blob/1.8.2/CHANGES.md?ref_type=tags. Can you help?

Found it: It seems it was removed from the interface in the 1.8.2 release:
https://gitlab.inria.fr/why3/why3/-/blob/1.8.1/src/mlw/check_ce.mli?ref_type=tags
https://gitlab.inria.fr/why3/why3/-/blob/1.8.2/src/mlw/check_ce.mli?ref_type=tags

claudemarche · 2025-09-15T11:42:24Z

I see frama-v.31.0 failing with Error: Unbound value "Why3.Check_ce.select_model_last_non_empty". I can't seem to find any mention of this API change in https://gitlab.inria.fr/why3/why3/-/blob/1.8.2/CHANGES.md?ref_type=tags. Can you help?

Found it: It seems it was removed from the interface in the 1.8.2 release: https://gitlab.inria.fr/why3/why3/-/blob/1.8.1/src/mlw/check_ce.mli?ref_type=tags https://gitlab.inria.fr/why3/why3/-/blob/1.8.2/src/mlw/check_ce.mli?ref_type=tags

This is a problem, that change was not intended to appear in the bugfix version 1.8.2.

I'll fix this first in the source release, and then I'll come back to the OPAM packages.

Better to close this PR now, I'll open a new one

claudemarche · 2025-09-16T15:52:57Z

Just reopened the PR with fixed opam files corresponding to a fixed distribution. Let's wait for the CI now...

claudemarche · 2025-09-16T16:13:29Z

The windows build for why3 and why3-coq work, not the why3-ide, this is expected because the latter builds upon GTK. This should not be blocking.

jmid · 2025-09-17T20:42:13Z

There are several lower-bounds failures during

- downgrade conf-gmp        5 to 1

The conf-gmp package is not a direct dependency of either of the 3 submitted packages though.
I think it comes in as a dependency of zarith. Hence it should probably be set there - or we should archive conf-gmp.{1,2,3,4}.

(Flashback to ~2-3 years ago when Kate stated that conf- packages shouldn't be versioned. I'm starting to get her point...)

jmid · 2025-09-17T21:13:00Z

The other 2 errors are revdeps ones frama-clang.0.0.18~beta (failed: conf-libclang.12 failed to build)
Here AFAICS frama-clang.0.0.18~beta has dependencies:

  "conf-llvm" {>= "11.0.0"}
  "conf-libclang" {>= "11.0.0"}

which allows installing

conf-llvm.17
conf-libclang.12

Now installing llvm@17 with the former along with the latter described as
"Virtual package relying on the installation of llvm and clang libraries (<= 12.0.x)"
is asking for trouble. Trouble that cannot be blamed on the why3.1.8.2 release, that is... 🤷

Based on the above, I suggest merging this and working out the failures of the conf-packages in a separate PR.

claudemarche · 2025-09-18T07:38:13Z

Thanks for the approval, thanks also for the useful feedback on the first commit.

mseri · 2025-09-19T18:40:33Z

I agree, the conf packages lowerbounds are not a reason to not merge this. Proceeding

Thanks both!

packages for release 1.8.2 of why3

b73729a

jmid reviewed Sep 12, 2025

View reviewed changes

jmid added needs reporter action and removed needs reporter action labels Sep 12, 2025

jmid added the question label Sep 12, 2025

claudemarche closed this Sep 15, 2025

jmid reopened this Sep 15, 2025

jmid added question and removed question labels Sep 15, 2025

jmid removed the question label Sep 15, 2025

claudemarche closed this Sep 15, 2025

fix original distrib, now compatible with OCaml 5.4

cd23c2f

claudemarche reopened this Sep 16, 2025

jmid added the consider for merge label Sep 17, 2025

jmid approved these changes Sep 17, 2025

View reviewed changes

This was referenced Sep 18, 2025

mark conf-gmp.1 as avoid version #28540

Merged

CI recently started failing conf-package lower bound tests #28541

Open

mseri merged commit 9e8b020 into ocaml:master Sep 19, 2025
1 of 4 checks passed

packages for release 1.8.2 of why3 #28511

packages for release 1.8.2 of why3 #28511

Uh oh!

Conversation

claudemarche commented Sep 12, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jmid commented Sep 12, 2025

Uh oh!

claudemarche commented Sep 15, 2025

Uh oh!

jmid commented Sep 15, 2025

Uh oh!

jmid commented Sep 15, 2025

Uh oh!

claudemarche commented Sep 15, 2025

Uh oh!

claudemarche commented Sep 16, 2025

Uh oh!

claudemarche commented Sep 16, 2025

Uh oh!

jmid commented Sep 17, 2025

Uh oh!

jmid commented Sep 17, 2025

Uh oh!

claudemarche commented Sep 18, 2025

Uh oh!

mseri commented Sep 19, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants