Packaging coq-native

[erikmd]

• This PR is a follow-up of PR Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887
• It is the implementation of item 1 of the Coq Enhancement Proposal 48 (the discussion itself took place in PR CEP for packaging coq-native coq/rfcs#48)
• Regarding the timeline: beyond CI feedback, I guess we should just wait that the CEP 48 and this new package coq-native has been announced, before considering a merge :)

Cc @proux01 @Zimmi48 FYI

[camelus]

Commit: fc5867f

@erikmd has posted 5 contributions.

☀️ All lint checks passed fc5867f

• These packages passed lint tests: coq-native.1, coq.8.10.0, coq.8.10.1, coq.8.10.2, coq.8.11.0, coq.8.11.1, coq.8.11.2, coq.8.12.0, coq.8.12.1, coq.8.5.0, coq.8.5.0~camlp4, coq.8.5.1, coq.8.5.2, coq.8.5.2~camlp4, coq.8.5.3, coq.8.6.1, coq.8.6, coq.8.7.0, coq.8.7.1+1, coq.8.7.1+2, coq.8.7.1, coq.8.7.2, coq.8.8.0, coq.8.8.1, coq.8.8.2, coq.8.9.0, coq.8.9.1

---

☀️ Installability check (+1)

• new installable packages (1): coq-native.1

[kit-ty-kate]

Looks alright to me. I've made it a draft PR to avoid merging it prematurely. Feel free to un-draft it whenever it is ready to go.

[erikmd]

Hi @kit-ty-kate @mseri , I discussed with @Zimmi48 about the timeline, and ideally, this PR #17690 should be merged just before the upcoming release of Coq 8.13+beta1 (planned on next Monday December 7).

So I'm currently preparing a message (regarding the announcement I was mentioning in my initial post) and I just wanted to know if it'd be feasible/acceptable for you to merge this PR on this Sunday afternoon (December 6)?

[kit-ty-kate]

So I'm currently preparing a message (regarding the announcement I was mentioning in my initial post) and I just wanted to know if it'd be feasible/acceptable for you to merge this PR on this Sunday afternoon (December 6)?

Sure, ping me if I forget.

[erikmd]

Hi @kit-ty-kate, ok thanks, but some infrastructure rework (in docker-coq) that is required before doing this is still on-going…
so on second thought we could just wait for a few more days before merging this one! stay tuned anyway :)

[erikmd]

FYI I did the announcement and @gares confirmed me he will tag coq 8.13+beta1 on this Monday 7 December; so feel free to merge this during the day.
Kind regards, Erik

[erikmd]

sorry @kit-ty-kate @mseri, I forgot to ping you in my previous comment, so maybe you didn't receive the notification.

Can you merge this PR when you see my message ?

[kit-ty-kate]

Oops sorry. Done. thanks!

[proux01]

@erikmd there seems to be a consensus on the Zulip discussion that installing this package should print a message warning the user about its experimental status, this seems feasible wia the post-messages: OPAM feature, WDYT?

[erikmd]

Hi @proux01, sure, no objection for that! Feel free to open a PR this afternoon if you have the time, otherwise I'll look into ASAP.
Hopefully one such update of the package coq-native.1 won't trigger a recompilation of all existing installations of the package…