Allow CI to run on old branches

[saraedum]

CircleCI and GitLab CI currently both build-from-latest using sagemath/sagemath-dev:develop. This leads to annoying errors when building from older branches as the build process won't find the commit that sagemath-dev:develop was built from in that branch.

Instead, we should build from sagemath-dev:latest-tag-in-branch, so currently we would build from sagemath-dev:8.4.rc0 for new branches but also branches based on older states of the repository would still work. In particular, the build is more reproducible. Rerunning a build later, does not try to build from a different base build.

[saraedum]

I have not tested whether all the relevant combinations work yet.

---

New commits:

​28c48df

Allow CI to run on old branches

[embray]

I have been getting bitten by this and it's confusing. That said, I wonder if this is really a good idea. For unmerged tickets we really want to make sure they work against the latest develop branch. Instead I think we should try to apply the ticket on top of the current develop.

Maybe that's what you're doing as well too; I might be missing something. I don't think there's much value in doing builds against old tags.

[embray]

E.g. If the last commit in the old branch is older than the current develop, then it should try automatically to rebase the branch on the newest develop, or merge it, and if there are merge conflicts then it should refuse to run the rest of the pipeline (on GitHub for example it generally won't run CI services if a PR has merge conflicts with the current master branch IIUC).

[saraedum]

In principle I think you are right. But I have a feeling that this is going to cause quite some headaches if I think about typical reruns that we trigger manually. Say, I found out that an old tag did not build and push to docker hub. Now I click "retry" and it will actually merge in the latest develop and build that :(

So, there is ways to find out, and say, do not merge when you are on a tag. But maybe that's just adding too much complexity.

There's a reasonable message in the build log I think. Could not find commit cat docker/.commit in your local Git history. Please merge in the latest built develop branch to fix this: git fetch trac && git merge cat docker/.commit`. I think I'd just leave this alone.