[Feature] mirroring to inria gitlab

@j-l-s @srcansiz hi, it would be nice (and safe) to set up a gitlab mirror of our current devs on github:
- by this I mean mirroring *from* github *towards* Inria gitlab
- this is know as a *pull mirror* on gitlab side
- the mirror is intended just for backup, no need to have a full / two way sync
- mirroring the main branch only is fine (no other branches, no issues / discussion, no wikis...)

The official gitlab doc is [here](https://docs.gitlab.com/user/project/repository/mirror/pull/) but, when I take a look at what they say, I typically only see the `push` option for mirrors, not the `pull`. This can also be set up with github CI, as explained [here](https://dev.to/brunorobert/github-and-gitlab-sync-44mn).

Last but not least: IIRC, @nniclausse had a look at that. (possible issue: he might have written the action in erlang 🫢) Nicolas ?