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?