github: fix timestamp and request HEAD

[axel-h]

use %M (minute 00..59) instead of %I (hour 01..12)

[lsf37]

I have no idea what format the Debian time stamps are, I just used existing code, but it looks like you are right. Have you seen this fail and checked that the new version works?

If we change it, we should change all occurrences. There is at least one in the PR workflow, but possibly also something in build scripts.

[axel-h]

I've not seen it fail, I was just wondering about the format and looked up the params. And tried to find an official source suggesting using this format string. I'm not sure if using %I will ever fail, as curl is used to get the right URL anyway - which will be whatever the server sends us and it may gracefully correct timstamps in the future. Where did you copy this string from, github code search does not give me any matches and google also does not give much.

[lsf37]

It's from @LukeMondy's Bamboo deployment script, which is fairly old. You're right that I doesn't make much sense in that position, I'll try it out with M and see what happens.

[LukeMondy]

It does indeed look like a bug, though MacOS date and Linux date are quite different from memory, so maybe it's related to that.

Despite being a bug, it is unlikely to have had much impact - the url_effective part is the magic - Debian snapshot allow you to put in any timestamp, and their server will resolve your request to the closest snapshot earlier than your requested date, returning a 301 with the real URL. The url_effective curl command does that ahead of time, so we get a concrete snapshot date. This thread talks about it a bit: https://www.mail-archive.com/debian-snapshot@lists.debian.org/msg00411.html and has a fancier one-liner too ;)

Anyway, the only time this would be an impact is when Debian snapshot released a snapshot, and the mismatch in minutes caused us to miss the new snapshot. Once the next hour rolls around, it would get the lastest one.

So in summary, probably not a huge deal, but as Michael Sproul once said to me: "We have a name for edge cases in Formal Verification: we call them 'cases'", so worth fixing :)

[lsf37]

Cool, thanks for the background! Will have a go at the fix.

[axel-h]

The linter still complains, but I can't make sense of the error. Seem it compares a branch with itself and then complans

[axel-h]

Adding a commit that uses "-I" to request HEAD instead of GET. Local test works:

$ curl -v -ILs -o /dev/null -w %{url_effective} http://snapshot.debian.org/archive/debian/$(date -u +%Y%m%dT%H%M00Z)/

*   Trying 193.62.202.27:80...
[...]
> HEAD /archive/debian/20220705T102800Z/ HTTP/1.1
[...]
< HTTP/1.1 301 Moved Permanently
[...]
< Location: http://snapshot.debian.org/archive/debian/20220705T084757Z/
[...]
* Issue another request to this URL: 'http://snapshot.debian.org/archive/debian/20220705T084757Z/'
[...]
> HEAD /archive/debian/20220705T084757Z/ HTTP/1.1
[...]
< HTTP/1.1 200 OK
[...]
http://snapshot.debian.org/archive/debian/20220705T084757Z/

[lsf37]

The linter still complains, but I can't make sense of the error. Seem it compares a branch with itself and then complans

There is a lot that doesn't make sense to me in that error message. It's saying GITHUB_SHA is 653c2913b91c07ba9020dbbde51ca100cd92fb40 which doesn't seem to exist anywhere, it then wants to compare master with 794dfef8b65dab002c0302d63649fdfcbfbb22f4 which looks like the merge commit, but also doesn't seem to exist in the local copy it checked out.

The action did work recently in another PR, so it might be related with it running from a fork, although it shouldn't need any privileges.

It's not one of our standard actions and predates the rest of our GitHub actions setup, so we could think about just removing it. I've left it in so far, because it has linters for things that are more relevant in this repo than others (specifically docker and bash). Maybe it's easier to run these directly.

Edit: aha! 653c2913b91c07ba9020dbbde51ca100cd92fb40 does exist (the GH UI links it), but you wouldn't get it if you cloned the repo, because it's not connected. Could be that there was a force push while the action was running.

[lsf37]

Ok, one difference I can see to the examples in the super-linter docs is that they use the checkout action v3, whereas we use v2. That might lead to unexpected results. I'll put up a PR that bumps that.

[axel-h]

Ok, checked it locally here as well and it works, so happy with that. If you change the occurrence in .github/workflows/docker-build.yml as well, we can merge this.

done

[axel-h]

Edit: aha! 653c291 does exist (the GH UI links it), but you wouldn't get it if you cloned the repo, because it's not connected. Could be that there was a force push while the action was running.

Ah yes, that could have been the case. I had to fix a typo in the commit message.

[axel-h]

I'm not quite sure why the build fails.

Step 1/15 : ARG BASE_BUILDER_IMG=trustworthysystems/prebuild-cakeml
Step 2/15 : ARG BASE_IMG=trustworthysystems/sel4
Step 3/15 : FROM $BASE_BUILDER_IMG as builder
Get "https://registry-1.docker.io/v2/": EOF
Error: Process completed with exit code 1.

Seems it could not load trustworthysystems/prebuild-cakeml, because the name is trustworthysystems/prebuild_cakeml (underscore instead of minus), see https://hub.docker.com/r/trustworthysystems/prebuilt_cakeml

EDIT: NO, I'm wrong,prebuild_cakeml is passed on the command line that is supposed to overwwrite the default. Seems it's just the request to https://registry-1.docker.io/v2/ failing. When I try locally it get a HTTP/1.1 401 Unauthorized and {"errors":[{"code":"UNAUTHORIZED","message":"authentication required","detail":null}]} there.

There is another unrelated odd thing, looking at the command docker build --force-rm=true --build-arg BASE_IMG=debian:bullseye-20210816-slim --build-arg SCM= --build-arg SNAPSHOT_DATE= -f dockerfiles/base_tools.Dockerfile -t base_tools . I wonder if SNAPSHOT_DATE should have a value here?

[lsf37]

I wonder if SNAPSHOT_DATE should have a value here?

Indeed, yes, it should. I don't think it's the cause for this specific failure (might have been just a network fluke), because it has worked fine in the past, but we should definitely fix it. The culprit is likely the missing | in the run action that sets the variable in docker-build.yml:

     - name: Set SNAPSHOT_DATE
-      run:
+      run: |

I fixed this recently in docker-deploy.yml, but forgot that there is another occurrence here.

Happy for you to tuck on a commit with that to this PR if you want.

[axel-h]

Indeed, yes, it should. I don't think it's the cause for this specific failure (might have been just a network fluke), because it has worked fine in the past, but we should definitely fix it. The culprit is likely the missing | in the run action that sets the variable in docker-build.yml: [...] I fixed this recently in docker-deploy.yml, but forgot that there is another occurrence here. Happy for you to tuck on a commit with that to this PR if you want.

Added a commit that applies the same change in docker-build.yml.

[lsf37]

The linter seems to work now, so #52 was a success!

[axel-h]

We have SNAPSHOT_DATE now set properly, logs say: docker build --force-rm=true --build-arg BASE_IMG=debian:bullseye-20210816-slim --build-arg SCM= --build-arg SNAPSHOT_DATE=20220706T150041Z -f dockerfiles/base_tools.Dockerfile -t base_tools .

[axel-h]

Good to merge now?