Wish: Composability with other actions

[JasonGross]

It might be nice to port fiat-crypto and coq-tools to the docker coq action.

Currently fiat-crypto uses actions/setup-haskell@v1 with ghc 8.8.1 and 3.0 (and uses my ppa for Coq versions 8.12.0, 8.11.1, 8.10.2, 8.9.1, as well as the tips of master, v8.12, v8.11, v8.10, v8.9), and coq-tools uses actions/setup-python@v1 to test python versions 2.7, 3.5, 3.6, 3.7, 3.8 with Coq versions 8.11.1, 8.10.2, 8.9.1, 8.8.2, 8.7.2, 8.6.1, 8.5pl3, and the tips of the master, v8.11, v8.10, v8.9, v8.8, v8.7, v8.6, and v8.5 branches. However, I don't think docker containers are easily composable with other actions.

[erikmd]

Hi @JasonGross, thanks for opening this.

On the one hand, it's true that unlike "lighter" TypeScript actions (very often named setup-*) which just intend to install some new binaries directly in the GHA worker path, Container actions are a bit more "monolithic" in some sense (in particular from the point of view of docker-coq-action, the bash script intended to call opam install or coqc or make check or so is intended to be run in an isolated way: within the step container, typically thanks to the custom_script feature).

But this appeared to be flexible enough to setup CI for all coq-community projects involving coq and/or ocaml. In particular, the default configuration only requires to specify the .opam file path, and all steps are handled by the docker-coq-action entrypoint, albeit it is possible to customize each element, a bit "in a Travis fashion" (with before_install, install, after_install, before_script, script, after_script, uninstall).

On the other hand (and you are the first user to request this), one might want to "compose" several actions such as actions/setup-haskell@v1 and coq-community/docker-coq-action, which is not straightforward at first sight, but still feasible I believe (cf. item 2 below).

Three related remarks:

1. everything that is touched/changed in the initial current directory of docker-coq-action's container is preserved (thanks to this bind-mount). So that will suffice, for example, to "export" some artifacts that would be generated using coq/ocaml.
2. docker-coq-action+docker-coq does not only bring the coqc/etc. binaries, but a whole opam switch. This opam switch is therefore part of the image, and it is not exported and "lost" for subsequent GHA steps, by design. But if your use case specifically relies upon an "export" of docker-coq opam switches, I guess one might investigate the design of a very similar action (named setup-coq-opam, maybe :) that would just copy the switch from the image, letting further GHA steps run the desired shell commands manually. I'll be very busy in the two upcoming weeks and I'm not sure this plan is 100% feasible (anyway given docker-coq relies on Debian stable, I expect it should work for Ubuntu jobs, obviously not Windows/Mac ones). Anyway, let me know if you think this would be really useful for your use case. In that case we might take a look together at some point to experiment this further.
3. last but not least, note that within the docker-coq-action container, you can install everything you want (the related documentation PR is pending − https://github.com/coq-community/docker-coq-action/issues/49). You can install APT packages, PyPI packages, nix or Haskell…, a bit like what we are currently attempting to implement in ProofGeneral's CI with @hendriktews (even if we pushed the automation one step further, by precompiling Docker images that include coq+nix+emacs: see e.g. this Dockerfile written by Hendrik to have some glimpse of this idea).
   Thus, maybe installing packages with apt-get could suffice for what you want to implement in fiat-crypto's or coq-tools' nextgen CI. I mean, without implementing the "setup-coq-opam" action mentioned in step 2; and it seems this would have the benefit of writing a whole bash script (passed to custom_script) that could be run outside of GHA if need be. Namely, locally on one's workstation or onto another CI platform.

[Zimmi48]

Thanks for writing such a quick and detailed answer @erikmd! I encouraged @JasonGross to open this issue so that this use case would be recorded, even if it might not be easy to address it. There might be another option to easily install various versions of Coq + Python or Haskell, which would be through Nix. I'll raise this point in the issue on CI templates using Nix.

[erikmd]

OK @Zimmi48 !

I agree the use of Nix is interesting to have more flexibility regarding the choice of a particular version of haskell (as opposed as directly installing the single version packaged in APT), but as I mentioned above, this is also directly feasible from the Docker-Coq images as well − relying on Nix :)