Skip to content

Dev Meeting 2020.11.06 (opam and coq repos)

Jump to bottom
Anil Madhavapeddy edited this page Nov 20, 2020 · 4 revisions

Agenda

Main purpose of this meeting is to add/strengthen the bridges between the islands!

  • What’s working?
  • What’s not working?
  • What potentially can be improved in opam itself to assist?

Notes

Present: @avsm, @AltGr, @rjbou, @dra27, @samoht, @claret

@claret introduced Coq's opam-repository. Coq bench is used to test the matrix of Coq packages against baseline OCaml version on various architectures. Zulip channel in addition receives error reports from this bench. @avsm - how are problems communicated back to the package maintainer? @claret - manually at the moment. If the issue is simple then a pull request is simply opened directly.

@avsm - what's the matrix of compiler versions? @claret - all of the compiler versions from 4.02+; it takes about a month to do a complete run of tests (so packages are tested in a random order). A lot of the errors tend to be transient failures (download errors, etc.). @avsm - same problem with opam-repository, which we're working towards mitigating with caching to eliminate the time wasted by transient errors

@dra27 - how many machines are dedicated to this? @claret - 1 big machine @samoht - is this simply a cron job set-up on the server? @claret - each OCaml version has its own Dockerfile, they are started up and given as long as needed. @samoht - and the results are then converted to a web server? @claret - the builds output results in CSV as they go (as the jobs can take several months) and then these are pulled, converted to HTML and pushed to GitHub Pages

@avsm - are the depexts particularly complicated? @claret - some packages require, for example, Python, but these depexts are installed globally. @avsm - this works to scale with new external dependencies? @claret - at the moment it's only a dozen or so depexts, so it's not at present a big enough problem.

@avsm - does the Coq opam-repository depend on the OCaml one? @claret - yes! @avsm - we've discussed the idea of discovery of remotes, for example being able to say opam install coq:... and have opam discover the repository automatically. This might potentially allow opam-repository testing also to check for downstream regressions.

@claret - testing continues on old compilers in order to ensure that packages submitted definitely can still be installed (even if with old compilers) in, say, 5 years.

@avsm - looking at this, how do we close the loop for getting more maintainers involved in this? For example, we've clearly got some duplicate effort (opam-health-check and coq-bench). @claret - at the moment there aren't enough packages to have to worry @avsm - indeed, though that's how opam-repository started with @samoht and @avsm and then it grew, which will hopefully happen for Coq too! Is this repo the "standard" way for installing and using Coq now? @claret - yes, using opam is the normal way of using it.

@avsm demonstrated the build cluster being used for opam-repository - the new system is bringing testing time for opam-repository down to 90 mins, and should be expandable. Coq - having significant computational needs - could be a good case for expanding the cluster further.

@avsm - ocaml-ci at the moment is able to produce precise lists of packages which altered between commits to be able to have improved incremental testing, which could also help here. Switching our CI reporting to Zulip could be good for us on the OCaml side to adopt, too.

@avsm - how many people are working on this at the moment? @claret - mostly me! Major work five years ago, and then mostly simply maintained since then. It's fairly simplistic @avsm - but effective! @dra27 - opam-health-check is at present looking at being overhauled early next year, so could be very interesting either to look at features which can be merged, or being able to deploy for testing either repository/ecosystem.

@avsm - what's done at present for packaging Coq on Debian? @claret - Coq itself is packaged, and then it goes from there. There's also an effort at the moment with Coq platform, especially to improve Windows support.

@avsm - docs.ocaml.org is being overhauled at the moment to have documentation package universes for all packages. Potential to be able to do the same for the Coq repo.

@dra27 - how frequent is package submission? @claret - a few per week, it's actually dropped with COVID slightly!

@samoht - how many of the packages are distributing binaries, rather than proofs? @claret - there are a few, principally packages which extract to OCaml and then compile (for example CompCert). @samoht - but does that then stay in Coq's repository, or shift upstream to opam-repository? @claret - no, they stay in opam-repository at the moment. @samoht - it could be very interesting to split this, although the support in opam for binary packages is limited. @dra27 - we could have, for example with compcert, the idea where the Coq repo package produces the OCaml source which becomes the source package for opam-repository, so installing compcert via opam-repository builds the compiler vs installing it via Coq repository does the formal extraction of the code. @samoht - similar need in Mirage both with code extracted from Coq and from F*; @claret - Tezos have similar issues. @dra27 - this would then tie neatly into Conex, allowing the extracted code to be signed. So the extraction can then be trusted without necessarily having to re-run the extraction.

Clone this wiki locally