CI failures using docker-coq-action cause of debian download issues

[MSoegtropIMC]

Dear docker-coq-action Team,

since today we are getting in VST CI this error about the download of the debian base image:

2022-03-07T12:52:09.9644526Z Step 1/3 : FROM samueldebruyn/debian-git@sha256:6fda212f1f62ba382143c797d771dee1f4aa505520c277195de5536f2926309f
2022-03-07T12:52:10.0776585Z pull access denied for samueldebruyn/debian-git, repository does not exist or may require 'docker login': denied: requested access to the resource is denied
2022-03-07T12:52:10.0799707Z ##[warning]Docker build failed with exit code 1, back off 5.966 seconds before retry.
2022-03-07T12:52:16.0472437Z ##[command]/usr/bin/docker build -t 29a95e:708aac7d1e4e4619be905e3066757165 -f "/home/runner/work/_actions/textbook/git-checkout-submodule-action/2.1.1/Dockerfile" "/home/runner/work/_actions/textbook/git-checkout-submodule-action/2.1.1"
2022-03-07T12:52:16.0773999Z Sending build context to Docker daemon  7.168kB

I must say I don't understand how it comes to this and where the debian image is coded. Shouldn't docker-coq-action and coq-docker depend on (https://hub.docker.com/_/debian/)?

See: PrincetonUniversity/VST#550

[erikmd]

Hi @MSoegtropIMC
Thanks for the report, I'm going to have a look ASAP.

[erikmd]

Dear @MSoegtropIMC, Cc @andrew-appel,

This error was actually independent of docker-coq and docker-coq-action:

Looking from the GHA log you mentioned (https://github.com/PrincetonUniversity/VST/runs/5440552516), the issue comes earlier than the building of docker-coq-action, it is due to this step that handles git submodules, which should be replaced just like this earlier patch by @Zimmi48: coq-community/templates@042472f

[erikmd]

Apart from that, I have run again docker-coq-action's own CI tests in this PR:

• chore(GHA): Add cron job for {coq-demo.yml, python-demo.yml} #72
  and the docker-coq/docker-mathcomp tests were fine,
• but thanks to the issue you opened, just in case, I think it'll be useful to merge this PR so these docker-coq-action CI tests are run every day (not just at docker-coq-action release time), using a GHA cron job.

[erikmd]

Incidentally, as mentioned by @MSoegtropIMC, all coqorg/coq:… images currently rely on debian:10-slim (oldstable):
https://github.com/coq-community/docker-base/blob/1b79d55eb610d7841c9ffc905839b385192115ca/base/single/Dockerfile#L1
and it could be nice to plan to switch to debian:11-slim (stable) anytime soon.

Of course, this bump is not trivial as it could cause breaking issues for Coq projects that install specific Debian packages.
(Maybe @Zimmi48, we could discuss this issue the next time we have a docker-coq-action meeting!)

In the meantime @MSoegtropIMC @andrew-appel, do you think BTW some of your CI workflows would be negatively impacted by one such Debian version bump?

[MSoegtropIMC]

@erikmd : thanks for your analysis - I will follow up in VST CI.

Regarding a debian change: I would say as long as OCaml runs we are fine. There have been recent issues with OCaml and recent Ubuntu - I guess Debian might be similar - but these have been fixed and back ported down to OCaml 4.10.X. So I don't expect any issues.

[Zimmi48]

FTR, there were a couple of PRs from our side applying this patch in VST's CI:

• Change the way submodules are fetched to fix CI. PrincetonUniversity/VST#535
• Fix CI PrincetonUniversity/VST#533

But at the time, it wasn't sufficient to fix all the issues that existed.

[MSoegtropIMC]

@erikmd , @Zimmi48 : thanks again for the analysis! As it turns out the issue is because Andrew used an outdated workflow file in a working branch. I assume that updating the workflow file with the VST master version will fix this.

I will close this issue.