I am not sure this is going to work fine in the long run, see ocaml/opam#2932 and ocaml/dune#880

Keep in mind that we hope to remove the opam files in favor of automatically-generated ones [using dune and dune-release] hopefully before the end of the year.

Maybe the pin command should specify the version? [I can't try right now sorry]

Maybe the pin command should specify the version? [I can't try right now sorry]

Indeed I was able to grab my laptop for a minute

$ opam pin add -n -k path coq.dev .

seems to do what we want?

Hi @ejgallego, thanks for your pointers! (this post in particular is useful to recap the algo applied here)

I agree with several points from your response:

• the command you mention works, and thus suggests it is not necessary to add version: "dev" to be able to use opam pin in some way
• in the long run, this issue won't occur anymore because opam files will be generated by dune, possibly with a much more precise version than "dev".

However, I still see some advantages of integrating this change because:

1. It causes less surprise to the user, namely the implied version will be "dev" by default (rather than e.g. 8.10.1, which makes less sense), and if a user still wants to override "dev" with another version such as 8.11+alpha, he/she could just as well use a similar command: opam pin add -k path coq.8.11+alpha .
2. anyway, this command opam pin add -k path PACKAGE.version TARGET is not formally documented currently (cf. opam pin --help and opam.ocaml.org/doc)
3. and combining -k path and a version is not that intuitive, because opam pin add -k path PACKAGE […] somewhat suggests the pinning should not be version-dependent (like in opam pin add -k version), but path-dependent, with some "fully-specified" .opam file
4. also, the opam files from coq-core-dev are fully-specified because the dev version is hard-coded in the path: https://github.com/coq/opam-coq-archive/tree/master/core-dev/packages/coq/coq.dev, so to some extent, merging this PR would make both .opam sources on an equal footing
5. and IINM adding these version: "dev" lines now won't hinder some later migration/improvement, when the committed opam files will just be removed and auto-generated by dune with a precise version?

WDYT?

Kind regards, Erik

Hi @erikmd ,

2. anyway, this command opam pin add -k path PACKAGE.version TARGET is not formally documented currently (cf. opam pin --help and opam.ocaml.org/doc)

I think the command is documented in the man page: "For source pinnings, the package version may be specified by using the format NAME.VERSION for PACKAGE, in the source opam file, or with edit."

5. and IINM adding these version: "dev" lines now won't hinder some later migration/improvement, when the committed opam files will just be removed and auto-generated by dune with a precise version?

This is indeed my main worry; I am OK merging this if you think it is useful; however we will regress again once opam files are generated by dune, version will be gone again, as it is only added on release / push to opam repos by the current automated workflow. The issues regarding versions upstream will take a long time to solve I think.

Thus anyways users must be aware of the limitations of pinning, even if not ideal, an explicit version is the only safe choice today IMHO.

Hi @ejgallego, thanks for your feedback!

5. […] This is indeed my main worry;

OK.

I am OK merging this if you think it is useful

Thanks! IMHO even if the issue I raised could show up later as you explained, I believe that merging this would be useful (especially for my arguments 1. and 4.). All in all, this PR just amounts to specifying a more sensible "default" version string for the git-committed .opam files, and as suggested by @Zimmi48, it has no downside per se…

Ok, merging then!

I do remain not very optimistic w.r.t. future of people using the commands in the way you describe, IMHO they will broken soon again so I recommend the explicit version.