OPAM files in extra-dev vs. upstream repository

[liyishuai]

We can already track GitHub repos with opam pin https://github.com/user/repo.git. Is it still worth maintaining a (very likely outdated) OPAM file in extra-dev? Should we host only the URL, from which to fetch all other OPAM configurations?

[clarus]

Does it work for dependencies? What do you mean by "hosting url"? As far as I know, the development packages are mainly used for two things:

• performance testing https://github.com/coq/coq-bench
• visibility

[liyishuai]

Developers can update their OPAM file rapidly and possibly forgot to merge changes here, making the configuration here outdated, including dependencies and build processes. If we only store a URL and let user fetch the latest configuration through that URL, that might solve the problem.

[palmskog]

If developers submit their OPAM files here, we can at least review them and correct mistakes and minor flaws. With only an URL, we can't really ensure anything, and any changes would have to be approved by upstream repo maintainers. Therefore, I'm against storing only URLs.

We are actively using the extra-dev repo and its metadata for finding and analyzing Coq projects for proof engineering research. Only storing URLs would be a big hindrance.

[palmskog]

@liyishuai for the record, I think the problem mentioned here (discrepancy between upstream opam file and extra-dev opam file) is very real and we should attempt to address it in less radical ways. For example, we can help project maintainers migrate to dune when the Coq support there is in place, and then dune will generate an idiomatic opam file.

It may even be a good idea to keep this issue open as a reminder.

[liyishuai]

I'm not familiar with Dune; it'll be nice to have that solution.

[anton-trunov]

FWIW, here is a somewhat related issue: https://github.com/coq/opam-coq-archive/issues/954.