Add support to build .opam file using dune

[adrianleh]

Many projects use dune build manager to generate the .opam file by running dune build.
It would be nice if the action could handle that step automatically.

As an example project, where this would come in useful, see https://github.com/inQWIRE/QuantumLib

Currently we have to generate the .opam locally and then push or install coq and dune manually in the CI

[erikmd]

Hi @adrianleh, thanks for opening this discussion!

On the one hand, the default entrypoint of docker-coq-action is the existence of an .opam file (which is necessary at least for knowing the list of opam dependencies of the project). Besides, not all projects use dune, e.g., the main Coq libraries I'm involved in use coq_makefile, notably because the longstanding compatibility issues of dune with CEP 48.

On the other hand, the docker-coq-action has been devised with a focus of customization, typically:

• you can override the standard test-script by adding a custom bash script after custom_script: (see this example)
• or less abruptly, you could override the initial command before_install:, to prepend a dune command or so, e.g.:

      - uses: coq-community/docker-coq-action@v1
        with:
          coq_version: ${{ matrix.coq_version }}
          ocaml_version: ${{ matrix.ocaml_version }}
          before_install: |
            startGroup "Generate opam file"
              # dune build … command
            endGroup
            startGroup "Print opam config"
              opam config list; opam repo list; opam list
            endGroup

However at first sight I'd be a bit wary of these custom solutions, as:

• "transferring the whole responsibility of the package-manager spec (the .opam files) to the build-manager (dune)" is not a trivial choice,
• one would lose track of the changes of the .opam file itself,
• and opam's git pinning feature such as opam pin add -n -y -k git coq-quantumlib.dev "https://github.com/inQWIRE/QuantumLib#main" would not be possible anymore if the .opam file is not committed (BTW https://discuss.ocaml.org/t/when-exactly-does-dune-generate-opam-files/8292/4?u=erikmd also mentions that we can/should commit the .opam file even with (generate_opam_files true))

Finally you said:

Currently we have to … or install coq and dune manually in the CI.

Either I didn't understand you remark, or you forgot that with docker-coq-action's default images, coq and dune are already installed (here is the current version of dune).

HTH (otherwise feel free to give more details!)