opam fetches package info from the package's GitHub, not from coq-extra-dev opam repo

[anton-trunov]

UPDATE:
Here is the real issue: #954 (comment).
And there is a solution by Karl Palmskog: #954 (comment)

ORIGINAL POST:
This repo says:
https://github.com/coq/opam-coq-archive/blob/d50875618e8b5be475a7529c9bc9bbea0350325e/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam#L13 says

but $ opam update; opam info coq-mathcomp-ssreflect returns the following:

version      dev
repository   coq-extra-dev
...
depends:     "coq" {((>= "8.7" & < "8.10~") | (= "dev"))}

hence $ opam install coq-mathcomp-ssreflect fails on Coq 8.10.0:

The following dependencies couldn't be met:
  - coq-mathcomp-ssreflect → coq (< 8.10~ & = dev)
      no matching version

[clarus]

Ah, works on my machine. What does opam repo returns?

[anton-trunov]

$ opam repo
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.

<><> Repository configuration for switch coq8.10 ><><><><><><><><><><><><><>  🐫
 1 coq-extra-dev https://coq.inria.fr/opam/extra-dev
 2 coq-released  https://coq.inria.fr/opam/released
 3 default       https://opam.ocaml.org

[clarus]

OK then I do not know.

[palmskog]

@anton-trunov I can't reproduce this, when I did:

opam update
opam info coq-mathcomp-ssreflect

I see the following line:

depends:     "coq" {(>= "8.7" & < "8.11~") | (= "dev")}

Do you have the latest opam (2.0.5)? Earlier versions had several bugs. If nothing else works, I would just do a new opam initialization (remove .opam and do opam init).

[anton-trunov]

Oh, I think I figured it out. The following script leads to that weird state.

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam pin add coq-mathcomp-ssreflect --dev --no-action
opam install coq-mathcomp-ssreflect

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><>  🐫
[coq-mathcomp-ssreflect.dev] no changes from git+https://github.com/math-comp/math-comp.git

The following dependencies couldn't be met:
  - coq-mathcomp-ssreflect → coq (< 8.10~ & = dev)
      no matching version

No solution found, exiting

opam info coq-mathcomp-ssreflect says

version      dev
repository   coq-extra-dev
pin          git+https://github.com/math-comp/math-comp.git

but in reality the opam file comes not from coq-extra-dev, but from https://github.com/math-comp/math-comp#master, which is not in sync with the opam repository.

This makes me wonder if coq-extra-dev is useful at all. Perhaps people should keep the development versions of their opam files directly in the corresponding repos, since opam can perfectly fetch the package info from there. This should solve the issue of synchronization, unless I'm missing something.

[clarus]

@anton-trunov I do not use the repository coq-extra-dev much myself. It is used for example to check for performance regressions in https://github.com/coq/coq-bench by Coq developers. I think it might be useful to give some visibility to packages under development. Could also be useful for packages with dependencies on other .dev packages.

[palmskog]

@anton-trunov there is a reason that the opam pin add command provides a -k/--kind option, which may be version/path/http/...

If you use:

opam pin add coq-mathcomp-ssreflect dev --kind=version

Then you would be guaranteed to get the extra-dev repo version.

The main utility of extra-dev from my point of view, and why I would oppose its removal, is that it documents (installation instructions for) many Coq projects which do not have regular (tarball) releases. This is invaluable for empirical research on Coq projects.

Since we figured out the problem in this case, can we close this issue?

[anton-trunov]

@clarus , @palmskog That was helpful, thanks a lot!