Refactor CI to run in fresh build box

[fdupress]

This refactors the CI jobs so compilation and checks (including external CI) run in a fresh build box. This will help ensure that changes to the box configuration (new dependencies, prover updates, prover additions, ...) are reflected quickly in the CI environment and can be leveraged in external proofs right away.

The workflow is now:

1. Build base and build boxes, then save them as an artefact;
2. Recover the build box, then run the compilation check;
3. Recover the build box, then compile EasyCrypt and run a matrix check; (this recompiles EC 3 times in parallel, and likely needs changed)
4. Recover the build box, then compile EasyCrypt and run the external matrix checks (this recompiles EC as many times as we have external checks, and likely needs changed)
5. Build the test box, push the base and build boxes (all pushes) and the test box (release branches and tags)

The nix compilation check is unchanged, notification fires after all succeed. Documentation is built as normal.

[fdupress]

OK. So this takes around the same time as the multiple workflows, but is much better in terms of actual checking.

Should I take the opportunity to try and avoid repeating work? I think we could:

1. Push the base and build boxes in phase 1 under a temporary tag (with short retention);
2. Build and push the test box in phase 2 (after compilation check with CI profile, rebuild with prod profile in the docker) under a temporary tag (with short retention);
3. Use the test box in phase 3 to avoid the multiple parallel recompilations of EC;
4. In phase 4, simply pull, retag, and push the appropriate boxes with the appropriate retention policy (indefinite for releases, attempting to keep only the latest for main).

The above would still have a minor race condition where we build the test box after the base and build boxes, so there could still be some small discrepancies in those environments if debian pushes some package updates between the two builds. I could also just build all 3 boxes in step 1 (4 if we keep the formosa images) before we check that compilation succeeds in the stricter CI profile.

[fdupress]

OK. So this takes around the same time as the multiple workflows, but is much better in terms of actual checking.

Should I take the opportunity to try and avoid repeating work? I think we could:

1. Push the base and build boxes in phase 1 under a temporary tag (with short retention);
2. Build and push the test box in phase 2 (after compilation check with CI profile, rebuild with prod profile in the docker) under a temporary tag (with short retention);
3. Use the test box in phase 3 to avoid the multiple parallel recompilations of EC;
4. In phase 4, simply pull, retag, and push the appropriate boxes with the appropriate retention policy (indefinite for releases, attempting to keep only the latest for main).

The above would still have a minor race condition where we build the test box after the base and build boxes, so there could still be some small discrepancies in those environments if debian pushes some package updates between the two builds. I could also just build all 3 boxes in step 1 (4 if we keep the formosa images) before we check that compilation succeeds in the stricter CI profile.

OK. So this takes around the same time as the multiple workflows, but is much better in terms of actual checking.

Should I take the opportunity to try and avoid repeating work? I think we could:

1. Push the base and build boxes in phase 1 under a temporary tag (with short retention);
2. Build and push the test box in phase 2 (after compilation check with CI profile, rebuild with prod profile in the docker) under a temporary tag (with short retention);
3. Use the test box in phase 3 to avoid the multiple parallel recompilations of EC;
4. In phase 4, simply pull, retag, and push the appropriate boxes with the appropriate retention policy (indefinite for releases, attempting to keep only the latest for main).

The above would still have a minor race condition where we build the test box after the base and build boxes, so there could still be some small discrepancies in those environments if debian pushes some package updates between the two builds. I could also just build all 3 boxes in step 1 (4 if we keep the formosa images) before we check that compilation succeeds in the stricter CI profile.

This is too much: the test Docker builds easycrypt from a git remote (via opam), which will not properly exist except in PR-related runs. Therefore, this should now be ready to review.