[coq.dev] Use url files instead of rewriting the opam files

[ejgallego]

Now that makes the opam files canonical w.r.t. the ones in the opam repos.

See discussion in #1923

[ejgallego]

Will merge tomorrow if no one opposes.

[palmskog]

@ejgallego can you explain what is going on here? I see a bunch of lines like this:

Ignoring core-dev/packages/coq-core/coq-core.dev/url

How do we know that the right git repo URL is actually being used?

[gares]

Can you point me to the doc of this feature? I seem to recall this was how opam1 was working, but not opam2

[gares]

Now that makes the opam files canonical w.r.t. the ones in the opam repos.

I don't think this is possible. If you find a way, I'm all ears.

[erikmd]

@ejgallego can you explain what is going on here? I see a bunch of lines like this:

Ignoring core-dev/packages/coq-core/coq-core.dev/url

How do we know that the right git repo URL is actually being used?

Maybe the warning is just related to the opam remove command? which indeed, need not read the url file.

[erikmd]

Can you point me to the doc of this feature? I seem to recall this was how opam1 was working, but not opam2

Indeed this seems to be a feature that dates back to opam1:
https://opam.ocaml.org/doc/1.1/Packaging.html#The-ounit-OPAM-package

but I don't see why it would have been removed from opam 2.1.* → the maintainer that will merge this PR should just test this locally I think (e.g. putting a dummy github url, or the proper one) and that'd be good to go I guess.

[erikmd]

good news: regarding the opam 2 compatibility, I've just found this:

https://opam.ocaml.org/doc/Upgrade_guide.html#New-features_1

• the descr file is now preferably replaced by synopsis: and description: fields in the opam file (and strings can be put between """ to avoid escaping issues)

• the url file can be replaced by a section of the form url { src: "URL" checksum: "CKSUM" }. With the above, this allows single-file package definitions

Thus it appears descr is somewhat deprecated, but url can be just as well be used like before 👍

[silene]

but url can be just as well be used like before

There are 23.5k packages in the official Opam repository. Not even a single one of them is using a url file. We should not be using a feature that is de facto unsupported.

[gares]

clarify the status of url files with opam upstream

[silene]

This is what Opam's reference manual has to say: "Older versions of opam used descr and url files besides the opam file, and this is still supported, but the preferred way is now to include their information into the opam file instead." I guess the only reason these files are still "supported" was to ease the transition from Opam 1 to Opam 2.

Looking at the source code, the opam command will forcefully remove from the filesystem any url or descr file it encounters. (This is especially noticeable in the code of opam update and opam pin.) The associated comment is "Remove obsolete auxiliary files, in case" [sic].

[gares]

Thanks for digging. Hence this PR has no future.

[ejgallego]

Ok, fair enough, you'll have to use sed to sync from canonical .opam files then.

Kate pointed out that maybe the whole .dev scheme could be replaced by pin-depends, but I'm unsure how that would work, out of my league.

[ejgallego]

Now that makes the opam files canonical w.r.t. the ones in the opam repos.

I don't think this is possible. If you find a way, I'm all ears.

I mean canonical w.r.t. ones in the Coq repos, sorry for the typo.

Tho, if we manage to use dune-release for 8.17, which is likely, then indeed the files in the main opam repos will be canonical w.r.t. to what's in the 8.17 branch tho.

[Zimmi48]

Tho, if we manage to use dune-release for 8.17, which is likely, then indeed the files in the main opam repos will be canonical w.r.t. to what's in the 8.17 branch tho.

Sounds like a better plan than the proposed CI check.