The plan is to keep Travis for a short while, until we are confident that
GitHub Actions work well enough for us. And after that we can remove Travis
entirely.
There is a bunch of duplicated things but it allows us to maximize
parallelismt to have results as soon as possible.
API documentation generation is still missing.
Adrien Crivelli