Stream: Coq devs & plugin devs

Topic: coq.dev package

view this post on Zulip Matthieu Sozeau (Jun 11 2021 at 09:39):

The current coq.dev package in opam is very misleading. Upgrading it does not force an upgrade of coq-core.dev, is there a way to fix this?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2021 at 09:42):

I don't know how to make the devscheme actually pull dependencies; when using dune-release for example a version number based on the git describe is added so these kind of things can be tracked properly.

view this post on Zulip Michael Soegtrop (Jun 11 2021 at 11:50):

I don't think this can be fixed - if the opam packages says to packages are generally compatible, they should be generally compatible. If coq.dev and coq-core.dev heavily depend on each other, it would probably be better to make them one package.

view this post on Zulip Théo Zimmermann (Jun 11 2021 at 15:04):

There is no coq-core.dev package in coq-opam-archive though, is there?

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:31):

No, I think it's taken directly from the coq.git archive

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:32):

But I get: 

# opam info coq.dev

<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><>  🐫
name                   coq
all-installed-versions 8.8.1 [system]  8.8.2 [ocaml701]  8.9.1 [coq.8.9 coq.8.9.1 coq89]  8.10.1 [coq.8.10]  8.11.0 [coq.8.11]  8.11.2 [ocaml4071 ocaml410-flam certicoq]  8.12.0 [certicoq-8.12]  8.12.2 [coq.8.12]  8.13.0 [coq.8.13]
                       8.13.1 [coq.8.13.1]  dev [coqdev]
all-versions           8.0.dev  8.1.dev  8.2.dev  8.3  8.3.dev  8.4pl1  8.4pl2  8.4pl4  8.4.5  8.4.6~camlp4  8.4.6  8.4.dev  8.4.dev+ltacprof  8.5~beta1  8.5~beta2  8.5~beta3  8.5~rc1  8.5.0~camlp4  8.5.0  8.5.1  8.5.2~camlp4  8.5.2
                       8.5.3  8.5.dev  8.5.dev+ltacprof  8.6~beta1  8.6  8.6.1  8.6.dev  8.7+beta1  8.7+beta2  8.7.0  8.7.1  8.7.1+1  8.7.1+2  8.7.2  8.7.dev  8.8+beta1  8.8.0  8.8.1  8.8.2  8.8.dev  8.9+beta1  8.9.0  8.9.1  8.9.dev
                       8.10+beta1  8.10+beta2  8.10+beta3  8.10.0  8.10.1  8.10.2  8.10.dev  8.11+beta1  8.11.0  8.11.1  8.11.2  8.11.dev  8.12+beta1  8.12.0  8.12.1  8.12.2  8.12.dev  8.13+beta1  8.13.0  8.13.1  8.13.2  8.13.dev  dev

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version      dev
repository   coq-core-dev
pin          git+https://github.com/coq/coq.git
source-hash  b97a2ce8
url.src:     "git+https://github.com/coq/coq.git"
homepage:    "https://coq.inria.fr/"
bug-reports: "https://github.com/coq/coq/issues"
dev-repo:    "git+https://github.com/coq/coq.git"
authors:     "The Coq development team, INRIA, CNRS, and contributors"
maintainer:  "The Coq development team <coqdev@inria.fr>"
license:     "LGPL-2.1-only"
depends:     "dune" {>= "2.5"} "coq-core" {= version} "coq-stdlib" {= version}
synopsis     The Coq Proof Assistant

So clearly coq.dev depends on it

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:39):

I see your point about the dependency being broken though. The should be special support to say that you want the exact same git commit

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:42):

A general opam upgrade does work as expected, it's just that opam upgrade coq.dev doesn't

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

Is opam upgrade even supported when you choose to pin directly from the git repository? In any case, coq.dev from the core-dev repository should keep working (in a fresh switch at least).

view this post on Zulip Guillaume Melquiond (Jun 15 2021 at 07:44):

Did you happen to pin the Opam package from the Coq repository? Otherwise, I don't understand how it could take precedence over the one in the Opam repository.

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:47):

Well according to the opam info, my coq.dev package does come from coq-core-dev

view this post on Zulip Guillaume Melquiond (Jun 15 2021 at 07:48):

opam pin list?

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:48):

But that's probably misleading as it does have a dependency on coq-core.dev which I can't see from looking at the coq/opam file in coq-core-dev

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:48):

Yep, it's pinned to the git repo

view this post on Zulip Matthieu Sozeau (Jun 15 2021 at 07:50):

So the only surprising thing is that it tells me that coq.dev is part of the coq-core-dev repository, while it's actually a git source (it does report the pin and hash though)

view this post on Zulip Théo Zimmermann (Jun 15 2021 at 08:36):

Yeah, the behavior of opam with respect to pins from git repositories has always been puzzling to me.

Last updated: Apr 19 2024 at 22:01 UTC