Further explanation of build-coq-demo.yml file

[zunction]

Thanks for this coq github action demo which helps entry users like me to get started by cloning your repository to test things out. With your template, I added a simple text file and push the updates up to my remote repository to see how github actions run (realised that when I used your template, github actions also get triggered in the initial commit).

In the CI workflow, I encountered an error when the jobs involving 4.09-flambda with the error:

COQ_IMAGE=coqorg/coq:dev-ocaml-4.09-flambda
  Error response from daemon: manifest for coqorg/coq:dev-ocaml-4.09-flambda not found: manifest unknown: manifest unknown

Would you be able to explain this error?

And then further explain the different jobs (build and mathcomp) in build-coq-demo.yml? It seems to me build is installing coq versions 8.11 and dev on the OCaml versions 4.07, 4.09-flambda and mathcomp just pulls the mathcomp:1.10.0-coq-8.10, 8.11 images from docker hub.

If we were to use the docker-mathcomp images, would it be possible for us to run a job to install other libraries, such as deriving in the image?

Many thanks and a happy new year!

[erikmd]

Hi @zunction, thanks for opening this issue!

I encountered an error when the jobs involving 4.09-flambda
Would you be able to explain this error?

Good point: this just comes from the fact the combination (coq.dev, ocaml.4.09-flambda) is not rebuilt anymore in docker-coq
(cf. this line taken from https://github.com/coq-community/docker-coq/wiki#supported-tags :
Coq dev: 4.05, 4.07-flambda, 4.10-flambda, 4.11-flambda), and I just forgot to update the template in this GitHub repo docker-coq-github-action-demo, sorry for that… so, you should just replace 4.09-flambda with 4.11-flambda for example.

And then further explain the different jobs (build and mathcomp) in build-coq-demo.yml?

Sure. All jobs pull a prebuilt image, the main difference being that:

1. in the (ocaml, coq) specified version, only Coq and Bignums are available,
   and the image is pulled ← https://hub.docker.com/r/coqorg/coq
2. in the mathcomp job, the image contains Coq, Bignums, as well as Math. Components (coq-mathcomp-character),
   and the image is pulled ← https://hub.docker.com/r/mathcomp/mathcomp or https://hub.docker.com/r/mathcomp/mathcomp-dev

So in a typical CI configuration, one should choose to include only one build like image or one mathcomp like image (if your library relies on mathcomp, so that the compilation can be done faster).

Note also that the (ocaml, coq) specification can be viewed as a Facade. Namely:

  build:
    runs-on: ubuntu-latest
    strategy:
      matrix:
        coq_version:
          - '8.11'
          - dev
        ocaml_version:
          - '4.07-flambda'
          - '4.11-flambda'
    steps:
      - uses: actions/checkout@v2
      - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          coq_version: ${{ matrix.coq_version }}
          ocaml_version: ${{ matrix.ocaml_version }}

is equivalent to:

  build:
    runs-on: ubuntu-latest
    strategy:
      matrix:
        image:
          - 'coqorg/coq:8.11-ocaml-4.07-flambda'
          - 'coqorg/coq:8.11-ocaml-4.11-flambda'
          - 'coqorg/coq:dev-ocaml-4.07-flambda'
          - 'coqorg/coq:dev-ocaml-4.11-flambda'
    steps:
      - uses: actions/checkout@v2
      - uses: coq-community/docker-coq-action@v1
        with:
          opam_file: 'coq-demo.opam'
          custom_image: ${{ matrix.image }}

but indeed I realize that some of my remarks above could be integrated somewhere in the repo, maybe in the README…

If we were to use the docker-mathcomp images, would it be possible for us to run a job to install other libraries, such as deriving in the image?

Yes, definitely.

Either these additional dependencies are already specified in your .opam file, so they will be automatically installed by the command opam install -y -j 2 $PACKAGE --deps-only, cf. https://github.com/coq-community/docker-coq-action#install

Or you have some external dependencies, such as Debian packages or so, that you may want to install as well.

In this case, you could write something like:

      before_install: |
        startGroup "Print opam config"
          opam config list; opam repo list; opam list
        endGroup
        startGroup "Install Debian packages"
          sudo apt-get update -y -q
          sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
        endGroup

Let me know if you have other questions.

Many thanks and a happy new year!

Thanks! best wishes

[zunction]

Hi @erikmd, thanks for replying with very clear explanations which is very helpful for my understanding :)

I'm now trying to use coq github actions to test my code, which uses the following (when I do opam list in the opam switch which works): coq 8.10.2, coq-mathcomp-ssreflect 1.9.0 and from the extra-dev repo, I require coq-deriving.

With these requirements, I tried using the image mathcomp/mathcomp:1.9.0-coq-8.10 with the following specifications in my .opam

depends: [
  "coq" { >= "8.10" }
  "coq-mathcomp-ssreflect" {= "1.9.0" | (= "dev")}
  "coq-deriving" {= "dev"} 
]

to facilitate coq-deriving, I included

before_install: |
            startGroup "Print opam config"
              opam config list; opam repo list; opam list
              opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
            endGroup

to make coq-deriving discoverable.

However, my action then runs into an error with the following message:

The following dependencies couldn't be met:
    - coq-knowledge-graph -> coq-deriving -> coq-mathcomp-ssreflect >= dev
        not available because the package is pinned to version 1.9.0

From my many attempts to make it work, it seems to me that the requirement of coq-mathcomp-ssreflect (1.9.0) and coq-deriving (dev) seems to be conflicting with each other, thus leading to the error message that I encounter.

Would you be able to provide suggestions/advise on the problem I'm encountering?

Many thanks!!

[erikmd]

Hi @zunction, indeed it seems that coq-deriving is marked (§1) as incompatible with coq-mathcomp-ssreflect.1.9.0.
this is specified here (§2):
https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-deriving/coq-deriving.dev/opam#L15

So a simple fix should just consist in replacing mathcomp/mathcomp:1.9.0-coq-8.10 with mathcomp/mathcomp:1.10.0-coq-8.10 or a later version.

---

Extra remarks:

• (§1) sometimes, some library might be marked as incompatible with a given version of Coq (e.g., if a new version of Coq is released after a compatible library was released). It is still possible to make opam try to install the library all the same: by using the opam install --ignore-constraints-on=coq your-library command − but this is obviously a hack.

• (§2) FYI, this other .opam file https://github.com/arthuraa/deriving/blob/master/deriving.opam#L15 gives the same constraint as the extra-dev constraint, but if it were different, only the extra-dev contraint would be taken into account.
  Still, this .opam specification from the upstream repo could also be taken into account if it is wished: this is feasible when git pinning the package, see e.g. https://stackoverflow.com/a/62503722/9164010 if you are interested in having more details on this feature of opam.