Support coqbot resume ci minimize ci-foo url

[JasonGross]

Both ci minimize ci-foo https://... and ci minimize ci-foo [description](url) are supported.

[JasonGross]

I think this will probably work for regular urls, and is probably worth merging rather than letting it bitrot. (I'm not sure when I'll next get to work on it)

For github artifact urls, I am running into the problem that

Lwt_main.run (Client.get ~headers:(Header.add (Header.init ()) "Authorization" "token github_pat_<...>") (Uri.of_string "https://api.github.com/repos/coq-community/run-coq-bug-minimizer/actions/artifacts/1199822634/zip"));;

gives

({Cohttp.Response.encoding = Cohttp__.Transfer.Fixed 0L; headers = <abstr>;
  version = `HTTP_1_1; status = `Found; flush = false},
 `Empty)

Any idea why I'm getting empty here, even though with curl -I I'm getting

HTTP/2 302
server: GitHub.com
date: Sun, 28 Jan 2024 03:12:22 GMT
content-type: text/html;charset=utf-8
content-length: 0
location: https://productionresultssa0.blob.core.windows.net/actions-results/31f870df-c0b7-436c-80db-f919addd7d93/workflow-job-run-ca395085-040a-526b-2ce8-bdc85f692774/artifacts/1906445c8ef92bb371515869f6160b65c9431a03596d43d49098d04d543bebe7.zip?rscd=attachment%3B+filename%3D%22tmp.v.zip%22&se=2024-01-28T03%3A22%3A22Z&sig=aDsCiEUUWmdNYUZiAf%2F6usA1MTj6RaPGWR3no66EmoA%3D&sp=r&spr=https&sr=b&st=2024-01-28T03%3A12%3A22Z&sv=2021-12-02
x-github-api-version-selected: 2022-11-28
x-ratelimit-limit: 5000
x-ratelimit-remaining: 4872
x-ratelimit-reset: 1706412997
x-ratelimit-used: 128
x-ratelimit-resource: core
access-control-expose-headers: ETag, Link, Location, Retry-After, X-GitHub-OTP, X-RateLimit-Limit, X-RateLimit-Remaining, X-RateLimit-Used, X-RateLimit-Resource, X-RateLimit-Reset, X-OAuth-Scopes, X-Accepted-OAuth-Scopes, X-Poll-Interval, X-GitHub-Media-Type, X-GitHub-SSO, X-GitHub-Request-Id, Deprecation, Sunset
access-control-allow-origin: *
strict-transport-security: max-age=31536000; includeSubdomains; preload
x-frame-options: deny
x-content-type-options: nosniff
x-xss-protection: 0
referrer-policy: origin-when-cross-origin, strict-origin-when-cross-origin
content-security-policy: default-src 'none'
vary: Accept-Encoding, Accept, X-Requested-With
x-github-request-id: C902:4040:8D1007:946B67:65B5C616

?

[JasonGross]

Ah, I guess this is a redirect

[JasonGross]

Now it works! coq/coq#18564 (comment)

[JasonGross]

I would like to merge this soon, any objections?

[Zimmi48]

Sorry for not being responsive here. In the future, feel free to merge such changes in the absence of response. Now, the PR did bitrot indeed. I didn't review it yet, but I should be available to do so during the summer if this is still relevant.

[JasonGross]

PR is rebased, and I'm deploying it here. I don't have much time free these days, so I'd like to get this merged before it bitrots again. I believe this functionality is still useful. (I had just forgotten to merge it back in Jan / March.)

[Zimmi48]

I only did a bird-eye review, but this looks good to me. Feel free to merge when you feel you have sufficiently tested this (up to you not to forget about it).
Note that I force-pushed to your branch, but that was only to apply autoformatting in two places where it had been forgotten.

[JasonGross]

coqbot seems to be responding fine to requests here, and I tested the "resume with artifact" way back when, so I'm going to merge this. I expect the new feature will work fine (trusting the past test), and if not, at least it hasn't broken anything else.

Some notes on usage:

• supported invocation is @coqbot resume ci minimize ci-foo [description](url) (what you get if you drag-and-drop an upload) and @coqbot resume ci minimize ci-foo url
• you can directly link to the artifacts of previous runs, such as the tmp.v file, and coqbot will unpack the artifact
• other links need to be to text files that are the buggy file (you can upload it as .txt or .v.txt or .log or w/e)
• plausibly in the future we can support non-artifact links to .zip files and .tar.gz files, etc; in the interim, I don't expect this to be a big issue