Stream: Coq devs & plugin devs

Topic: Dev opam packages for Coq related OCaml packages (gappa, ..)


view this post on Zulip Michael Soegtrop (Dec 28 2020 at 18:57):

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?

view this post on Zulip Karl Palmskog (Dec 28 2020 at 20:22):

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.

view this post on Zulip Karl Palmskog (Dec 28 2020 at 20:27):

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)

view this post on Zulip Michael Soegtrop (Dec 28 2020 at 20:28):

@Karl Palmskog : thanks - I will talk to the maintainers of the respective packages.

view this post on Zulip Karl Palmskog (Dec 28 2020 at 20:29):

personally, I think it's good to have a buildable dev package for a project, I maintain this for aac-tactics for example

view this post on Zulip Michael Soegtrop (Dec 28 2020 at 20:32):

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).

view this post on Zulip Karl Palmskog (Dec 28 2020 at 20:41):

since 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.

view this post on Zulip Enrico Tassi (Dec 28 2020 at 22:08):

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).

view this post on Zulip Karl Palmskog (Dec 29 2020 at 00:29):

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.

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 08:56):

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.

view this post on Zulip Enrico Tassi (Dec 29 2020 at 09:11):

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.

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 09:53):

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.

view this post on Zulip Enrico Tassi (Dec 29 2020 at 12:19):

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.

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 12:22):

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.

view this post on Zulip Karl Palmskog (Dec 29 2020 at 12:54):

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.

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:40):

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)

view this post on Zulip Karl Palmskog (Dec 29 2020 at 14:17):

@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.

view this post on Zulip Karl Palmskog (Dec 29 2020 at 14:19):

@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?

view this post on Zulip Rudi Grinberg (Dec 29 2020 at 14:27):

The expectation is that the opam file should still be committed. If it is not committed, opam pin will not work.


Last updated: Oct 15 2021 at 20:02 UTC