Stream: Coq users

Topic: Coq 8.11.2


view this post on Zulip Ralf Jung (May 29 2020 at 11:57):

What is the status of Coq 8.11.2? I see it has been tagged two weeks ago and https://coq.inria.fr/refman/ says 8.11.2 in the title, but opam knows no such version.

view this post on Zulip Ralf Jung (May 29 2020 at 12:02):

oh I see @Pierre-Marie Pédrot just sent an email about that on the coq-dev list^^

view this post on Zulip Ralf Jung (May 29 2020 at 12:02):

I can help with the opam packaging if you want

view this post on Zulip Ralf Jung (May 29 2020 at 12:03):

Cc @Anton Trunov who did that for 8.11.1

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 12:06):

The messages were sent a minute apart, I guess our minds are connected in 11-dimension folds or something :space_invader:

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 12:10):

I still have to sign the MacOS packages btw.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 12:11):

The wiki page says I need credentials for the VM but I don't have them, so I guess I'll need help from @Vincent Laporte again...

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 12:11):

Pinging @Maxime Dénès also, in case he manage to put his hands on those again.

view this post on Zulip Anton Trunov (May 29 2020 at 12:19):

@Ralf Jung :+1: That would be great, I'm a bit swamped right now.

view this post on Zulip Ralf Jung (May 29 2020 at 12:23):

@Anton Trunov okay will do

view this post on Zulip Anton Trunov (May 29 2020 at 12:24):

Thanks! Feel free to ping me if you need an extra pair of hands. I'll have time to help during the weekend.

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:53):

@Pierre-Marie Pédrot You might need to ping @Vincent Laporte through another channel. It doesn't look like he has logged into Zulip yet.

view this post on Zulip Ralf Jung (May 29 2020 at 14:07):

Anton Trunov said:

Ralf Jung :+1: That would be great, I'm a bit swamped right now.

PR is up: https://github.com/coq/opam-coq-archive/pull/1265

view this post on Zulip Anton Trunov (Jun 05 2020 at 21:14):

Hey @Ralf Jung, do you still want to release Coq 8.11.2 on https://github.com/ocaml/opam-repository? I can help with that this weekend.

view this post on Zulip Ralf Jung (Jun 05 2020 at 21:35):

I did the packaging but then somehow forgot to make a PR... d'oh. that's what thesis writing does to you.^^

view this post on Zulip Ralf Jung (Jun 05 2020 at 21:38):

@Anton Trunov PR is up, sorry for the delay: https://github.com/ocaml/opam-repository/pull/16584

view this post on Zulip Karl Palmskog (Jun 05 2020 at 23:16):

can we agree to always make separate PRs for Coq and CoqIDE opam packages? It looks like the opam ci gets stuck on some obscure native dep for CoqIDE...

view this post on Zulip Ralf Jung (Jun 06 2020 at 09:36):

that sounds like it duplicates the amount of work this is as I'd have to submit coq, wait until it lands, and them submit a 2nd PR... I'd rather not do that. but if someone wants to take over, fine for me :)

view this post on Zulip Anton Trunov (Jun 06 2020 at 11:30):

Looks like the luck is our side this time :) Thanks @Ralf Jung !

view this post on Zulip Théo Zimmermann (Jun 07 2020 at 15:15):

@Erik Martin-Dorel Since the opam package has been updated, it might be time to update the Docker images as well.

view this post on Zulip Erik Martin-Dorel (Jun 07 2020 at 16:22):

@Théo Zimmermann Sure; I've just pushed the branch https://github.com/coq-community/docker-coq/commits/8.11.2 so the coqorg/org:8.11.2 build is on-going; I'll update https://github.com/coq-community/docker-coq/wiki as soon as coqorg/coq:8.11 = coqorg/coq:8.11.2.

view this post on Zulip Erik Martin-Dorel (Jun 07 2020 at 17:19):

Done, now latest = 8.11 = 8.11.2 in coqorg/coq

$ docker pull coqorg/coq:8.11 && \
  docker run --rm -it coqorg/coq:8.11 bash -c 'coqtop --version; opam list'
The Coq Proof Assistant, version 8.11.2 (June 2020)
compiled on Jun 7 2020 16:35:34 with OCaml 4.05.0
# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 base        Num library distributed with the OCaml compiler
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-m4                  1           Virtual package relying on m4
coq                      8.11.2      pinned to version 8.11.2
coq-bignums              8.11.0      Bignums, the Coq library of arbitrary large numbers
dune                     2.5.1       pinned to version 2.5.1
num                      0           pinned to version 0
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.8.1       pinned to version 1.8.1
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compiler
opam-depext              1.1.3       Query and install external dependencies of OPAM packages

view this post on Zulip Erik Martin-Dorel (Jun 07 2020 at 17:20):

(Note that this image already has dune 2.5.1 as requested in https://github.com/coq-community/docker-base/issues/8, but I still have to propagate this change for other images < 8.11, so I'll close https://github.com/coq-community/docker-base/issues/8 only at that moment)


Last updated: Jan 27 2023 at 01:03 UTC