[configure] Check for OCaml 5.0 in configure.

[ejgallego]

No description provided.

[Zimmi48]

IINM, this will make ./configure fail if run with the default options, forcing an explicit -native-compiler no when building with OCaml 5. What if, instead, the default was set to no if the option is not provided and OCaml 5 is used?

In any case, the changelog entry should clarify what the behavior is.

[ejgallego]

IINM, this will make ./configure fail if run with the default options, forcing an explicit -native-compiler no when building with OCaml 5. What if, instead, the default was set to no if the option is not provided and OCaml 5 is used?

I was indeed aware of this, and I choose the current behavior on purpose, to make users to realize that the default doesn't work on OCaml 5.0 so they have to disable native explicitly.

IMHO if we change the default, it should be changed also for OCaml 4.x, it seems a bit weird to have different defaults depending on the OCaml version that is in scope. WDYT?

I'll improve the changelog once we agree on this.

[SkySkimmer]

I feel like configure picking the "best" available default is reasonable.
TBH users are probably using opam which doesn't use the default.

[Zimmi48]

I feel like configure picking the "best" available default is reasonable.

I also feel that way, but I would also be fine with the solution of changing the default to -native-compiler no for everyone (after all, that's already the behavior on opam without coq-native).

[ejgallego]

I think the current solution still has the advantage that we don't introduce a change of behavior from Coq's previous releases. IMHO, this is the best scenario for users from a UI perspective; no changes to how configure behaves, unless the expected default fails (which is to set native=ondemand), which we then signal that to the user that action is needed.

[Zimmi48]

While not being fond of this solution, I won't oppose it. In any case, most users will not be affected, whatever choice we make.

[ejgallego]

Yes, I wonder how the "principle of least surprise" would manifest here as indeed it is not clear to me what users expect when calling configure manually; I guess some people would expect configure to pick the best configuration, whereas others would expect configure to pick the configuration it picked in previous releases.

I'm also not opposed to tweaking this, these little details are indeed annoying.

[ejgallego]

Anyways I've been lazy and after improving the changelog, I've opted for the solution that required me to touch less code in the end :)

[ejgallego]

Feel free to push and do differently if you folks wish.

[Zimmi48]

In the currently chosen solution, will make world work for someone who builds Coq with OCaml 5 without explicitly calling ./configure (typical developer workflow)?

[ejgallego]

In the currently chosen solution, will make world work for someone who builds Coq with OCaml 5 without explicitly calling ./configure (typical developer workflow)?

Yes, config/dune calls configure with -native-compiler no by default. (Tested locally)

[Zimmi48]

@coqbot run full ci

[ejgallego]

Note that make world does not still work with OCaml 5.0 due to deprecations warnings (thus release mode does work)

But that's unrelated to this PR; unfortunately the best we can do is to ignore these warnings (about Thread.exit)

[SkySkimmer]

I still disagree that configure should error by default.
I don't care if we change the default for all ocaml or just when 5.0 is detected.

[Zimmi48]

I'm looking into fixing this PR to change the default behavior to -native-compiler no in all cases.

[Zimmi48]

@coqbot run full CI

[Zimmi48]

Done. I'm convinced that this was the right thing to do.

[ejgallego]

Done. I'm convinced that this was the right thing to do.

I'm fine with it, and I can see why having configure fail by default in 5.x is annoying, tho for me Coq + 5.x support is still very experimental. The advantage is that this choice of UI did make the users notice of the change.

Note however that this is will have all devs and users that still call configure to build Coq have their defaults changed under the hood, silently, so at least let me warn Nix maintainers and @JasonGross so they can update their build scripts to set native explicitly.

[Zimmi48]

Note however that this is will have all devs and users that still call configure to build Coq have their defaults changed under the hood, silently

Well, that's release notes / changelogs are for, and packagers should really read those (especially the "infrastructure and dependencies" part). Maybe we can also put this in the release highlights (together with OCaml 5 compatibility).

With respect to the Nix packaging, there were already issues with native compute (see NixOS/nixpkgs#34657), so having it off by default will probably be a good thing anyway (but it indeed should get an argument so that users can override the default). cc @vbgl

[ejgallego]

Well, that's release notes / changelogs are for, and packagers should really read those (especially the "infrastructure and dependencies" part). Maybe we can also put this in the release highlights (together with OCaml 5 compatibility).

Indeed @Zimmi48 ! Actually I was thinking more of people that package master / etc... and indeed are often bit by our build changes, we don't have a good system to signal them other than well, signal them. Maybe a Zulip channel could be created for packagers, but not sure we have enougth critical mass (or maybe we do ?)

[Zimmi48]

Maybe we do indeed. This Zulip channel doesn't seem like a bad idea to me.

[Zimmi48]

Regarding users beyond packagers, fortunately they are rarely calling configure directly, so they should be mostly unaffected.

[ejgallego]

Regarding users beyond packagers, fortunately they are rarely calling configure directly, so they should be mostly unaffected.

You'd be surprised at the stuff long-term users still do; I know first hand because I helped clean such setup many times!

But indeed, not really relevant to this change.

[Zimmi48]

This PR is ready. It already had a full CI run. The last force-push is to fix a stupid mistake in the changelog.

@SkySkimmer Would you approve / merge when you are available?

[SkySkimmer]

@coqbot merge now