Resync coq/coqide dev packages with (safer, slower) release settings #1354
Conversation
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).
Warning: haven't tested the comment syntax.
| @@ -33,7 +33,8 @@ build: [ | |||
| "-libdir" "%{lib}%/coq" | |||
| "-datadir" "%{share}%/coq" | |||
| "-coqide" "no" | |||
| "-flambda-opts" "-O3 -unbox-closures" | |||
| # These settings are used as templates for release packages | |||
There was a problem hiding this comment.
I don't understand the point of this comment here. If native-compiler is broken on macOS, I'd expect a comment pointing to why it is broken. Whether or not they are sued for release packages is irrelevant IMO; even dev packages should work on macos after all.
There was a problem hiding this comment.
Likewise, "unbox-closures" is not set because it is broken, so the justification should be a link to the issue for that, not "this is a template for releases".
There was a problem hiding this comment.
True. My comments was meant for the current users of these packages, whose revealed preferences seem different.
This PR could also wait for ocaml/opam-repository#16887 to be finalized and sync with that, since the solution there should be much better, and would be needed even if we fixed all current bugs.
There was a problem hiding this comment.
That seems to still enable flambda for ocaml >= 4.07 -- so only older ocaml is broken?
Indeed if that PR is likely to be accepted, it makes sense to wait for it.
There was a problem hiding this comment.
That enables flambda if you picked an flambda compiler (else those options are ignored).
so only older ocaml is broken?
flambda+native is also "YMMV", depending on multiple factors, but native must also be selected explicitly.
The story for native is even longer and I'll spare you, but the plan (in coq/coq#12757) includes producing sufficient docs; eventually, enabling native should precompile native versions of all libraries where it makes sense.
|
Also no idea why CI failed, hope that's a spurious failure; investigation can wait. |
|
for some reasons coqide.dev failed to install, but I don't get why from the log It seems to build correctly |
|
Disk out of space? EDIT: or permission error (but that'd be worse). |
|
@Blaisorblade are we going to see any progress on this PR in the near future? The same error occurs on several runners, so it's not clear to me this is a spurious error. |
|
I don’t see how the error could be due to this PR. EDIT: it could be a valid underlying error. This was marked as draft while waiting for ocaml/opam-repository#16887, but that’s also stalled. |
|
But I don’t have to follow up on this in the near future, nor do I see anything I can follow up on. So closing; feel free to resurrect. |
|
@palmskog This is sure going to lead to more confusion and issues down the road when these packages are not in sync with the ocaml repo. |
|
Opened #1389. |
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).