That works well, except that even if only a single source file is changed, the HTML pages of all the source files are regenerated and, since they are more than 1200 source files, that takes too much time (more than 15 minutes).
I then got help outside this forum from a guy (but who has no clue about sphinx-doc). Here is what he said:
[Y]ou are shooting yourself in your foot because you use make. make is utterly ineffective in CI pipelines because at the beginning of each pipeline the repo is cloned afresh, meaning the file modification dates of the source files are usually newer than the cached output files even if nothing did change. Because make only considers file modification dates/timestamps, make is definitely not helpful for the first invocation. The second invocation obviously behaves correctly because the first make invocation rebuilds all outputs.
So you can reduce this minimal example by removing make and simply calling sphinx-build. And the pipelines for this new repository also show that a cache is pulled at the beginning and uploaded at the end of the pipeline. So GitLab’s caching is working. It’s now a question of what sphinx-build needs to determine whether to rebuild. If it works like make, you are out of luck because of file timestamps. If it works with another mechanism, you should look up where that is stored and check that all information needed for the rebuild are cached (maybe more is needed than just the doctrees directory).
I told him that:
He answers then:
So you need to use one of the solutions modifying the file timestamps to match the git commits to have an effective solution here. There are a variety of tools out there that do this. Just search the internet for git checkouts with mtime preserved.