The Coq opam repo has a separate set of dev packages. As far as I can see the main opam repo doesn't have such a concept. For the Coq platform master branch I need a few dev packages for OCaml stuff, e.g. gappa, menhir, ... . I wonder what I should do about this. The options I see are:
Strictly speaking I don't need these packages as dev/master, but I think it wouldn't hurt to test the master branch of these packages as well, so I would prefer the first or last option above, but I am open to use the release version for OCaml stuff as well.
@Guillaume Melquiond : this mostly applies to gappa - what is your preference?
@Karl Palmskog : what is your opinion on this?
as long as the project maintainer approves, I think
dev packages for the Platform can live in
extra-dev. Quite a few people use
extra-dev for CI/testing purposes so it seems to me this would be in line with that.
on the other hand, I'm also fine with these dev packages living in the Platform repo - although this means they will likely be used/tested much less. (Recall that the coq-bench for opam actually does test extra-dev now and then)
@Karl Palmskog : thanks - I will talk to the maintainers of the respective packages.
personally, I think it's good to have a buildable dev package for a project, I maintain this for aac-tactics for example
I agree. I now changed the Coq platform master branch so that it takes the dev version of all packages (you probably have seen the Coq opam PRs). I plan to do a daily CI run. Right now CI on Coq platform master passes for all packages except VST (some CompCert master incompatibility).
extra-dev is basically wild west, I wouldn't mind having a dev package for menhir itself there either. I think this could be usable for Coq project developers who want to use (verified) parsers.
The only problem I see with this plan is that projects typically have a
opam file at their root on github (opam lets you install a "git repo" if this is the case). That opam file is, morally, the
.dev version. If we duplicate these opam files in the extra-dev repo, we may need a way to keep them in sync (eg w.r.t. build rules and external deps).
there is already an issue about this: https://github.com/coq/opam-coq-archive/issues/995
Unfortunately, the quality of opam files in repos is terribly low on average.
I would say the packages with an opam file in the root is a minority, and if there is one it doesn't mean that it is up to date (one example is Coq which had for a long time an unusable opam file at its root). I hope that the Coq platform and its CI help to increase the quality of the opam packages. For teh time beeing I don't think an outomated update of opam files from project git repos to extra-dev will work - it likely does more damage than good. I think we first need some manual cleanup to bring it in a sane state. For all packages in the Coq Platform (growing) I am working on this. What might more sense right now is a difference statistic between released, extra-dev and the package git. If the diff is too larger (it should be mostly the SRC URL and the dependecy versions) there should be a warning.
I think it is more convenient to have the opam files in extra-dev. Otherwise I can't install the packages directly via opam (I have to do a git clone first) and the build system for the master and release branches of the Coq platform would have to be quite different.
Hum, opam let's you
opam pin add URL, which clones the git and installs the opam package. I use that, but maybe it's an old way of doing (if you let dune generate the opam file, I guess it does not work). Anyway I'm fine with the plan, but at least for coq-elpi I'll have to remember to push to the dev repo any change I make to the local opam file, since it is the only place were I write down the external build dependencies.
Hum, opam let's you opam pin add URL, which clones the git and installs the opam package.
Still the mechanism with the packages file just listing opam packages and versions won't work any more and I guess also dependencies might get tricky this way. I think this mechsniam is useful for top level packages but not for nested dependencies as we have in the Coq Platform.
To give you the full picture, all project following the coq-community practices do have an opam file. For example the https://github.com/coq-community/docker-coq-action/ works with it to test a project in CI. In particular it uses that file to install the (right) dependencies, so I guess it is kept up to date. It makes also sense to also have .dev versions in extra-dev/, there are good reasons, but I don't see why one would want it to be different than the one in the git repo.
I don't want them to be different. All I say is that I have seen more than one example where the opam file in the project was older than the opam file in released or extra-dev. It will take a manual clean up phase to align released, extra-dev and the project opam files. After that I am fine with installing scripts to keep it aligned for the future.
the reason coq-community projects have opam files in the repo root is because we put a lot of effort into standardizing and parameterizing boilerplate (not least because we use opam in CI via
opam pin add ...). However, other Coq projects (which includes nearly all platform projects) in the wild generally do not put much effort into opam maintenance.
Karl do you know how it works with dune when the opam files are generated by it? Do you also commit the opam file in the repo? (I'm just curious)
@Enrico Tassi I didn't use that functionality so far, but my understanding is that the opam file is not usually committed to the repo in this case.
@Rudi Grinberg can you comment on best practices on opam files and generation of those files by Dune? Should one use a fallback rule or something similar for an opam file and keep it in the repo?
The expectation is that the opam file should still be committed. If it is not committed,
opam pin will not work.
Last updated: Dec 01 2023 at 07:01 UTC