Add deploy job to CI to publish new releases when tag is put.

[Zimmi48]

Meta-issue

The idea is simply to make it as easy as possible for principal maintainers of coq-community packages to publish a new release.

When pushing a new tag, the deploy job would:

• create a release on GitHub, include information about the supported versions of Coq and dependencies;
• create a PR on the Coq opam repository using opam-publish or an ad-hoc script;
• (optional / later) create a PR on the nixpkgs repository, updating the package in coqPackages.

A question is how to include the release date meta-data in the opam file that is published in the opam repository. Either the maintainer updates the date in meta.yml before tagging (but I expect people to forget), or we add it later (but then we can't use opam-publish as-is).

[ejgallego]

Note that topkg / dune-release can already do a lot of this workflow; so indeed you may want to start from there [and hope an eventual integration when all the pieces fall together]

[Zimmi48]

Thanks for the info. I hadn't realized dune-release was so powerful. Then, it makes sense to just wait on Dune support for Coq, migrate the coq-community packages, and document the process using dune-release.

[ejgallego]

dune-release is just a fork of topkg. topkg remains a bit more flexible today. In fact, I find dune-release a bit limited [for example they removed options to target a different opam repos. Thus there is work to do here, but not a lot IMO; but the base model topkg / dune-release bistro seems a good starting point.

I guess the main problem they faced is how to infer certain configuration options without requiring cumbersome config files.

[Zimmi48]

OK, thanks for the additional info. So either we propose changes to dune-release, or we try something on top of topkg.

[ejgallego]

Note that https://github.com/ejgallego/coq-plugin-template includes reasonable support for using dune-release with Coq packages.

[palmskog]

@gares might have some hints for us since he recently automated a similar workflow opening a PR for Elpi, see example, and also this Coq Zulip topic.

[gares]

We looked into dune-release (I use it for elpi for example), but it seems it does not work for vscoq since the opam package (and dune project) are in a subdirectory: tarides/dune-release#471 Also I did not find any use of it in CI, but the doc suggests setting env variables should be enough.

Then we looked into opam-publish which does fewer things and we paired it with a simple action to build a tarball an create a draft release. With some hacks one can convince opam-publish to run in batch mode and open a PR.

So we used it in vscoq, and then I reproduced it in coq-elpi (which is not even a dune project, so it can't use dune-release to begin with). In vscoq @maximedenes did separate the job below into two jobs which always run but don't really do the action in the very end, to keep the CI code tested (I put the if upfront, instead in the commands). I did not do it in coq-elpi. I'll let you chose if the extra CI minutes are worth it in the context of coq-community.

Here my job for coq-elpi:
https://github.com/LPCIC/coq-elpi/blob/dfe528598d04588376eb6b240003647cdd5aa473/.github/workflows/main.yml#L40-L94

release:
    runs-on: ubuntu-latest
    if: startsWith(github.ref, 'refs/tags/')
    needs: [build]
    steps:
      - name: Checkout
        uses: actions/checkout@v3

of course you want to run this (or some parts of this) only if the CI runs on a tag and if the other tests worked (here called build).

      - name: Inject slug/short variables
        uses: rlespinasse/github-slug-action@v4

      - name: Create archive
        run: |
          VERSION="${GITHUB_REF_NAME_SLUG#v}"
          git archive -o coq-elpi-$VERSION.tar.gz --prefix=coq-elpi-$VERSION/ $GITHUB_SHA .

      - name: Release
        uses: softprops/action-gh-release@v1
        with:
          files: coq-elpi-*.tar.gz
          fail_on_unmatched_files: true
          prerelease: true
          generate_release_notes: true
          name: Coq-Elpi ${{ github.ref }} for Coq XXX

Since my tags are named like v1.18.0 I compute the VERSION (without the v).
The slug thing also takes care of other symbols git does not like, I just copied what @maximedenes did, no strong opinion.
Here I create a pre-release with the artifact tarball. I guess for dune projects one needs to also call dune subst (I guess dune release does it for you) so that the version string in the archive is correct (and not %VERSION%).
The release is marked as a pre-release, and the title is a stub (I like to put there the Coq version but it is not immediately inferrable so I just left a XXX placeholder.

And here the dragons:

      - name: Use OCaml 4.14.x
        uses: avsm/setup-ocaml@v2
        with:
          ocaml-compiler: 4.14.x
          opam-local-packages: |
            !coq-elpi.opam

You need ocaml for opam-publish. The action also tries to install the dependencies of the opam files it finds at the root of your project (which is useless here, since we need ocaml opam-publish and not elpi, and also may require non strandard opam repos making it fail). Miraculously it does not look into subfolders (so vscoq CI job does not need the last option).

      - name: Write PAT
        env:
          OPAM_PUBLISH_TOKEN: ${{ secrets.OPAM_PUBLISH_TOKEN }}
        run: |
          mkdir -p ~/.opam/plugins/opam-publish
          printf "$OPAM_PUBLISH_TOKEN" > ~/.opam/plugins/opam-publish/coqelpibot.token

You need to issue an access token from the bot account (just google for PAT), take an old token format otherwise the new ones expire in at most 1 year, put it into a secret, then "preseed" opam-publish configuration.
If you run it by hand, it asks you the token interactively, then it stores it there to avoid asking you again.
Credit to @erikmd for hacking this, I believe.

      - name: Setup SSH
        uses: webfactory/ssh-agent@v0.8.0
        with:
          ssh-private-key: ${{ secrets.BOT_SSH_KEY }}

The bot needs an ssh key, the private part is stored in this secret, the action does the rest.
Now you can push to the github repo of the bot (to his fork of coq/opam).

      - name: Install opam-publish # 2.0.3 because more recent versions do not respect OPAMYES
        run: opam install -y -j 2 opam-publish=2.0.3

Why would it work out of the box?

      - name: Publish
        run: |
          eval $(opam env)
          git config --global user.name coqelpibot
          git config --global user.email coqelpibot@inria.fr
          OPAM_SUITE=released
          TAG=`git tag --sort=-v:refname|head -1`
          opam-publish --tag=$TAG --packages-directory=$OPAM_SUITE/packages --repo=coq/opam --no-browser -v ${TAG##v}	https://github.com/LPCIC/coq-elpi/releases/download/$TAG/coq-elpi-${TAG##v}.tar.gz

You want to prepare a commit for coq/opam, the author is the bot.
Here I use old code of mine to get the tag name, I think I should have used the github.ref and the slug above, I was lazy (and my tag names don't really need any magic).
Then the URL must match the one of the artifact attached to the pre-release above.

[gares]

One thing I did not understand is where the github user name (of the bot) is written.
Maybe it is in the PAT itself, mybe it uses the git user.name... I don't know, so I was consistent (see also the file name where the PAT is stored).

I did the fork of the repo myself (using the bot account). I don't know if it is necessary. opam-publish for sure does a git clone of it, I don't know if it is able to do the fork. Since the cloning was not working I tried doing the fork, but it did not solve the problem (or at least, was not sufficient). In any case, you have to do the fork only once.

[erikmd]

Dear @gares,
Sorry I just skimmed your long comment, but note that for the regression

      - name: Install opam-publish # 2.0.3 because more recent versions do not respect OPAMYES
        run: opam install -y -j 2 opam-publish=2.0.3

I opened an issue: ocaml-opam/opam-publish#132
which is still pending, but which I can volunteer to (try to) fix this month… as it is blocking for our learn-ocaml CI/CD setup.

[erikmd]

FYI @Zimmi48 @gares, the opam-publish maintainers just released version 2.3.0, which contains a new option --no-confirmation, which makes it possible to greatly simplify the GHA workflow of learn-ocaml I was talking about earlier:

• https://github.com/ocaml-sf/learn-ocaml/blob/master/.github/workflows/opam-publish.yml (should be generic enough to be easily adapted)
• https://github.com/ocaml-sf/learn-ocaml/blob/master/.github/workflows/test-opam-publish.yml (a unit test !-)