Skip to content
Théo Zimmermann edited this page Aug 8, 2021 · 3 revisions

Notes of a meeting between Karl Palmskog and Théo Zimmermann on 2019-09-18.

Release coq-community packages for Coq 8.10

Coq 8.10+beta3 has been released and Coq 8.10.0 should land soon. We should start releasing opam packages compatible with Coq 8.10 for coq-community packages. We should write documentation for maintainers in the wiki, with some tips on how to submit an opam package (there should also be a PR template in the Coq opam repository).

Changelog

It seems like the standard nowadays is https://keepachangelog.com/en/1.0.0/. Some projects in the Coq ecosystem (Math-Comp) and in coq-community (reduction-effects) are already using it. We should probably recommend it for coq-community projects, with a link to an example. The changelog of reduction-effects is too small to be used as an example, but Karl is going to try to produce one for Chapar, which received many changes recently.

Automate the release process (cf. #49)

We should simplify the release process before Coq 8.11. The solution is probably to use Dune and dune-release. (probably not for a while)

Generation of templates (cf. #67) (there is generate.sh now)

Goal: provide a convenient and easy way to use coq-community templates in a coq-community project.

The tool may clone the templates repository (https://github.com/coq-community/templates), or use a git submodule to pin it to a particular version, and generate all the files. Could be written in bash or OCaml. The advantage of bash is that it won't need additional dependencies (except mustache in fact...).

Generation of documentation

To start with, we can rely on just coqdoc, and add some extensions later maybe. It's probably best to start by setting up continuous deployment to a gh-pages branch, rather than a docs/ sub-folder, because the latter would require the maintainer to remember to update it locally before committing.

Publishing extraction projects on OCaml's opam repository

This is something that we could do. To avoid depending on Coq, the "source" archive would include the extracted OCaml files. This could probably be done using Dune (and a fallback rule) and dune-release.

CI: explore GitHub Actions (done)

GitHub built their own CI/CD solution called Actions. It is in fact more powerful than just CI and can automate many things. We should explore it as this might provide an even easier way to set up CI in a coq-community project. It relies on Docker images, so this should make it easy to port the Docker + opam setup, but also the Nix setup (using a NixOS Docker image).

EDIT: in https://github.com/coq-community/templates/issues/1#issuecomment-541896329, @liyishuai said:

I've also tried GitHub Actions, resulting in frustrations, as it doesn't support starting from a Coq docker.

Backups (cf. #76)

We already back-up coq-community repositories on GitLab, but this is not done automatically when a new project is added. It should be automated, and the easiest way is probably to add this to @coqbot. We could also explore backing up coq-community repositories frequently on Software Heritage. Finally, backing up meta-data such as issues would require interfacing with the GitHub API to regularly synchronize its content. Currently, this is not even done for Coq. We don't know of any free software that does it.