Migrate to GitLab

To do

Study feasibility of adapting mike to GitLab Pages
Set up CI on GitLab
Turn off mirroring from this repo to the GitLab one
Update helpers/draft-release.sh and docs via commit in GitLab repo to point to gitlab.com/gitlab.io instead of github.com/github.io
- grep 2>|/dev/null -il github * */* for places to look
Set up reverse mirroring or replace this repo with a link to the GitLab one

I don't presume to know your motivations, but FWIW here's my experience in moving in the other direction:

I started on GitLab for the somewhat petty reason that GitLab's wiki has built-in support for inline LaTeX, and GitHub's wiki does not.
I decided to move to GitHub because it seems there is more action here. Furthermore, I've been increasingly using JupyterLite, which is poised to take over much of what I used wiki pages for (including LaTeX).
I'd say GitLab's CI configuration is simpler overall than GitHub's. On the other hand, I personally prefer the GitHub Actions UX.

Thanks so much for the insight! My motivations were mainly to move away from Microsoft, but I'm not sure how important that is at this point. It's certainly not a priority, so maybe it's best to close this and reopen it if/when it emerges as worthwhile. Thanks again for the input on your own transition, though! It definitely helps.