[CI] use container instead of chroot for Debian

[JasonGross]

Passing GITHUB_STEP_SUMMARY="$GITHUB_STEP_SUMMARY" through to the chroot was not working, so let's try using a container instead

[andres-erbsen]

Can you point me to what was not working?

[JasonGross]

Look at the failing debian CI before https://github.com/mit-plv/fiat-crypto/commit/6bce0ff7b316874b4706cc3de066a46364791ce6, where I reverted the change that broke things. GitHub Actions defines GITHUB_STEP_SUMMARY (per step, I think) but the chroot doesn't seem to know about it

[JasonGross]

Look at the failing debian CI before 6bce0ff, where I reverted the change that broke things. GitHub Actions defines GITHUB_STEP_SUMMARY (per step, I think) but the chroot doesn't seem to know about it

Here it says

id -u
+ id -g
+ pwd
+ exec sudo chroot /chroot setpriv --reuid 1001 --regid 127 --init-groups /bin/sh -e -u -x -c cd "$1"; shift; exec sh -e -u -x "$@" -- /home/runner/work/fiat-crypto/fiat-crypto /home/runner/work/_temp/6cba05fe-d649-48be-a360-34765f85caa5
+ cd /home/runner/work/fiat-crypto/fiat-crypto
+ shift
+ exec sh -e -u -x /home/runner/work/_temp/6cba05fe-d649-48be-a360-34765f85caa5
/home/runner/work/_temp/6cba05fe-d649-48be-a360-34765f85caa5: 1: GITHUB_STEP_SUMMARY: parameter not set

[andres-erbsen]

Could you please point me to the code where you tried to set the variable inside the chroot? I would like to go back to that setup and I don't think it would be hard to fix.

[andres-erbsen]

Oh, is https://github.com/mit-plv/fiat-crypto/commit/6bce0ff7b316874b4706cc3de066a46364791ce6#diff-66eee238a3c2480cc0fb962e08ff6a6b91570e9944ab4058a7ed9fe5cff62360L42 the code? That does not work because the rhs is evaluated inside chroot as well, failing because the variable is unset there. See here for how it works in the alpine script -- I am not sure passing through all the variables is great, which is why I didn't imitate it, but if we could pass just the ci-script-derived ones that would be good. (Does github actions stash them in some file already?) Or we could just imitate that.

[andres-erbsen]

(As I have just confirmed, it's not chroot that messes with the env anyway, it's sudo)

[JasonGross]

Oh, is 6bce0ff#diff-66eee238a3c2480cc0fb962e08ff6a6b91570e9944ab4058a7ed9fe5cff62360L42 the code?

Yes

That does not work because the rhs is evaluated inside chroot as well, failing because the variable is unset there. See here for how it works in the alpine script

Ah, I see

I am not sure passing through all the variables is great, which is why I didn't imitate it, but if we could pass just the ci-script-derived ones that would be good.

Sure, I'm happy to revert this in favor of the chroot solution. Do you have a preference for chroot over docker container?

Does github actions stash them in some file already?

Yes, the file name is stored in $GITHUB_ENV

[andres-erbsen]

Do you have a preference for chroot over docker container?

Yes. When chroot goes wrong, I have some idea of how to troubleshoot it.