Migrate documentation jobs to Cacio

What

Migrate documentation-related CI jobs to Cacio, in their own module (in ci/bin/documentation.ml).

Side-effects:

• move documentation jobs from schedule_extended_test to a new dedicated pipeline: documentation.daily
• rename schedule_documentation into documentation.update
• jobs renamed from documentation:* to documentation.*
• documentation.rst-check moved to the test stage (from sanity)
• jobs are no longer triggered if the following files change: .gitlab-ci.yml, .gitlab/ci/pipelines/before_merging.yml, .gitlab/ci/pipelines/merge_train.yml
• some jobs can no longer be triggered manually
• documentation:manuals now uses the static executables in documentation.daily (it did not in schedule_extended_test)

WARNING

After merging this MR, the schedule_documentation pipeline must be reconfigured in GitLab (set TZ_SCHEDULE_KIND to documentation.update), and a new scheduled pipeline must be created (with TZ_SCHEDULE_KIND set to documentation.daily).

Why

Ideally we will eventually migrate everything to Cacio, because it allows to define the CI of each component separately. The documentation is not really a component though (for now). But Cacio also provides guarantees that CIAO does not and enforces some conventions to make the CI more consistent. In particular, Cacio encourages each component to have their own dedicated scheduled pipelines instead of having only schedule_extended_test. In this MR we do that with documentation.daily.

Another reason is that the code for those jobs is quite spaghetti. The main declarations are in code_verification.ml, but also in master_branch.ml. To avoid completely duplicating the code, common parts are in common.ml, in submodule Documentation. The code in code_verification.ml is deep inside the jobs function, which is itself spaghetti because it aims to be usable for both before_merging / merge_train pipelines, and schedule_extended_tests pipelines. So it is parameterized by the pipeline type. It defines many subfunctions which depend on the pipeline type, and the jobs depend on those subfunctions, including jobs that are depended on by other jobs, such as documentation:manuals. The result is arguably a bit of a mess.

The reason schedule_documentation is renamed into documentation.update is that Cacio enforces the convention that scheduled pipelines are prefixed by the component name, followed by a period, i.e. documentation.something. Same reason for the jobs being renamed.

The reason documentation.rst_check is now in the test stage is that it is a test. See the documentation of type stage in cacio.mli.

The reason changes to .gitlab-ci.yml, .gitlab/ci/pipelines/before_merging.yml and .gitlab/ci/pipelines/merge_train.yml no longer trigger jobs is because we don't do that for other components such as Teztale and Grafazos. In theory, modifying the YAML files changes the definition of the jobs and thus we should test the jobs again, but:

• this is only true for .gitlab/ci/pipelines/before_merging.yml (and maybe merge_train.yml but it's usually a consequence of the former)
• most changes to those files are not related to the documentation, so it's a bit heavy to enforce this
• I don't think this is really necessary, if we know we are modifying the doc jobs we can tag the MR with ci--docs or change the relevant files to trigger a test
• rst-check cannot be triggered with tag ci--docs, but actually, if the RST files do not change, there is rarely a reason to re-check them (one reason could be a change of version of the checker)

This is debatable though. I'm ok to add those changes back if you think they are important.

The reason some jobs can no longer be triggered manually is that this is not supported by Cacio: either a job is always manual, or it is always automatic. We could implement the mixed strategy (automatic if file changed, manual otherwise), but one goal of Cacio is to make it so that if nothing changes, the pipeline is empty. The mixed strategy would go counter to this goal. Forcing specific jobs should be done with MR labels instead.

The reason documentation:manuals now uses the static executables is quite technical. It is explained in a comment in documentation.ml, line 135.

How

I have split the MR to migrate one job per commit. Because some jobs depend on others, I introduced dummy jobs to serve as placeholders for the dependencies. E.g. when migrating documentation:odoc, I replace its definition in CIAO with a placeholder so that other jobs defined in CIAO. Those placeholders are removed later in the MR.

The first two commits do not need placeholders. They could be merged separately. But I think having a state where some jobs are in documentation.ml and some are still in code_verification.ml et al. would be confusing. The other commits use placeholders that we don't want to have on master so they need to be merged all together Unfortunately this makes the MR a bit large.

The main work consists in un-spaghettifying / flattening the code by inlining the relevant definitions. I think the result is much simpler.

Manually testing the MR

make -C ci

Test pipelines:

• documentation.daily
• documentation.update: TODO but I don't want it to actually publish…

Checklist

• Document the interface of any function added or modified (see the coding guidelines)
• Document any change to the user interface, including configuration parameters (see node configuration)
• Provide automatic testing (see the testing guide).
• For new features and bug fixes, add an item in the appropriate changelog (docs/protocols/alpha.rst for the protocol and the environment, CHANGES.rst at the root of the repository for everything else).
• Select suitable reviewers using the Reviewers field below.
• Select as Assignee the next person who should take action on that MR