Hi, I was wondering what was the best approach to write a Gitlab runner script in order to install a few dependencies with opam, then run an ocaml project in order to publish what is produced (in my case a webpage).
My main questions are:
Which image should I use? I’m fine with having any recent OCaml version. I don’t need to test with several, I just want it to be fast (and reduce carbon footprint). It seems that using Alpine would be a nice way to go, but https://hub.docker.com/r/ocaml/opam doesn’t have a tag for recent OCaml versions with it right?
How should I perform caching efficiently?
I have read this topic in full but I’m not sure it answers my questions. For instance the solution proposed by @gasche looks cool but I think it’s not exactly what I need.
Everything I knew about gitlab CI at the time of that thread, I wrote carefully in gitlab-ocaml-ci-example, and then I quickly forgot about it. I would maybe recommend having a look at the .gitlab-ci.yml file there, and reusing things from it. It also includes some deployment logic.
Instead of trying to move between _opam and .opam, the script only use _opam – so there is a single “local” switch at the top of the root directory, and it works just fine. There are various tweaks to make it easy for humans to clear the caches from the Github UI, and links to the various documentation I had to read to make it work.
One disappointing thing I realized later is that this CI script is very tied to specifically how Gitlab.com public workers work. If you try to use the same script on gitlab.inria.fr, it will not work, because they designed their own CI workers that work in a different way (of course), and you need to write different scripts.
I thought the Rocq community had reached a nirvana of judicious Nix usage for CI that solves all these problems for good?
Ah, I’m indeed using the Inria Gitlab so maybe that’s why I didn’t manage to adapt your .yml file…
I’d like to use a local switch, but when using an image that already comes with a global switch it seems like a waste to install a local switch manually…
Maybe I should just accept it since it will be cached anyway.
As for Nix, maybe they solved it, I wish I knew how.
For Why3 (and it is quite similar for Coq itself), a Docker image is used as the cache. In other words, there is a Dockerfile somewhere which describes the build/deployment environment. The Docker image is built once and then stored inside the internal Docker registry of the Gitlab instance. (It is only rebuilt when Dockerfile is modified.) Then the various jobs use it. Here is an excerpt:
able to cache one or two global switches in a custom opamroot. Especially for Windows, which needs a short C:\o opam root since OCaml has the long-standing Windows bug of not supporting paths longer than 260 characters.
jobs should be agnostic to desktop/GitLab/GitHub
support building OCaml inside Docker images for the Linux part of the DkML test matrix (GitLab is supercomplicated with their Docker-in-Docker requirements)
be able to maintain and update the test matrix in OCaml.
The test matrix and default variables are in src/logic/model.ml
src/scripts has all the pieces that get assembled into a desktop/GitLab/GitHub job. Look at how opam_root and opam_root_cacheable can be different in both setup-dkml.sh and teardown-dkml.sh. If they are different, the opam root is transferred to a location where GitLab CI can do caching.
The GitLab templates are in tmpl/gl/. The desktop ones are in tmpl/pc/ if you want to test changes locally before trying on GitLab.
The rendered output is in test/gl/
There is an external script (described in the README.md) that copies and maintains the rendered output into your own project.
It doesn’t require you to use dkml-base-compiler. You can use the variable OCAML_COMPILER to change to a different OCaml compiler.
@silene If I understand correctly, the docker image is not cached using Gitlab caching mechanism, but instead pushed to the “container registry”. I guess it’s more complicated than what I’d hoped but it has the advantage of also “caching” the other packages that I would be installing.
@jbeckford If I’m being honest this looks a bit intimidating. And if I read correctly here it will take around 5 or so minutes in the best case? My current setup which installs all dependencies (but not opam or ocaml) every time takes around 8 minutes to run on the CI. I was hoping to bring it down to a few seconds like on my machine.
The Docker image build sounds great but docker push gets rejected every time.
$ docker push "$BUILD_IMAGE"
Using default tag: latest
The push refers to repository [docker.io/library/main-2024-07-27]
44b1eac140ca: Preparing
7dc7e325d84c: Preparing
154742bf41ad: Preparing
denied: requested access to the resource is denied
I’m surprised by the error message which suggests it’s not trying to push to registry.gitlab.inria.fr even though that’s what the variable contains and login succeeded.
I followed the instructions there but that didn’t help.
The main difference I see with why3 is that for me “Deploy” doesn’t contain a “Container Registry” tab. It might be to do with the fact that the repository is private?
EDIT: I see now the problem is that in addition to activating “Container Registry” from parameters, I also needed to make sure that the image name was of the form