Status update bot

Stream: nightly-testing

[Ruben Van de Velde]

The Update the nightly-testing-YYYY-MM-DD branch fails (as far as I can tell) at the curl invocation if the tag doesn't exist yet:

/home/runner/work/_temp/609b384d-ec77-4109-86b3-6dfb93bb97f1.sh: line 14: ***: command not found
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100    52  100    52    0     0    148      0 --:--:-- --:--:-- --:--:--   148
100    52  100    52    0     0    148      0 --:--:-- --:--:-- --:--:--   148
Creating tag nightly-testing-2024-04-09 from the current state of the nightly-testing branch.{"code":405,"message":"HTTP 405 Method Not Allowed"}

https://github.com/leanprover-community/mathlib4/actions/runs/8615325483/job/23610624487

and Fetch lean-toolchain from latest bump branch fails because the commit reference seems to be empty.
https://github.com/leanprover-community/mathlib4/actions/runs/8613013146/job/23603458087

The first failure also blocks the zulip message

[Ruben Van de Velde]

I tried to debug but realized this action uses the script from the master branch

[Joachim Breitner]

One problem is probably a missing quote, it should be

curl -X POST "http://speed.lean-fro.org/mathlib4/api/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"

as the secret contains characters worth escaping. Will put that into an (necessarily untested) PR at https://github.com/leanprover-community/mathlib4/pull/12038

[Joachim Breitner]

Do you want to merge it to hopefully unbreak the workflow, or are there more issues lurking?

[Ruben Van de Velde]

Huh, I thought I put it on the maintainer queue. Anyway, it's in bors's hands now

[Ruben Van de Velde]

We'll see if it works in production :)

[Joachim Breitner]

That's the spirit :-D

[Joachim Breitner]

I'm not always monitoring this, so feel free to ping me if more work is needed.

[Ruben Van de Velde]

(We'll only be able to see if it worked once the 2024-04-10 nightly is out)

[Ruben Van de Velde]

Joachim Breitner said:

I'm not always monitoring this, so feel free to ping me if more work is needed.

Something has improved in https://github.com/leanprover-community/mathlib4/actions/runs/8645841052/job/23703844328 in that it's no longer marked as a failure (compare https://github.com/leanprover-community/mathlib4/actions/runs/8615325483/job/23610624487), but it still prints {"code":405,"message":"HTTP 405 Method Not Allowed"}. Any chance you can see why it's returning that?

[Joachim Breitner]

Strange. With the wrong key, I get 401 Unauthorized. And with empty $hash I get 404.
Ah, simply wrong URL. Should be api/queue/commit. Do you want to make that change, I am about to go.

[Ruben Van de Velde]

Ha, sure

[Ruben Van de Velde]

Ruben Van de Velde said:

and Fetch lean-toolchain from latest bump branch fails because the commit reference seems to be empty.
https://github.com/leanprover-community/mathlib4/actions/runs/8613013146/job/23603458087

I think this was caused by the bane of every careless github api user: pagination. #12072 up for review

[Ruben Van de Velde]

Never make changes after testing your code or you look like a numpty. A review for #12081, please?

[Ruben Van de Velde]

AI generated code isn't replacing us yet: #12085