Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887

erikmd · 2020-07-26T22:09:10Z

Implements the packaging strategy described in coq/coq#12757

In particular, I inserted a conditional line (-native-compiler (yes|no)) in all coq releases supporting native_compute for the sake of uniformity (i.e., coq {>= "8.5"}), and this thereby amounts to changing the packaging specification of 25 versions of Coq. (Hopefully this large number of opam files touched does not raise an issue w.r.t. opam-repository's CI)

Cc @maximedenes @Blaisorblade could one of you (ideally both! :) have a look at my PR to be sure everything looks fine from a coq / native_compute perspective?

camelus · 2020-07-26T22:53:33Z

Commit: 507151a

@erikmd has posted 4 contributions.

☀️ All lint checks passed `507151a`

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.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

maximedenes · 2020-07-27T08:39:18Z

@erikmd I'm missing context, sorry. Doesn't this PR completely disable native_compute by default? I.e. when coq-native is not installed?

Blaisorblade · 2020-07-27T09:51:02Z

@maximedenes That's exactly the intention; the right context for "why?" is coq/coq#12757.

Blaisorblade · 2020-07-27T11:23:19Z

I guess we should wait for the discussion on coq/coq#12757 to play out before this is merged?

silene · 2020-07-28T08:40:40Z

For the sake of consistency, should the coq-native package depend on coq {>= 8.5}?

Edit: I suppose it would introduce a circular dependency. So, instead, should it be marked conflicts: [ "coq" {< 8.5} ]?

erikmd · 2020-07-28T10:41:40Z

So, instead, should it be marked conflicts: [ "coq" {< 8.5} ]?

I'm not sure it's needed: coq-native is just a package flag so installing it along with coq 8.4 in a switch would not cause any harm: it would just be useless. I don't have a definite opinion on this choice though.

erikmd · 2020-07-28T11:14:40Z

On second thought, installing coq-native + some coq not supporting native_compute would break the assumption that the {coq-native:installed} predicate can be relied on by children packages… so I believe you're right, we should add this conflicts: item.

* Fix linting issues as well

for coq >= 8.7, provided {ocaml:version >= "4.07"} Related: - coq/coq#12757 - coq/coq#540 - https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html

erikmd · 2020-07-28T15:42:00Z

PR updated − don't merge yet though

These opam packages are currently used as templates for releases. Only done for 8.12 and dev, which will be used in the future. The resulting packages are safer and slower (for flambda users); fixing that will require a more proper fix (such as ocaml/opam-repository#16887).

Blaisorblade · 2020-07-29T12:06:39Z

FYI: this will need rebasing over the (more urgent) #16908.

These opam packages are currently used as templates for releases. See discussion at ocaml/opam-repository#16908 and ocaml/opam-repository#16876 (comment). Only done for 8.12 and dev, which will be used in the future. The resulting packages are safer and slower (for flambda users); fixing that will require a more proper fix (such as ocaml/opam-repository#16887).

These opam packages are currently used as templates for releases. See discussion at ocaml/opam-repository#16908, ocaml/opam-repository#16876 (comment) and coq/coq#11178 (comment). Only done for 8.12 and dev, which will be used in the future. The resulting packages are safer and slower (for flambda users); fixing that will require a more proper fix (such as ocaml/opam-repository#16887).

mseri · 2020-10-22T09:24:16Z

@erikmd I am going to close this since it keeps rebuilding dozens of instances of coq every night. Feel free to reopen it if you need to test something or there are new progresses.

@kit-ty-kate it would be useful to have a label to notify the CI to not test a PR until further notice and not re-test an already tested PR, it would avoid us closing PRs to avoid overloading the system

Blaisorblade · 2020-12-10T14:30:01Z

packages/coq/coq.8.12.0/opam

@@ -33,6 +36,9 @@ build: [
    "-libdir" "%{lib}%/coq"
    "-datadir" "%{share}%/coq"
    "-coqide" "no"
+    "-flambda-opts" {ocaml:version >= "4.07"}
+    "-O3 -unbox-closures" {ocaml:version >= "4.07"}


Just to be safe, should this be 4.07.1? We have much less QA on 4.07 AFAIK.

Blaisorblade mentioned this pull request Jul 27, 2020

Updating Coq's (native-compiler, flambda) configure options in opam packages coq/coq#12757

Closed

mseri added the do not merge label Jul 27, 2020

erikmd added 3 commits July 28, 2020 16:52

feat: Add coq-native package flag

8b25da0

feat: Update coq {>= 8.5} to rely on the coq-native package flag

aea3522

* Fix linting issues as well

feat: Add -flambda-opts "-O3 -unbox-closures" configure options

507151a

for coq >= 8.7, provided {ocaml:version >= "4.07"} Related: - coq/coq#12757 - coq/coq#540 - https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html

erikmd force-pushed the coq-native branch from 94e5c2e to 507151a Compare July 28, 2020 15:35

erikmd changed the title ~~Add coq-native package flag~~ Add coq-native package flag & Update coq flags (native-compiler + flambda) Jul 28, 2020

erikmd mentioned this pull request Jul 28, 2020

Which ocaml versions to ultimately provide in docker-coq? coq-community/docker-coq#12

Closed

Blaisorblade mentioned this pull request Jul 29, 2020

Resync coq/coqide dev packages with (safer, slower) release settings coq/opam#1354

Closed

mseri closed this Oct 22, 2020

erikmd mentioned this pull request Nov 23, 2020

Packaging coq-native #17690

Merged

Blaisorblade reviewed Dec 10, 2020

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887

Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887

erikmd commented Jul 26, 2020 •

edited

Loading

camelus commented Jul 26, 2020 •

edited

Loading

maximedenes commented Jul 27, 2020 •

edited

Loading

Blaisorblade commented Jul 27, 2020

Blaisorblade commented Jul 27, 2020

silene commented Jul 28, 2020 •

edited

Loading

erikmd commented Jul 28, 2020

erikmd commented Jul 28, 2020

erikmd commented Jul 28, 2020

Blaisorblade commented Jul 29, 2020

mseri commented Oct 22, 2020 •

edited

Loading

Blaisorblade Dec 10, 2020

Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887

Add coq-native package flag & Update coq flags (native-compiler + flambda) #16887

Conversation

erikmd commented Jul 26, 2020 • edited Loading

camelus commented Jul 26, 2020 • edited Loading

☀️ All lint checks passed 507151a

☀️ Installability check (+1)

maximedenes commented Jul 27, 2020 • edited Loading

Blaisorblade commented Jul 27, 2020

Blaisorblade commented Jul 27, 2020

silene commented Jul 28, 2020 • edited Loading

erikmd commented Jul 28, 2020

erikmd commented Jul 28, 2020

erikmd commented Jul 28, 2020

Blaisorblade commented Jul 29, 2020

mseri commented Oct 22, 2020 • edited Loading

Blaisorblade Dec 10, 2020

Choose a reason for hiding this comment

erikmd commented Jul 26, 2020 •

edited

Loading

camelus commented Jul 26, 2020 •

edited

Loading

☀️ All lint checks passed `507151a`

maximedenes commented Jul 27, 2020 •

edited

Loading

silene commented Jul 28, 2020 •

edited

Loading

mseri commented Oct 22, 2020 •

edited

Loading