package Coq 8.12.0 #16876

RalfJung · 2020-07-25T08:36:25Z

No description provided.

Blaisorblade

Thanks for this @RalfJung! Here are some comments.

Blaisorblade · 2020-07-25T08:55:50Z

packages/coqide/coqide.8.12.0/opam

+
+depends: [
+  "coq" {= version}
+  "lablgtk3-sourceview3"


Did the problem with beta7 get fixed?

I don't know, but the latest version 3.3.1 works. I don't think it is worth testing each intermediate version for incompatibilities, nor is it worth keeping a list of incompatible versions forever.

In that case, just stick a constraint in to indicate the supported envelope.

Suggested change

"lablgtk3-sourceview3"

"lablgtk3-sourceview3" {>="3.1.1"}

I used {>= "3.1.0"} so that it at least gets rid of the 3.0beta versions, which seems sensible. This can always be modified later if you prefer.

I have no idea what the future-compat policy is for these packages, but I'd naively also expect an upper bound.

Blaisorblade · 2020-07-25T08:58:00Z

packages/coq/coq.8.12.0/opam

+    "-libdir" "%{lib}%/coq"
+    "-datadir" "%{share}%/coq"
+    "-coqide" "no"
+    "-flambda-opts" "-O3 -unbox-closures"


Having this on by default seems a bit too dangerous — there's serious enough bugs that 8.12.0 doesn't fix — some with bad ocaml versions, others in combo with native-compiler.
The best way forward seems to make native-compiler depend on a "package flag", encoded as a dummy package.

For the last discussion see #16779 and https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users/topic/flambda-using.20Docker-Coq.20images, but I think that's the summary.

Sure I can remove this. I took it from the core-dev packages.

If those flags cause problems, IMO they should be removed from the core-dev packages as well.

Blaisorblade · 2020-07-25T08:58:55Z

packages/coqide/coqide.8.12.0/opam

@@ -0,0 +1,50 @@
+opam-version: "2.0"


Let's remember to split CoqIDE out if there are problems in CI.

I don't follow... we want a CoqIDE package, no?
I consider creating two PRs and tracking their mutual dependencies to be just unnecessary work.

Your call; I was just mentioning @palmskog's suggestion to avoid holding up Coq packages (IIRC because coqide held up some 8.11.* version for a long while). No strong opinion myself.

But again, no action needed if there are no problems in CI 🙂

camelus · 2020-07-25T10:06:56Z

Commit: 674d6a6

@RalfJung has posted 14 contributions.

☀️ All lint checks passed `674d6a6`

These packages passed lint tests: coq.8.12.0, coqide.8.12.0

☀️ Installability check (+2)

new installable packages (2): coq.8.12.0 coqide.8.12.0

🌤️ 2 ignored non-opam files:

packages/coq/coq.8.12.0/files/coq.install
packages/coqide/coqide.8.12.0/files/coqide.install

kit-ty-kate · 2020-07-25T15:43:10Z

Thanks a lot!

MSoegtropIMC · 2020-07-26T12:08:24Z

packages/coqide/coqide.8.12.0/opam

+
+depends: [
+  "coq" {= version}
+  "lablgtk3-sourceview3" {>= "3.1.0"}


@RalfJung @ejgallego : Is there a good reason for the restriction to lablgtk 3.1.0? For a reason yet to be investigated this version does not build on windows, but 3.0.beta5 does and it seems to work fine.

Summing up: no, beta7 had to be banned only for coqide 8.10.*. No comment on potential other problems.
Coq 8.11.0 should be compatible with beta7 since coq/coq#11234.

=== Below the former comments which I dropped.

That's from package Coq 8.12.0 #16876 (comment); there was a specific reason we banned beta7, but beta8 was fine again, and I suspect it was fixed on the Coq side as well.

Sorry: that's to say "no, there's no strong reason for the restriction to be that strict".

In fact, I should have searched the original issue. Indeed, beta7 needn't be blacklisted since
[ide] Don't use -linkall for the GUI app. coq/coq#11234, which was merged in 8.11.0; only 8.10.* need the exclusion, as I noted in [build] don't link Gtk{Th,}Init static initializers into the main library garrigue/lablgtk#100 (comment).

Okay, I opened #16881 to relax the version bound.

MSoegtropIMC · 2020-07-27T08:17:00Z

Thanks, this should work! I didn't try it but hearsay is that beta6 still works on windows but beta7 doesn't (I resorted to beta5 which we have been using on Windows for a while). Before I release the 8.12.0 platform, I will find out what the issue is (a strange link and/or flexlink issue).

Zimmi48 · 2020-07-29T10:38:08Z

Is there a reason why native compute was not disabled on macOS for this version contrary to what was done for versions 8.11.1 and 8.11.2?

Blaisorblade · 2020-07-29T11:04:33Z

Is there a reason why native compute was not disabled on macOS for this version contrary to what was done for versions 8.11.1 and 8.11.2?

No good reason. And apologies, you'd think I'd notice, wouldn't you 🤦?

But we know how to avoid that: fix the core-dev packages. #16876 (comment)
@RalfJung used those as templates, and I'd guess that's the correct workflow (I used it too) — if the new release needs different opam packaging, how else would you know?
OTOH, there's also an opam file in-tree, but that's for devs and uses dune so it's not directly applicable.

See ocaml#16876 (comment).

Blaisorblade · 2020-07-29T11:15:33Z

Just submitted #16908 with the (untested) fix — I took a diff with the 8.11.2 packages.

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

RalfJung · 2020-07-29T12:18:52Z

Ah, I wasn't aware it is still needed -- indeed I assumed it was not since the core-dev packages do not have this.

package Coq 8.12.0

c446476

RalfJung force-pushed the coq branch from f1b16dd to c446476 Compare July 25, 2020 08:53

Blaisorblade reviewed Jul 25, 2020

View reviewed changes

remove flambda options

9850d23

coqide.8.12.0: Add missing constraint

674d6a6

kit-ty-kate merged commit 973b299 into ocaml:master Jul 25, 2020

erikmd mentioned this pull request Jul 25, 2020

[released] Add coq-bignums.8.12.0 coq/opam#1344

Merged

MSoegtropIMC reviewed Jul 26, 2020

View reviewed changes

RalfJung deleted the coq branch July 26, 2020 13:32

RalfJung mentioned this pull request Jul 26, 2020

coq: relax lablgtk3-sourceview3 dependency #16881

Merged

Blaisorblade mentioned this pull request Jul 27, 2020

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

Closed

Zimmi48 mentioned this pull request Jul 29, 2020

On OS X, Coq with native-compiler is too slow coq/coq#11178

Open

Blaisorblade added a commit to Blaisorblade/opam-repository that referenced this pull request Jul 29, 2020

coq/coqide 8.12.0: disable native-compiler on Mac, following 8.11.2

70b4f95

See ocaml#16876 (comment).

Blaisorblade mentioned this pull request Jul 29, 2020

coq/coqide 8.12.0: disable native-compiler on Mac, following 8.11.2 #16908

Merged

Blaisorblade mentioned this pull request Jul 29, 2020

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

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

package Coq 8.12.0 #16876

package Coq 8.12.0 #16876

RalfJung commented Jul 25, 2020

Blaisorblade left a comment

Blaisorblade Jul 25, 2020

RalfJung Jul 25, 2020

avsm Jul 25, 2020

kit-ty-kate Jul 25, 2020

RalfJung Jul 26, 2020 •

edited

Loading

Blaisorblade Jul 25, 2020

RalfJung Jul 25, 2020

RalfJung Jul 25, 2020

Blaisorblade Jul 25, 2020

RalfJung Jul 25, 2020

Blaisorblade Jul 25, 2020

Blaisorblade Jul 25, 2020

camelus commented Jul 25, 2020 •

edited

Loading

kit-ty-kate commented Jul 25, 2020

MSoegtropIMC Jul 26, 2020

Blaisorblade Jul 26, 2020

RalfJung Jul 26, 2020

MSoegtropIMC commented Jul 27, 2020

Zimmi48 commented Jul 29, 2020

Blaisorblade commented Jul 29, 2020

Blaisorblade commented Jul 29, 2020

RalfJung commented Jul 29, 2020

package Coq 8.12.0 #16876

package Coq 8.12.0 #16876

Conversation

RalfJung commented Jul 25, 2020

Blaisorblade left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung Jul 26, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

camelus commented Jul 25, 2020 • edited Loading

☀️ All lint checks passed 674d6a6

☀️ Installability check (+2)

🌤️ 2 ignored non-opam files:

kit-ty-kate commented Jul 25, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MSoegtropIMC commented Jul 27, 2020

Zimmi48 commented Jul 29, 2020

Blaisorblade commented Jul 29, 2020

Blaisorblade commented Jul 29, 2020

RalfJung commented Jul 29, 2020

RalfJung Jul 26, 2020 •

edited

Loading

camelus commented Jul 25, 2020 •

edited

Loading

☀️ All lint checks passed `674d6a6`