From 49e6613f21be70f13a1dec100abe8f8f231b33e9 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 11:12:15 -0800
Subject: [PATCH 01/13] Support `coqbot resume ci minimize ci-foo url`

Both `ci minimize ci-foo https://...` and `ci minimize ci-foo
[description](url)` are supported.
---
 src/actions.ml  | 47 +++++++++++++++++---------------
 src/actions.mli |  2 +-
 src/bot.ml      | 72 +++++++++++++++++++++++++++++++++++++++----------
 src/helpers.ml  | 41 ++++++++++++++++++++++++++++
 src/helpers.mli |  4 +++
 5 files changed, 129 insertions(+), 37 deletions(-)

diff --git a/src/actions.ml b/src/actions.ml
index 280adb98..87b50e14 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -732,20 +732,27 @@ type ci_minimization_info =
   ; failing_urls: string
   ; passing_urls: string }
 
+type coqbot_minimize_script_data =
+  | MinimizeScript of {quote_kind: string; body: string}
+  | MinimizeAttachment of {description: string; url: string}
+
 let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
-    ~base ~head ~ci_minimization_infos ~bug_file_contents
-    ~minimizer_extra_arguments =
+    ~base ~head ~ci_minimization_infos ~bug_file ~minimizer_extra_arguments =
   (* for convenience of control flow, we always create the temporary
      file, but we only pass in the file name if the bug file contents
      is non-None *)
   Lwt_io.with_temp_file (fun (bug_file_name, bug_file_ch) ->
-      Lwt_io.write bug_file_ch (Option.value ~default:"" bug_file_contents)
+      ( match bug_file with
+      | None ->
+          Lwt.return_unit
+      | Some (MinimizeScript {body= bug_file_contents}) ->
+          Lwt_io.write bug_file_ch bug_file_contents
+      | Some (MinimizeAttachment {url}) ->
+          download_to ~uri:(Uri.of_string url) bug_file_ch )
       >>= fun () ->
       Lwt_io.flush bug_file_ch
       >>= fun () ->
-      let bug_file_name =
-        Option.map ~f:(fun _ -> bug_file_name) bug_file_contents
-      in
+      let bug_file_name = Option.map ~f:(fun _ -> bug_file_name) bug_file in
       Lwt_list.map_s
         (fun {target; opam_switch; failing_urls; passing_urls; docker_image} ->
           git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo
@@ -1200,8 +1207,8 @@ let accumulate_extra_minimizer_arguments options =
   >>= fun inline_stdlib_args -> inline_stdlib_args @ extra_args |> Lwt.return
 
 let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
-    ~head_pipeline_summary ~request ~comment_on_error ~bug_file_contents
-    ~options ?base_sha ?head_sha () =
+    ~head_pipeline_summary ~request ~comment_on_error ~bug_file ~options
+    ?base_sha ?head_sha () =
   let options = format_options_for_getopts options in
   accumulate_extra_minimizer_arguments options
   >>= fun minimizer_extra_arguments ->
@@ -1297,7 +1304,7 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
       run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo
         ~pr_number:(Int.to_string pr_number) ~base ~head
         ~ci_minimization_infos:jobs_to_minimize ~minimizer_extra_arguments
-        ~bug_file_contents
+        ~bug_file
       >>= fun (jobs_minimized, jobs_that_could_not_be_minimized) ->
       let pluralize word ?plural ls =
         match (ls, plural) with
@@ -1452,8 +1459,7 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
               f
                 "I am now %s minimization at commit %s on %s. I'll come back \
                  to you with the results once it's done.%s"
-                ( if Option.is_none bug_file_contents then "running"
-                else "resuming" )
+                (if Option.is_none bug_file then "running" else "resuming")
                 head
                 (jobs_minimized |> String.concat ~sep:", ")
                 note_some_head_unfinished_msg )
@@ -1560,8 +1566,7 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
                 "I am now %s minimization at commit %s on requested %s %s. \
                  I'll come back to you with the results once it's done.%s\n\n\
                  %s"
-                ( if Option.is_none bug_file_contents then "running"
-                else "resuming" )
+                (if Option.is_none bug_file then "running" else "resuming")
                 head
                 (pluralize "target" successful_requests)
                 (successful_requests |> String.concat ~sep:", ")
@@ -1751,7 +1756,7 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
         pr_number err
 
 let ci_minimize ~bot_info ~comment_info ~requests ~comment_on_error ~options
-    ~bug_file_contents =
+    ~bug_file =
   minimize_failed_tests ~bot_info ~owner:comment_info.issue.issue.owner
     ~repo:comment_info.issue.issue.repo ~pr_number:comment_info.issue.number
     ~head_pipeline_summary:None
@@ -1763,7 +1768,7 @@ let ci_minimize ~bot_info ~comment_info ~requests ~comment_on_error ~options
           RequestAll
       | requests ->
           RequestExplicit requests )
-    ~comment_on_error ~options ~bug_file_contents ()
+    ~comment_on_error ~options ~bug_file ()
 
 let pipeline_action ~bot_info ({common_info= {http_repo_url}} as pipeline_info)
     ~gitlab_mapping : unit Lwt.t =
@@ -1890,17 +1895,12 @@ let pipeline_action ~bot_info ({common_info= {http_repo_url}} as pipeline_info)
                       minimize_failed_tests ~bot_info ~owner:gh_owner
                         ~repo:gh_repo ~pr_number
                         ~head_pipeline_summary:(Some summary) ~request:Auto
-                        ~comment_on_error:false ~options:""
-                        ~bug_file_contents:None
+                        ~comment_on_error:false ~options:"" ~bug_file:None
                         ?base_sha:pipeline_info.common_info.base_commit
                         ~head_sha:pipeline_info.common_info.head_commit ()
                   | _ ->
                       Lwt.return_unit ) ) ) )
 
-type coqbot_minimize_script_data =
-  | MinimizeScript of {quote_kind: string; body: string}
-  | MinimizeAttachment of {description: string; url: string}
-
 let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
     ~owner ~repo ~options =
   let options = format_options_for_getopts options in
@@ -2028,7 +2028,10 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
                         ; passing_urls
                         ; docker_image
                         ; full_target= target (* dummy value *) } ]
-                    ~bug_file_contents:(Some bug_file_contents) )
+                    ~bug_file:
+                      (Some
+                         (MinimizeScript
+                            {quote_kind= ""; body= bug_file_contents} ) ) )
                >>= function
                | [], [] ->
                    Lwt_io.printlf
diff --git a/src/actions.mli b/src/actions.mli
index 7630d62f..578204dc 100644
--- a/src/actions.mli
+++ b/src/actions.mli
@@ -103,7 +103,7 @@ val ci_minimize :
   -> requests:string list
   -> comment_on_error:bool
   -> options:string
-  -> bug_file_contents:string option
+  -> bug_file:coqbot_minimize_script_data option
   -> unit Lwt.t
 
 val coq_bug_minimizer_resume_ci_minimization_action :
diff --git a/src/bot.ml b/src/bot.ml
index 95e7ed28..4b557eb0 100644
--- a/src/bot.ml
+++ b/src/bot.ml
@@ -54,6 +54,11 @@ let callback _conn req body =
       |> Str.split (Str.regexp_string "\n```")
       |> List.hd |> Option.value ~default:""
     in
+    let extract_minimize_script quote_kind body =
+      MinimizeScript
+        { quote_kind= quote_kind |> Str.global_replace (Str.regexp "[ \r]") ""
+        ; body= body |> extract_minimize_file }
+    in
     let parse_minimiation_requests requests =
       requests
       |> Str.global_replace (Str.regexp "[ ,]+") " "
@@ -81,12 +86,7 @@ let callback _conn req body =
           , Str.matched_group 2 body
           , Str.matched_group 3 body )
         in
-        Some
-          ( options
-          , MinimizeScript
-              { quote_kind=
-                  quote_kind |> Str.global_replace (Str.regexp "[ \r]") ""
-              ; body= body |> extract_minimize_file } )
+        Some (options, extract_minimize_script quote_kind body)
       else if
         string_match
           ~regexp:
@@ -125,14 +125,59 @@ let callback _conn req body =
                 "@%s:?\\( [^\n\
                  ]*\\)\\bresume [Cc][Ii][- ][Mm]inimiz\\(e\\|ation\\):?\\([^\n\
                  ]*\\)\n\
-                 +```[^\n\
-                 ]*\n\
+                 +```\\([^\n\
+                 ]*\\)\n\
                  \\(\\(.\\|\n\
                  \\)+\\)"
             @@ Str.quote github_bot_name )
           body
       then
-        let options, requests, body =
+        let options, requests, quote_kind, body =
+          ( Str.matched_group 1 body
+          , Str.matched_group 3 body
+          , Str.matched_group 4 body
+          , Str.matched_group 5 body )
+        in
+        Some
+          ( options
+          , requests |> parse_minimiation_requests
+          , extract_minimize_script quote_kind body )
+      else if
+        string_match
+          ~regexp:
+            ( f
+                "@%s:?\\( [^\n\
+                 ]*\\)\\bresume [Cc][Ii][- ][Mm]inimiz\\(e\\|ation\\):?[ \n\
+                 ]+\\([^ \n\
+                 ]+\\)[ \n\
+                 ]+\\[\\([^]]*\\)\\] *(\\([^)]*\\))"
+            @@ Str.quote github_bot_name )
+          body
+      then
+        let options, requests, description, url =
+          ( Str.matched_group 1 body
+          , Str.matched_group 3 body
+          , Str.matched_group 4 body
+          , Str.matched_group 5 body )
+        in
+        Some
+          ( options
+          , requests |> parse_minimiation_requests
+          , MinimizeAttachment {description; url} )
+      else if
+        string_match
+          ~regexp:
+            ( f
+                "@%s:?\\( [^\n\
+                 ]*\\)\\bresume [Cc][Ii][- ][Mm]inimiz\\(e\\|ation\\):?[ \n\
+                 ]+\\([^ \n\
+                 ]+\\)[ \n\
+                 ]+\\(https?://[^ \n\
+                 ]+\\)"
+            @@ Str.quote github_bot_name )
+          body
+      then
+        let options, requests, url =
           ( Str.matched_group 1 body
           , Str.matched_group 3 body
           , Str.matched_group 4 body )
@@ -140,7 +185,7 @@ let callback _conn req body =
         Some
           ( options
           , requests |> parse_minimiation_requests
-          , body |> extract_minimize_file )
+          , MinimizeAttachment {description= ""; url} )
       else None
     in
     ( coqbot_minimize_text_of_body
@@ -363,14 +408,14 @@ let callback _conn req body =
                don't want to parse "resume" as an option, we test
                resumption first *)
             match coqbot_resume_ci_minimize_text_of_body body with
-            | Some (options, requests, bug_file_contents) ->
+            | Some (options, requests, bug_file) ->
                 (fun () ->
                   init_git_bare_repository ~bot_info
                   >>= fun () ->
                   action_as_github_app ~bot_info ~key ~app_id
                     ~owner:comment_info.issue.issue.owner
                     (ci_minimize ~comment_info ~requests ~comment_on_error:true
-                       ~options ~bug_file_contents:(Some bug_file_contents) ) )
+                       ~options ~bug_file:(Some bug_file) ) )
                 |> Lwt.async ;
                 Server.respond_string ~status:`OK
                   ~body:"Handling CI minimization resumption." ()
@@ -383,8 +428,7 @@ let callback _conn req body =
                     action_as_github_app ~bot_info ~key ~app_id
                       ~owner:comment_info.issue.issue.owner
                       (ci_minimize ~comment_info ~requests
-                         ~comment_on_error:true ~options ~bug_file_contents:None )
-                    )
+                         ~comment_on_error:true ~options ~bug_file:None ) )
                   |> Lwt.async ;
                   Server.respond_string ~status:`OK
                     ~body:"Handling CI minimization." ()
diff --git a/src/helpers.ml b/src/helpers.ml
index 4ac155fc..4c0ca0f2 100644
--- a/src/helpers.ml
+++ b/src/helpers.ml
@@ -1,4 +1,8 @@
 open Base
+open Lwt.Syntax
+open Cohttp
+open Cohttp_lwt
+open Cohttp_lwt_unix
 
 let f = Printf.sprintf
 
@@ -131,3 +135,40 @@ let github_repo_of_gitlab_url ~gitlab_mapping ~http_repo_url =
   |> Result.map ~f:(fun (gitlab_domain, gitlab_repo_full_name) ->
          github_repo_of_gitlab_project_path ~gitlab_mapping ~gitlab_domain
            ~gitlab_repo_full_name )
+
+let download_cps ~uri ~with_file =
+  let rec inner_download uri =
+    let* resp, body = Client.get uri in
+    match Response.status resp with
+    | `OK ->
+        let stream = Body.to_stream body in
+        with_file (fun chan -> Lwt_stream.iter_s (Lwt_io.write chan) stream)
+    | `Moved_permanently
+    | `Found
+    | `See_other
+    | `Temporary_redirect
+    | `Permanent_redirect -> (
+      match Header.get_location (Response.headers resp) with
+      | Some new_uri ->
+          inner_download new_uri
+      | None ->
+          let msg =
+            Printf.sprintf "Redirected from %s, but no Location header found"
+              (Uri.to_string uri)
+          in
+          Lwt.fail_with msg )
+    | status_code ->
+        let msg =
+          Printf.sprintf "HTTP request to %s failed with status code: %s"
+            (Uri.to_string uri)
+            (Code.string_of_status status_code)
+        in
+        Lwt.fail_with msg
+  in
+  inner_download uri
+
+let download ~uri dest =
+  download_cps ~uri ~with_file:(Lwt_io.with_file ~mode:Lwt_io.output dest)
+
+let download_to ~uri chan =
+  download_cps ~uri ~with_file:(fun write_to -> write_to chan)
diff --git a/src/helpers.mli b/src/helpers.mli
index c3a32fb8..9f5e988b 100644
--- a/src/helpers.mli
+++ b/src/helpers.mli
@@ -35,3 +35,7 @@ val github_repo_of_gitlab_url :
      gitlab_mapping:(string, string) Base.Hashtbl.t
   -> http_repo_url:string
   -> (string * string, string) result
+
+val download : uri:Uri.t -> string -> unit Lwt.t
+
+val download_to : uri:Uri.t -> Lwt_io.output_channel -> unit Lwt.t

From 20a8d1b62d0dfc89a7cfc8cc090bf2f586b88bff Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 11:23:00 -0800
Subject: [PATCH 02/13] Strip out leading and trailing ticks from url
 description

---
 src/bot.ml | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/bot.ml b/src/bot.ml
index 4b557eb0..bfd768e4 100644
--- a/src/bot.ml
+++ b/src/bot.ml
@@ -59,6 +59,12 @@ let callback _conn req body =
         { quote_kind= quote_kind |> Str.global_replace (Str.regexp "[ \r]") ""
         ; body= body |> extract_minimize_file }
     in
+    let extract_minimize_url url =
+      url |> Str.global_replace (Str.regexp "^[` ]+\\|[` ]+$") ""
+    in
+    let extract_minimize_attachment ?(description = "") url =
+      MinimizeAttachment {description; url= url |> extract_minimize_url}
+    in
     let parse_minimiation_requests requests =
       requests
       |> Str.global_replace (Str.regexp "[ ,]+") " "
@@ -100,7 +106,7 @@ let callback _conn req body =
           , Str.matched_group 2 body
           , Str.matched_group 3 body )
         in
-        Some (options, MinimizeAttachment {description; url})
+        Some (options, extract_minimize_attachment ~description url)
       else None
     in
     let coqbot_ci_minimize_text_of_body body =
@@ -163,7 +169,7 @@ let callback _conn req body =
         Some
           ( options
           , requests |> parse_minimiation_requests
-          , MinimizeAttachment {description; url} )
+          , extract_minimize_attachment ~description url )
       else if
         string_match
           ~regexp:
@@ -185,7 +191,7 @@ let callback _conn req body =
         Some
           ( options
           , requests |> parse_minimiation_requests
-          , MinimizeAttachment {description= ""; url} )
+          , extract_minimize_attachment url )
       else None
     in
     ( coqbot_minimize_text_of_body

From fdee297effd7a095ceaf02564cc355f032eb8e2e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 15:28:25 -0800
Subject: [PATCH 03/13] Fix support for url-based resumption via github api

---
 bot-components/GitHub_queries.ml  |   6 +
 bot-components/GitHub_queries.mli |   7 +
 bot-components/Utils.ml           |  32 +
 bot-components/Utils.mli          |   9 +
 bot-components/dune               |   4 +-
 src/actions.ml                    | 958 +++++++++++++++++-------------
 6 files changed, 595 insertions(+), 421 deletions(-)

diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml
index 1af574e9..74853d20 100644
--- a/bot-components/GitHub_queries.ml
+++ b/bot-components/GitHub_queries.ml
@@ -1021,3 +1021,9 @@ let get_project_field_values ~bot_info ~organization ~project ~field ~options =
         Lwt.return_error (f "Organization %s does not exist." organization) )
   | Error err ->
       Lwt.return_error err
+
+let get_artifact_blob ~bot_info ~owner ~repo ~artifact_id =
+  generic_get_zip ~bot_info
+    (f "repos/%s/%s/actions/artifacts/%s/zip" owner repo artifact_id)
+    (let open Zip in
+    List.map ~f:(fun (entry, contents) -> (entry.filename, contents)) )
diff --git a/bot-components/GitHub_queries.mli b/bot-components/GitHub_queries.mli
index b9b569e4..969e4ba6 100644
--- a/bot-components/GitHub_queries.mli
+++ b/bot-components/GitHub_queries.mli
@@ -151,3 +151,10 @@ val get_project_field_values :
      , string )
      result
      Lwt.t
+
+val get_artifact_blob :
+     bot_info:Bot_info.t
+  -> owner:string
+  -> repo:string
+  -> artifact_id:string
+  -> ((string * string) list, string) result Lwt.t
diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index 8587df60..8317e308 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -3,6 +3,7 @@ open Bot_info
 open Cohttp
 open Cohttp_lwt_unix
 open Lwt
+open Zip
 
 let f = Printf.sprintf
 
@@ -43,6 +44,26 @@ let handle_json action body =
   | Yojson.Basic.Util.Type_error (err, _) ->
       Error (f "Json type error: %s\n" err)
 
+let handle_zip action body_stream =
+  Lwt_io.with_temp_file (fun (tmp_name, tmp_channel) ->
+      body_stream
+      |> Lwt_stream.iter_s (Lwt_io.write tmp_channel)
+      >>= fun () ->
+      Lwt_io.close tmp_channel
+      >>= Lwt_preemptive.detach (fun () ->
+              let zip_entries =
+                let zf = Zip.open_in tmp_name in
+                let entries =
+                  Zip.entries zf
+                  |> List.filter ~f:(fun entry -> not entry.is_directory)
+                  |> List.map ~f:(fun entry ->
+                         (entry, Zip.read_entry zf entry) )
+                in
+                Zip.close_in zf ; entries
+              in
+              zip_entries ) )
+  >|= action >>= Lwt.return_ok
+
 (* GitHub specific *)
 
 let project_api_preview_header =
@@ -51,6 +72,8 @@ let project_api_preview_header =
 let app_api_preview_header =
   [("Accept", "application/vnd.github.machine-man-preview+json")]
 
+let api_json_header = [("Accept", "application/vnd.github+json")]
+
 let github_header bot_info =
   [("Authorization", "bearer " ^ github_token bot_info)]
 
@@ -62,3 +85,12 @@ let generic_get ~bot_info relative_uri ?(header_list = []) json_handler =
   Client.get ~headers uri
   >>= (fun (_response, body) -> Cohttp_lwt.Body.to_string body)
   >|= handle_json json_handler
+
+let generic_get_zip ~bot_info relative_uri ?(header_list = []) zip_handler =
+  let uri = "https://api.github.com/" ^ relative_uri |> Uri.of_string in
+  let headers =
+    headers (header_list @ github_header bot_info) bot_info.github_name
+  in
+  Client.get ~headers uri
+  >>= fun (_response, body) ->
+  Cohttp_lwt.Body.to_stream body |> handle_zip zip_handler
diff --git a/bot-components/Utils.mli b/bot-components/Utils.mli
index 142a99e2..0766d2c0 100644
--- a/bot-components/Utils.mli
+++ b/bot-components/Utils.mli
@@ -17,6 +17,8 @@ val project_api_preview_header : (string * string) list
 
 val app_api_preview_header : (string * string) list
 
+val api_json_header : (string * string) list
+
 val github_header : Bot_info.t -> (string * string) list
 
 val generic_get :
@@ -25,3 +27,10 @@ val generic_get :
   -> ?header_list:(string * string) list
   -> (Yojson.Basic.t -> 'a)
   -> ('a, string) result Lwt.t
+
+val generic_get_zip :
+     bot_info:Bot_info.t
+  -> string
+  -> ?header_list:(string * string) list
+  -> ((Zip.entry * string) list -> 'a)
+  -> ('a, string) result Lwt.t
diff --git a/bot-components/dune b/bot-components/dune
index e7f35d79..a2c5ba1a 100644
--- a/bot-components/dune
+++ b/bot-components/dune
@@ -1,8 +1,8 @@
 (library
  (name Bot_components)
  (public_name bot-components)
- (libraries base cohttp-lwt-unix cstruct eqaf hex mirage-crypto stdio str
-   x509 yojson ISO8601)
+ (libraries base camlzip cohttp-lwt-unix cstruct eqaf hex mirage-crypto stdio
+   str x509 yojson ISO8601)
  (private_modules GraphQL_query GitHub_GraphQL Utils)
  (modules_without_implementation GitHub_types GitLab_types)
  (preprocess
diff --git a/src/actions.ml b/src/actions.ml
index 87b50e14..0205bc31 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -736,20 +736,101 @@ type coqbot_minimize_script_data =
   | MinimizeScript of {quote_kind: string; body: string}
   | MinimizeAttachment of {description: string; url: string}
 
+type artifact_info =
+  | ArtifactInfo of
+      {artifact_owner: string; artifact_repo: string; artifact_id: string}
+
+let parse_github_artifact_url url =
+  let github_prefix = "https://github.com/" in
+  let regexp =
+    Str.quote github_prefix
+    ^ "\\([^/]+\\)/\\([^/]+\\)/suites/.*/artifacts/\\([0-9]+\\)"
+  in
+  if string_match ~regexp url then
+    Some
+      (ArtifactInfo
+         { artifact_owner= Str.matched_group 1 url
+         ; artifact_repo= Str.matched_group 2 url
+         ; artifact_id= Str.matched_group 3 url } )
+  else None
+
+type artifact_error =
+  | ArtifactEmpty
+  | ArtifactContainsMultipleFiles of string list
+  | ArtifactDownloadError of string
+
+type run_ci_minimization_error =
+  {url: string; artifact: artifact_info; artifact_error: artifact_error}
+
+let run_ci_minimization_error_to_string
+    { url= artifact_url
+    ; artifact= ArtifactInfo {artifact_owner; artifact_repo; artifact_id}
+    ; artifact_error } =
+  match artifact_error with
+  | ArtifactEmpty ->
+      f "Could not resume minimization with [empty artifact](%s)" artifact_url
+  | ArtifactContainsMultipleFiles filenames ->
+      f
+        "Could not resume minimization because [artifact](%s) contains more \
+         than one file: %s"
+        artifact_url
+        (String.concat ~sep:", " filenames)
+  | ArtifactDownloadError error ->
+      f
+        "Could not resume minimization because [artifact %s/%s:%s](%s) failed \
+         to download:\n\
+         Error:\n\
+         %s"
+        artifact_owner artifact_repo artifact_id artifact_url error
+
 let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
     ~base ~head ~ci_minimization_infos ~bug_file ~minimizer_extra_arguments =
+  let open Lwt_result.Infix in
   (* for convenience of control flow, we always create the temporary
      file, but we only pass in the file name if the bug file contents
      is non-None *)
   Lwt_io.with_temp_file (fun (bug_file_name, bug_file_ch) ->
-      ( match bug_file with
+      (let open Lwt.Infix in
+      match bug_file with
       | None ->
-          Lwt.return_unit
+          Lwt.return_ok ()
       | Some (MinimizeScript {body= bug_file_contents}) ->
-          Lwt_io.write bug_file_ch bug_file_contents
-      | Some (MinimizeAttachment {url}) ->
-          download_to ~uri:(Uri.of_string url) bug_file_ch )
+          Lwt_io.write bug_file_ch bug_file_contents >>= Lwt.return_ok
+      | Some (MinimizeAttachment {url}) -> (
+        match parse_github_artifact_url url with
+        | Some
+            ( ArtifactInfo {artifact_owner; artifact_repo; artifact_id} as
+            artifact ) -> (
+            Lwt_io.printlf
+              "Downloading artifact %s/%s:%s for %s/%s#%s (%s) (parsed from %s)"
+              artifact_owner artifact_repo artifact_id owner repo pr_number
+              (GitHub_ID.to_string comment_thread_id)
+              url
+            >>= fun () ->
+            GitHub_queries.get_artifact_blob ~bot_info ~owner:artifact_owner
+              ~repo:artifact_repo ~artifact_id
+            >>= function
+            | Ok [(_filename, bug_file_contents)] ->
+                Lwt_io.write bug_file_ch bug_file_contents >>= Lwt.return_ok
+            | Ok [] ->
+                Lwt.return_error {url; artifact; artifact_error= ArtifactEmpty}
+            | Ok files ->
+                files
+                |> List.map ~f:(fun (filename, _contents) -> filename)
+                |> fun artifact_filenames ->
+                Lwt.return_error
+                  { url
+                  ; artifact
+                  ; artifact_error=
+                      ArtifactContainsMultipleFiles artifact_filenames }
+            | Error err ->
+                Lwt.return_error
+                  {url; artifact; artifact_error= ArtifactDownloadError err} )
+        | None ->
+            download_to ~uri:(Uri.of_string url) bug_file_ch >>= Lwt.return_ok )
+      )
       >>= fun () ->
+      let open Lwt.Infix in
       Lwt_io.flush bug_file_ch
       >>= fun () ->
       let bug_file_name = Option.map ~f:(fun _ -> bug_file_name) bug_file in
@@ -759,7 +840,8 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
             ~pr_number ~docker_image ~target ~opam_switch ~failing_urls
             ~passing_urls ~base ~head ~minimizer_extra_arguments ~bug_file_name
           >>= fun result -> Lwt.return (target, result) )
-        ci_minimization_infos )
+        ci_minimization_infos
+      >>= Lwt.return_ok )
   >>= fun results ->
   results
   |> List.partition_map ~f:(function
@@ -767,7 +849,7 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
            Either.First target
        | target, Error f ->
            Either.Second (target, f) )
-  |> Lwt.return
+  |> Lwt.return_ok
 
 type ci_minimization_job_suggestion_info =
   { base_job_failed: bool
@@ -1305,444 +1387,474 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
         ~pr_number:(Int.to_string pr_number) ~base ~head
         ~ci_minimization_infos:jobs_to_minimize ~minimizer_extra_arguments
         ~bug_file
-      >>= fun (jobs_minimized, jobs_that_could_not_be_minimized) ->
-      let pluralize word ?plural ls =
-        match (ls, plural) with
-        | [_], _ ->
-            word
-        | _, Some plural ->
-            plural
-        | _, _ ->
-            word ^ "s"
-      in
-      (* Construct a comment body *)
-      let unminimizable_jobs_description ~f =
-        match
-          unminimizable_jobs |> List.filter ~f:(fun (name, _) -> f name)
-        with
-        | [] ->
-            None
-        | [(name, err)] ->
-            Some
-              (Printf.sprintf "The job %s could not be minimized because %s.\n"
-                 name err )
-        | unminimizable_jobs ->
-            Some
-              ( "The following jobs could not be minimized:\n"
-              ^ ( unminimizable_jobs
-                |> List.map ~f:(fun (name, err) ->
-                       Printf.sprintf "- %s (%s)" name err )
-                |> String.concat ~sep:"\n" )
-              ^ "\n\n" )
-      in
-      let bad_jobs_description ~f =
-        match
-          bad_jobs_to_minimize
-          |> List.filter ~f:(fun (_, {target (*; full_target*)}) ->
-                 f target (*|| f full_target*) )
-        with
-        | [] ->
-            None
-        | [(reason, {target})] ->
-            Some
-              (Printf.sprintf "The job %s was not minimized because %s.\n"
-                 target reason )
-        | bad_jobs ->
-            Some
-              ( "The following jobs were not minimized:\n"
-              ^ ( bad_jobs
-                |> List.map ~f:(fun (reason, {target}) ->
-                       Printf.sprintf "- %s because %s" target reason )
-                |> String.concat ~sep:"\n" )
-              ^ "\n\n" )
-      in
-      let bad_and_unminimizable_jobs_description ~f =
-        match (bad_jobs_description ~f, unminimizable_jobs_description ~f) with
-        | None, None ->
-            None
-        | Some msg, None | None, Some msg ->
-            Some msg
-        | Some msg1, Some msg2 ->
-            Some (msg1 ^ msg2)
-      in
-      let failed_minimization_description =
-        match jobs_that_could_not_be_minimized with
-        | [] ->
-            None
-        | _ :: _ ->
-            Some
-              ( "I failed to trigger minimization on the following jobs:\n"
-              ^ ( jobs_that_could_not_be_minimized
-                |> List.map ~f:(fun (name, err) ->
-                       Printf.sprintf "- %s (%s)" name err )
-                |> String.concat ~sep:"\n" )
-              ^ "\n\n" )
-      in
-      let unfinished_pipelines_description =
-        (if base_pipeline_finished then [] else [f "base commit (%s)" base])
-        @ if head_pipeline_finished then [] else [f "head commit (%s)" head]
-      in
-      let try_again_msg =
-        match unfinished_pipelines_description with
-        | [] ->
-            ""
-        | ls ->
-            f "\nHowever, you may want to try again once the %s for the %s %s."
-              (pluralize "pipeline" ls)
-              (ls |> String.concat ~sep:" and ")
-              (pluralize "finishes" ~plural:"finish" ls)
-      in
-      let may_wish_to_wait_msg =
-        match unfinished_pipelines_description with
-        | [] ->
-            ""
-        | ls ->
-            f
-              "\n\n\
-               :warning: :hourglass: You may want to wait until the %s for the \
-               %s %s."
-              (pluralize "pipeline" ls)
-              (ls |> String.concat ~sep:" and ")
-              (pluralize "finishes" ~plural:"finish" ls)
-      in
-      let note_some_head_unfinished_msg =
-        if head_pipeline_finished then ""
-        else
-          f
-            "\n\
-             Some jobs may have been missed because the pipeline for the head \
-             commit (%s) has not yet finished."
-            head
-      in
-      let note_some_base_unfinished_msg =
-        if base_pipeline_finished then ""
-        else
-          f
-            "\n\
-             However, minimization may fail because the pipeline for the base \
-             commit (%s) has not yet finished."
-            base
-      in
-      ( match (request, jobs_minimized, failed_minimization_description) with
-      | RequestAll, [], None ->
-          Lwt.return_some
-            ( match
-                bad_and_unminimizable_jobs_description ~f:(fun _ -> true)
-              with
-            | None ->
-                f "No valid CI jobs detected for %s.%s" head try_again_msg
-            | Some msg ->
-                f
-                  "I attempted to run all CI jobs at commit %s for \
-                   minimization, but was unable to find any jobs to \
-                   minimize.%s\n\n\
-                   %s"
-                  head try_again_msg msg )
-      | RequestAll, _, _ ->
-          ( match bad_and_unminimizable_jobs_description ~f:(fun _ -> true) with
-          | Some msg ->
-              Lwt_io.printlf
-                "When attempting to run CI Minimization by request all on \
-                 %s/%s@%s for PR #%d:\n\
-                 %s"
-                owner repo head pr_number msg
-          | None ->
-              Lwt.return_unit )
-          >>= fun () ->
-          ( match jobs_minimized with
-          | [] ->
-              f
-                "I did not succeed at triggering minimization on any jobs at \
-                 commit %s.%s"
-                head try_again_msg
-          | _ :: _ ->
-              f
-                "I am now %s minimization at commit %s on %s. I'll come back \
-                 to you with the results once it's done.%s"
-                (if Option.is_none bug_file then "running" else "resuming")
-                head
-                (jobs_minimized |> String.concat ~sep:", ")
-                note_some_head_unfinished_msg )
-          ^ "\n\n"
-          ^ Option.value ~default:"" failed_minimization_description
-          |> Lwt.return_some
-      | RequestExplicit requests, _, _ ->
-          (* N.B. requests may be things like library:ci-cross_crypto,
-             while the job targets are things like GitLab CI job
-             library:ci-cross_crypto (pull request) *)
-          requests
-          |> List.partition3_map ~f:(fun request ->
-                 match
-                   ( List.exists
-                       ~f:(string_match ~regexp:(Str.quote request))
-                       jobs_minimized
-                   , List.find
-                       ~f:(fun (target, _) ->
-                         string_match ~regexp:(Str.quote request) target )
-                       jobs_that_could_not_be_minimized
-                   , List.find
-                       ~f:(fun (target, _) ->
-                         string_match ~regexp:(Str.quote request) target )
-                       unminimizable_jobs
-                   , List.find
-                       ~f:(fun (_, {target}) ->
-                         string_match ~regexp:(Str.quote request) target )
-                       bad_jobs_to_minimize )
-                 with
-                 | true, _, _, _ ->
-                     `Fst request
-                 | false, Some (target, err), _, _ ->
-                     `Snd
-                       (f "%s: failed to trigger minimization (%s)" target err)
-                 | false, None, Some (target, err), _ ->
-                     `Snd (f "%s could not be minimized (%s)" target err)
-                 | false, None, None, Some (reason, {target}) ->
-                     `Snd (f "%s was not minimized because %s" target reason)
-                 | false, None, None, None ->
-                     `Trd request )
-          |> fun (successful_requests, unsuccessful_requests, unfound_requests) ->
-          let unsuccessful_requests_report =
-            match unsuccessful_requests with
+      >>= function
+      | Ok (jobs_minimized, jobs_that_could_not_be_minimized) -> (
+          let pluralize word ?plural ls =
+            match (ls, plural) with
+            | [_], _ ->
+                word
+            | _, Some plural ->
+                plural
+            | _, _ ->
+                word ^ "s"
+          in
+          (* Construct a comment body *)
+          let unminimizable_jobs_description ~f =
+            match
+              unminimizable_jobs |> List.filter ~f:(fun (name, _) -> f name)
+            with
             | [] ->
                 None
-            | [msg] ->
-                Some msg
-            | _ ->
+            | [(name, err)] ->
+                Some
+                  (Printf.sprintf
+                     "The job %s could not be minimized because %s.\n" name err )
+            | unminimizable_jobs ->
                 Some
-                  ( "The following requests were not fulfilled:\n"
-                  ^ ( unsuccessful_requests
-                    |> List.map ~f:(fun msg -> "- " ^ msg)
+                  ( "The following jobs could not be minimized:\n"
+                  ^ ( unminimizable_jobs
+                    |> List.map ~f:(fun (name, err) ->
+                           Printf.sprintf "- %s (%s)" name err )
                     |> String.concat ~sep:"\n" )
                   ^ "\n\n" )
           in
-          let unfound_requests_report =
-            let all_jobs =
-              List.map
-                ~f:(fun (target, _) -> target)
-                jobs_that_could_not_be_minimized
-              @ List.map ~f:(fun (target, _) -> target) unminimizable_jobs
-              @ List.map ~f:(fun (_, {target}) -> target) bad_jobs_to_minimize
-              |> List.sort ~compare:String.compare
-            in
-            match unfound_requests with
+          let bad_jobs_description ~f =
+            match
+              bad_jobs_to_minimize
+              |> List.filter ~f:(fun (_, {target (*; full_target*)}) ->
+                     f target (*|| f full_target*) )
+            with
             | [] ->
                 None
-            | [request] ->
+            | [(reason, {target})] ->
                 Some
-                  (f
-                     "requested target '%s' could not be found among the jobs \
-                      %s.%s"
-                     request
-                     (all_jobs |> String.concat ~sep:", ")
-                     note_some_head_unfinished_msg )
-            | _ :: _ :: _ ->
+                  (Printf.sprintf "The job %s was not minimized because %s.\n"
+                     target reason )
+            | bad_jobs ->
                 Some
-                  (f
-                     "requested targets %s could not be found among the jobs \
-                      %s.%s"
-                     (unfound_requests |> String.concat ~sep:", ")
-                     (all_jobs |> String.concat ~sep:", ")
-                     note_some_head_unfinished_msg )
+                  ( "The following jobs were not minimized:\n"
+                  ^ ( bad_jobs
+                    |> List.map ~f:(fun (reason, {target}) ->
+                           Printf.sprintf "- %s because %s" target reason )
+                    |> String.concat ~sep:"\n" )
+                  ^ "\n\n" )
           in
-          let unsuccessful_requests_report =
-            match (unsuccessful_requests_report, unfound_requests_report) with
+          let bad_and_unminimizable_jobs_description ~f =
+            match
+              (bad_jobs_description ~f, unminimizable_jobs_description ~f)
+            with
             | None, None ->
                 None
-            | Some msg, None ->
+            | Some msg, None | None, Some msg ->
                 Some msg
-            | None, Some msg ->
-                Some ("The " ^ msg)
             | Some msg1, Some msg2 ->
-                Some (msg1 ^ "\nAdditionally, the " ^ msg2)
+                Some (msg1 ^ msg2)
           in
-          ( match (successful_requests, unsuccessful_requests_report) with
-          | [], None ->
-              "No CI minimization requests made?"
-          | [], Some msg ->
-              "I was unable to minimize any of the CI targets that you \
-               requested." ^ try_again_msg ^ "\n" ^ msg
-          | _ :: _, _ ->
-              f
-                "I am now %s minimization at commit %s on requested %s %s. \
-                 I'll come back to you with the results once it's done.%s\n\n\
-                 %s"
-                (if Option.is_none bug_file then "running" else "resuming")
-                head
-                (pluralize "target" successful_requests)
-                (successful_requests |> String.concat ~sep:", ")
-                note_some_base_unfinished_msg
-                (Option.value ~default:"" unsuccessful_requests_report) )
-          |> Lwt.return_some
-      | RequestSuggested, [], None ->
-          ( match possible_jobs_to_minimize with
-          | [] ->
-              f "No CI jobs are available to be minimized for commit %s.%s" head
-                try_again_msg
-          | _ :: _ ->
-              f
-                "You requested minimization of suggested failing CI jobs, but \
-                 no jobs were suggested at commit %s. You can trigger \
-                 minimization of %s with `ci minimize all` or by requesting \
-                 some targets by name.%s"
-                head
-                ( possible_jobs_to_minimize
-                |> List.map ~f:(fun (_, {target}) -> target)
-                |> String.concat ~sep:", " )
-                may_wish_to_wait_msg )
-          |> Lwt.return_some
-      | RequestSuggested, [], Some failed_minimization_description ->
-          f
-            "I attempted to minimize suggested failing CI jobs at commit %s, \
-             but was unable to succeed on any jobs.%s\n\
-             %s"
-            head try_again_msg failed_minimization_description
-          |> Lwt.return_some
-      | RequestSuggested, _ :: _, _ ->
-          f
-            "I have initiated minimization at commit %s for the suggested %s \
-             %s as requested.%s\n\n\
-             %s"
-            head
-            (pluralize "target" jobs_minimized)
-            (jobs_minimized |> String.concat ~sep:", ")
-            try_again_msg
-            (Option.value ~default:"" failed_minimization_description)
-          |> Lwt.return_some
-      | Auto, jobs_minimized, failed_minimization_description -> (
-          ( match bad_and_unminimizable_jobs_description ~f:(fun _ -> true) with
-          | Some msg ->
-              Lwt_io.printlf
-                "When attempting to run CI Minimization by auto on %s/%s@%s \
-                 for PR #%d:\n\
-                 %s"
-                owner repo head pr_number msg
-          | None ->
-              Lwt.return_unit )
-          >>= fun () ->
-          let suggest_jobs =
-            match suggested_jobs_to_minimize with
+          let failed_minimization_description =
+            match jobs_that_could_not_be_minimized with
             | [] ->
                 None
-            | _ ->
+            | _ :: _ ->
                 Some
-                  (f
-                     ":runner: <code>@%s ci minimize</code> will minimize the \
-                      following %s: %s"
-                     bot_info.github_name
-                     (pluralize "target" suggested_jobs_to_minimize)
-                     ( suggested_jobs_to_minimize
-                     |> List.map ~f:(fun {target} -> target)
-                     |> String.concat ~sep:", " ) )
+                  ( "I failed to trigger minimization on the following jobs:\n"
+                  ^ ( jobs_that_could_not_be_minimized
+                    |> List.map ~f:(fun (name, err) ->
+                           Printf.sprintf "- %s (%s)" name err )
+                    |> String.concat ~sep:"\n" )
+                  ^ "\n\n" )
           in
-          let suggest_only_all_jobs =
-            let pre_message =
-              f
-                "- If you tag me saying `@%s ci minimize all`, I will \
-                 additionally minimize the following %s (which I do not \
-                 suggest minimizing):"
-                bot_info.github_name
-                (pluralize "target" possible_jobs_to_minimize)
-            in
-            match possible_jobs_to_minimize with
+          let unfinished_pipelines_description =
+            (if base_pipeline_finished then [] else [f "base commit (%s)" base])
+            @ if head_pipeline_finished then [] else [f "head commit (%s)" head]
+          in
+          let try_again_msg =
+            match unfinished_pipelines_description with
             | [] ->
-                None
-            | [(reason, {target})] ->
-                Some (f "%s %s (because %s)\n\n\n" pre_message target reason)
-            | _ ->
-                Some
-                  (f "%s\n%s\n\n\n" pre_message
-                     ( possible_jobs_to_minimize
-                     |> List.map ~f:(fun (reason, {target}) ->
-                            f "  - %s (because %s)" target reason )
-                     |> String.concat ~sep:"\n" ) )
+                ""
+            | ls ->
+                f
+                  "\n\
+                   However, you may want to try again once the %s for the %s \
+                   %s."
+                  (pluralize "pipeline" ls)
+                  (ls |> String.concat ~sep:" and ")
+                  (pluralize "finishes" ~plural:"finish" ls)
           in
-          match
-            ( jobs_minimized
-            , failed_minimization_description
-            , suggest_jobs
-            , suggest_only_all_jobs
-            , suggest_minimization )
-          with
-          | [], None, None, None, _ ->
-              Lwt_io.printlf
-                "No candidates found for minimization on %s/%s@%s for PR #%d."
-                owner repo head pr_number
-              >>= fun () -> Lwt.return_none
-          | [], None, None, Some msg, _ ->
-              Lwt_io.printlf
-                "No suggested candidates found for minimization on %s/%s@%s \
-                 for PR #%d:\n\
-                 %s"
-                owner repo head pr_number msg
-              >>= fun () -> Lwt.return_none
-          | [], None, Some suggestion_msg, _, Error reason ->
-              Lwt_io.printlf
-                "Candidates found for minimization on %s/%s@%s for PR #%d, but \
-                 I am not commenting because minimization is not suggested \
-                 because %s:\n\
-                 %s\n\
-                 %s"
-                owner repo head pr_number reason suggestion_msg
-                (Option.value ~default:"" suggest_only_all_jobs)
-              >>= fun () -> Lwt.return_none
-          | [], Some failed_minimization_description, _, _, _ ->
-              Lwt_io.printlf
-                "Candidates found for auto minimization on %s/%s@%s for PR \
-                 #%d, but all attempts to trigger minimization failed:\n\
-                 %s"
-                owner repo head pr_number failed_minimization_description
-              >>= fun () -> Lwt.return_none
-          | [], None, Some suggestion_msg, _, Ok () ->
+          let may_wish_to_wait_msg =
+            match unfinished_pipelines_description with
+            | [] ->
+                ""
+            | ls ->
+                f
+                  "\n\n\
+                   :warning: :hourglass: You may want to wait until the %s for \
+                   the %s %s."
+                  (pluralize "pipeline" ls)
+                  (ls |> String.concat ~sep:" and ")
+                  (pluralize "finishes" ~plural:"finish" ls)
+          in
+          let note_some_head_unfinished_msg =
+            if head_pipeline_finished then ""
+            else
               f
-                ":red_circle: CI %s at commit %s without any failure in the \
-                 test-suite\n\n\
-                 :heavy_check_mark: Corresponding %s for the base commit %s \
-                 succeeded\n\n\
-                 :grey_question: Ask me to try to extract %s that can be added \
-                 to the test-suite\n\n\
-                 <details><summary>%s</summary>\n\n\
-                 - You can also pass me a specific list of targets to minimize \
-                 as arguments.\n\
-                 %s\n\
-                 </details>%s"
-                (pluralize "failure" suggested_jobs_to_minimize)
+                "\n\
+                 Some jobs may have been missed because the pipeline for the \
+                 head commit (%s) has not yet finished."
                 head
-                (pluralize "job" suggested_jobs_to_minimize)
+          in
+          let note_some_base_unfinished_msg =
+            if base_pipeline_finished then ""
+            else
+              f
+                "\n\
+                 However, minimization may fail because the pipeline for the \
+                 base commit (%s) has not yet finished."
                 base
-                (pluralize "a minimal test case" ~plural:"minimal test cases"
-                   suggested_jobs_to_minimize )
-                suggestion_msg
-                (Option.value ~default:"" suggest_only_all_jobs)
-                may_wish_to_wait_msg
+          in
+          ( match (request, jobs_minimized, failed_minimization_description) with
+          | RequestAll, [], None ->
+              Lwt.return_some
+                ( match
+                    bad_and_unminimizable_jobs_description ~f:(fun _ -> true)
+                  with
+                | None ->
+                    f "No valid CI jobs detected for %s.%s" head try_again_msg
+                | Some msg ->
+                    f
+                      "I attempted to run all CI jobs at commit %s for \
+                       minimization, but was unable to find any jobs to \
+                       minimize.%s\n\n\
+                       %s"
+                      head try_again_msg msg )
+          | RequestAll, _, _ ->
+              ( match
+                  bad_and_unminimizable_jobs_description ~f:(fun _ -> true)
+                with
+              | Some msg ->
+                  Lwt_io.printlf
+                    "When attempting to run CI Minimization by request all on \
+                     %s/%s@%s for PR #%d:\n\
+                     %s"
+                    owner repo head pr_number msg
+              | None ->
+                  Lwt.return_unit )
+              >>= fun () ->
+              ( match jobs_minimized with
+              | [] ->
+                  f
+                    "I did not succeed at triggering minimization on any jobs \
+                     at commit %s.%s"
+                    head try_again_msg
+              | _ :: _ ->
+                  f
+                    "I am now %s minimization at commit %s on %s. I'll come \
+                     back to you with the results once it's done.%s"
+                    (if Option.is_none bug_file then "running" else "resuming")
+                    head
+                    (jobs_minimized |> String.concat ~sep:", ")
+                    note_some_head_unfinished_msg )
+              ^ "\n\n"
+              ^ Option.value ~default:"" failed_minimization_description
+              |> Lwt.return_some
+          | RequestExplicit requests, _, _ ->
+              (* N.B. requests may be things like library:ci-cross_crypto,
+                 while the job targets are things like GitLab CI job
+                 library:ci-cross_crypto (pull request) *)
+              requests
+              |> List.partition3_map ~f:(fun request ->
+                     match
+                       ( List.exists
+                           ~f:(string_match ~regexp:(Str.quote request))
+                           jobs_minimized
+                       , List.find
+                           ~f:(fun (target, _) ->
+                             string_match ~regexp:(Str.quote request) target )
+                           jobs_that_could_not_be_minimized
+                       , List.find
+                           ~f:(fun (target, _) ->
+                             string_match ~regexp:(Str.quote request) target )
+                           unminimizable_jobs
+                       , List.find
+                           ~f:(fun (_, {target}) ->
+                             string_match ~regexp:(Str.quote request) target )
+                           bad_jobs_to_minimize )
+                     with
+                     | true, _, _, _ ->
+                         `Fst request
+                     | false, Some (target, err), _, _ ->
+                         `Snd
+                           (f "%s: failed to trigger minimization (%s)" target
+                              err )
+                     | false, None, Some (target, err), _ ->
+                         `Snd (f "%s could not be minimized (%s)" target err)
+                     | false, None, None, Some (reason, {target}) ->
+                         `Snd
+                           (f "%s was not minimized because %s" target reason)
+                     | false, None, None, None ->
+                         `Trd request )
+              |> fun ( successful_requests
+                     , unsuccessful_requests
+                     , unfound_requests ) ->
+              let unsuccessful_requests_report =
+                match unsuccessful_requests with
+                | [] ->
+                    None
+                | [msg] ->
+                    Some msg
+                | _ ->
+                    Some
+                      ( "The following requests were not fulfilled:\n"
+                      ^ ( unsuccessful_requests
+                        |> List.map ~f:(fun msg -> "- " ^ msg)
+                        |> String.concat ~sep:"\n" )
+                      ^ "\n\n" )
+              in
+              let unfound_requests_report =
+                let all_jobs =
+                  List.map
+                    ~f:(fun (target, _) -> target)
+                    jobs_that_could_not_be_minimized
+                  @ List.map ~f:(fun (target, _) -> target) unminimizable_jobs
+                  @ List.map
+                      ~f:(fun (_, {target}) -> target)
+                      bad_jobs_to_minimize
+                  |> List.sort ~compare:String.compare
+                in
+                match unfound_requests with
+                | [] ->
+                    None
+                | [request] ->
+                    Some
+                      (f
+                         "requested target '%s' could not be found among the \
+                          jobs %s.%s"
+                         request
+                         (all_jobs |> String.concat ~sep:", ")
+                         note_some_head_unfinished_msg )
+                | _ :: _ :: _ ->
+                    Some
+                      (f
+                         "requested targets %s could not be found among the \
+                          jobs %s.%s"
+                         (unfound_requests |> String.concat ~sep:", ")
+                         (all_jobs |> String.concat ~sep:", ")
+                         note_some_head_unfinished_msg )
+              in
+              let unsuccessful_requests_report =
+                match
+                  (unsuccessful_requests_report, unfound_requests_report)
+                with
+                | None, None ->
+                    None
+                | Some msg, None ->
+                    Some msg
+                | None, Some msg ->
+                    Some ("The " ^ msg)
+                | Some msg1, Some msg2 ->
+                    Some (msg1 ^ "\nAdditionally, the " ^ msg2)
+              in
+              ( match (successful_requests, unsuccessful_requests_report) with
+              | [], None ->
+                  "No CI minimization requests made?"
+              | [], Some msg ->
+                  "I was unable to minimize any of the CI targets that you \
+                   requested." ^ try_again_msg ^ "\n" ^ msg
+              | _ :: _, _ ->
+                  f
+                    "I am now %s minimization at commit %s on requested %s %s. \
+                     I'll come back to you with the results once it's done.%s\n\n\
+                     %s"
+                    (if Option.is_none bug_file then "running" else "resuming")
+                    head
+                    (pluralize "target" successful_requests)
+                    (successful_requests |> String.concat ~sep:", ")
+                    note_some_base_unfinished_msg
+                    (Option.value ~default:"" unsuccessful_requests_report) )
+              |> Lwt.return_some
+          | RequestSuggested, [], None ->
+              ( match possible_jobs_to_minimize with
+              | [] ->
+                  f "No CI jobs are available to be minimized for commit %s.%s"
+                    head try_again_msg
+              | _ :: _ ->
+                  f
+                    "You requested minimization of suggested failing CI jobs, \
+                     but no jobs were suggested at commit %s. You can trigger \
+                     minimization of %s with `ci minimize all` or by \
+                     requesting some targets by name.%s"
+                    head
+                    ( possible_jobs_to_minimize
+                    |> List.map ~f:(fun (_, {target}) -> target)
+                    |> String.concat ~sep:", " )
+                    may_wish_to_wait_msg )
               |> Lwt.return_some
-          | _ :: _, _, _, _, _ ->
+          | RequestSuggested, [], Some failed_minimization_description ->
               f
-                ":red_circle: CI %s at commit %s without any failure in the \
-                 test-suite\n\n\
-                 :heavy_check_mark: Corresponding %s for the base commit %s \
-                 succeeded\n\n\
-                 <details><summary>:runner: I have automatically started \
-                 minimization for %s to augment the test-suite</summary>\n\n\
-                 - You can also pass me a specific list of targets to minimize \
-                 as arguments.\n\
-                 %s\n\
-                 </details>"
-                (pluralize "failure" jobs_minimized)
+                "I attempted to minimize suggested failing CI jobs at commit \
+                 %s, but was unable to succeed on any jobs.%s\n\
+                 %s"
+                head try_again_msg failed_minimization_description
+              |> Lwt.return_some
+          | RequestSuggested, _ :: _, _ ->
+              f
+                "I have initiated minimization at commit %s for the suggested \
+                 %s %s as requested.%s\n\n\
+                 %s"
                 head
-                (pluralize "job" jobs_minimized)
-                base
+                (pluralize "target" jobs_minimized)
                 (jobs_minimized |> String.concat ~sep:", ")
-                (Option.value ~default:"" suggest_only_all_jobs)
-              |> Lwt.return_some ) )
-      >>= function
-      | Some message ->
-          GitHub_mutations.post_comment ~id:comment_thread_id ~message ~bot_info
-          >>= GitHub_mutations.report_on_posting_comment
-      | None ->
-          Lwt_io.printlf
-            "NOT commenting with CI minimization information at %s/%s@%s (PR \
-             #%d)."
-            owner repo head pr_number )
+                try_again_msg
+                (Option.value ~default:"" failed_minimization_description)
+              |> Lwt.return_some
+          | Auto, jobs_minimized, failed_minimization_description -> (
+              ( match
+                  bad_and_unminimizable_jobs_description ~f:(fun _ -> true)
+                with
+              | Some msg ->
+                  Lwt_io.printlf
+                    "When attempting to run CI Minimization by auto on \
+                     %s/%s@%s for PR #%d:\n\
+                     %s"
+                    owner repo head pr_number msg
+              | None ->
+                  Lwt.return_unit )
+              >>= fun () ->
+              let suggest_jobs =
+                match suggested_jobs_to_minimize with
+                | [] ->
+                    None
+                | _ ->
+                    Some
+                      (f
+                         ":runner: <code>@%s ci minimize</code> will minimize \
+                          the following %s: %s"
+                         bot_info.github_name
+                         (pluralize "target" suggested_jobs_to_minimize)
+                         ( suggested_jobs_to_minimize
+                         |> List.map ~f:(fun {target} -> target)
+                         |> String.concat ~sep:", " ) )
+              in
+              let suggest_only_all_jobs =
+                let pre_message =
+                  f
+                    "- If you tag me saying `@%s ci minimize all`, I will \
+                     additionally minimize the following %s (which I do not \
+                     suggest minimizing):"
+                    bot_info.github_name
+                    (pluralize "target" possible_jobs_to_minimize)
+                in
+                match possible_jobs_to_minimize with
+                | [] ->
+                    None
+                | [(reason, {target})] ->
+                    Some
+                      (f "%s %s (because %s)\n\n\n" pre_message target reason)
+                | _ ->
+                    Some
+                      (f "%s\n%s\n\n\n" pre_message
+                         ( possible_jobs_to_minimize
+                         |> List.map ~f:(fun (reason, {target}) ->
+                                f "  - %s (because %s)" target reason )
+                         |> String.concat ~sep:"\n" ) )
+              in
+              match
+                ( jobs_minimized
+                , failed_minimization_description
+                , suggest_jobs
+                , suggest_only_all_jobs
+                , suggest_minimization )
+              with
+              | [], None, None, None, _ ->
+                  Lwt_io.printlf
+                    "No candidates found for minimization on %s/%s@%s for PR \
+                     #%d."
+                    owner repo head pr_number
+                  >>= fun () -> Lwt.return_none
+              | [], None, None, Some msg, _ ->
+                  Lwt_io.printlf
+                    "No suggested candidates found for minimization on \
+                     %s/%s@%s for PR #%d:\n\
+                     %s"
+                    owner repo head pr_number msg
+                  >>= fun () -> Lwt.return_none
+              | [], None, Some suggestion_msg, _, Error reason ->
+                  Lwt_io.printlf
+                    "Candidates found for minimization on %s/%s@%s for PR #%d, \
+                     but I am not commenting because minimization is not \
+                     suggested because %s:\n\
+                     %s\n\
+                     %s"
+                    owner repo head pr_number reason suggestion_msg
+                    (Option.value ~default:"" suggest_only_all_jobs)
+                  >>= fun () -> Lwt.return_none
+              | [], Some failed_minimization_description, _, _, _ ->
+                  Lwt_io.printlf
+                    "Candidates found for auto minimization on %s/%s@%s for PR \
+                     #%d, but all attempts to trigger minimization failed:\n\
+                     %s"
+                    owner repo head pr_number failed_minimization_description
+                  >>= fun () -> Lwt.return_none
+              | [], None, Some suggestion_msg, _, Ok () ->
+                  f
+                    ":red_circle: CI %s at commit %s without any failure in \
+                     the test-suite\n\n\
+                     :heavy_check_mark: Corresponding %s for the base commit \
+                     %s succeeded\n\n\
+                     :grey_question: Ask me to try to extract %s that can be \
+                     added to the test-suite\n\n\
+                     <details><summary>%s</summary>\n\n\
+                     - You can also pass me a specific list of targets to \
+                     minimize as arguments.\n\
+                     %s\n\
+                     </details>%s"
+                    (pluralize "failure" suggested_jobs_to_minimize)
+                    head
+                    (pluralize "job" suggested_jobs_to_minimize)
+                    base
+                    (pluralize "a minimal test case"
+                       ~plural:"minimal test cases" suggested_jobs_to_minimize )
+                    suggestion_msg
+                    (Option.value ~default:"" suggest_only_all_jobs)
+                    may_wish_to_wait_msg
+                  |> Lwt.return_some
+              | _ :: _, _, _, _, _ ->
+                  f
+                    ":red_circle: CI %s at commit %s without any failure in \
+                     the test-suite\n\n\
+                     :heavy_check_mark: Corresponding %s for the base commit \
+                     %s succeeded\n\n\
+                     <details><summary>:runner: I have automatically started \
+                     minimization for %s to augment the test-suite</summary>\n\n\
+                     - You can also pass me a specific list of targets to \
+                     minimize as arguments.\n\
+                     %s\n\
+                     </details>"
+                    (pluralize "failure" jobs_minimized)
+                    head
+                    (pluralize "job" jobs_minimized)
+                    base
+                    (jobs_minimized |> String.concat ~sep:", ")
+                    (Option.value ~default:"" suggest_only_all_jobs)
+                  |> Lwt.return_some ) )
+          >>= function
+          | Some message ->
+              GitHub_mutations.post_comment ~id:comment_thread_id ~message
+                ~bot_info
+              >>= GitHub_mutations.report_on_posting_comment
+          | None ->
+              Lwt_io.printlf
+                "NOT commenting with CI minimization information at %s/%s@%s \
+                 (PR #%d)."
+                owner repo head pr_number )
+      | Error err ->
+          let message = run_ci_minimization_error_to_string err in
+          if comment_on_error then
+            GitHub_mutations.post_comment ~id:comment_thread_id ~message
+              ~bot_info
+            >>= GitHub_mutations.report_on_posting_comment
+          else
+            Lwt_io.printlf "Error while attempting to minimize from PR #%d:\n%s"
+              pr_number message )
   | Error (Some comment_thread_id, err) when comment_on_error ->
       GitHub_mutations.post_comment ~id:comment_thread_id
         ~message:
@@ -2033,13 +2145,13 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
                          (MinimizeScript
                             {quote_kind= ""; body= bug_file_contents} ) ) )
                >>= function
-               | [], [] ->
+               | Ok ([], []) ->
                    Lwt_io.printlf
                      "Somehow no jobs were returned from minimization \
                       resumption?\n\
                       %s"
                      message
-               | jobs_minimized, jobs_that_could_not_be_minimized -> (
+               | Ok (jobs_minimized, jobs_that_could_not_be_minimized) -> (
                    ( match jobs_minimized with
                    | [] ->
                        Lwt.return_unit
@@ -2056,7 +2168,15 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
                        Lwt.return_unit
                    | msgs ->
                        Lwt_io.printlf "Could not resume minimization of %s"
-                         (msgs |> String.concat ~sep:", ") ) )
+                         (msgs |> String.concat ~sep:", ") )
+               | Error err ->
+                   Lwt_io.printlf
+                     "Internal error (should not happen because no url was \
+                      passed):\n\
+                      Could not resume minimization of %s for %s/%s#%s:\n\
+                      %s"
+                     target owner repo pr_number
+                     (run_ci_minimization_error_to_string err) )
             |> Lwt.async ;
             Server.respond_string ~status:`OK
               ~body:"Handling CI minimization resumption." ()

From 3b15983e4fe0e81bd323332292d8a283ddbfe105 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 15:55:52 -0800
Subject: [PATCH 04/13] Fix uncaught exception around http errors

---
 src/actions.ml  | 68 +++++++++++++++++++++++++++++--------------------
 src/helpers.ml  |  6 +++--
 src/helpers.mli |  5 ++--
 3 files changed, 48 insertions(+), 31 deletions(-)

diff --git a/src/actions.ml b/src/actions.ml
index 0205bc31..a403423f 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -760,28 +760,37 @@ type artifact_error =
   | ArtifactDownloadError of string
 
 type run_ci_minimization_error =
-  {url: string; artifact: artifact_info; artifact_error: artifact_error}
-
-let run_ci_minimization_error_to_string
-    { url= artifact_url
-    ; artifact= ArtifactInfo {artifact_owner; artifact_repo; artifact_id}
-    ; artifact_error } =
-  match artifact_error with
-  | ArtifactEmpty ->
-      f "Could not resume minimization with [empty artifact](%s)" artifact_url
-  | ArtifactContainsMultipleFiles filenames ->
+  | ArtifactError of
+      {url: string; artifact: artifact_info; artifact_error: artifact_error}
+  | DownloadError of {url: string; error: string}
+
+let run_ci_minimization_error_to_string = function
+  | ArtifactError
+      { url= artifact_url
+      ; artifact= ArtifactInfo {artifact_owner; artifact_repo; artifact_id}
+      ; artifact_error } -> (
+    match artifact_error with
+    | ArtifactEmpty ->
+        f "Could not resume minimization with [empty artifact](%s)" artifact_url
+    | ArtifactContainsMultipleFiles filenames ->
+        f
+          "Could not resume minimization because [artifact](%s) contains more \
+           than one file: %s"
+          artifact_url
+          (String.concat ~sep:", " filenames)
+    | ArtifactDownloadError error ->
+        f
+          "Could not resume minimization because [artifact %s/%s:%s](%s) \
+           failed to download:\n\
+           Error:\n\
+           %s"
+          artifact_owner artifact_repo artifact_id artifact_url error )
+  | DownloadError {url; error} ->
       f
-        "Could not resume minimization because [artifact](%s) contains more \
-         than one file: %s"
-        artifact_url
-        (String.concat ~sep:", " filenames)
-  | ArtifactDownloadError error ->
-      f
-        "Could not resume minimization because [artifact %s/%s:%s](%s) failed \
-         to download:\n\
-         Error:\n\
+        "Could not resume minimization because [artifact](%s) failed to \
+         download:\n\
          %s"
-        artifact_owner artifact_repo artifact_id artifact_url error
+        url error
 
 let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
     ~base ~head ~ci_minimization_infos ~bug_file ~minimizer_extra_arguments =
@@ -813,21 +822,26 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
             | Ok [(_filename, bug_file_contents)] ->
                 Lwt_io.write bug_file_ch bug_file_contents >>= Lwt.return_ok
             | Ok [] ->
-                Lwt.return_error {url; artifact; artifact_error= ArtifactEmpty}
+                Lwt.return_error
+                  (ArtifactError {url; artifact; artifact_error= ArtifactEmpty})
             | Ok files ->
                 files
                 |> List.map ~f:(fun (filename, _contents) -> filename)
                 |> fun artifact_filenames ->
                 Lwt.return_error
-                  { url
-                  ; artifact
-                  ; artifact_error=
-                      ArtifactContainsMultipleFiles artifact_filenames }
+                  (ArtifactError
+                     { url
+                     ; artifact
+                     ; artifact_error=
+                         ArtifactContainsMultipleFiles artifact_filenames } )
             | Error err ->
                 Lwt.return_error
-                  {url; artifact; artifact_error= ArtifactDownloadError err} )
+                  (ArtifactError
+                     {url; artifact; artifact_error= ArtifactDownloadError err}
+                  ) )
         | None ->
-            download_to ~uri:(Uri.of_string url) bug_file_ch >>= Lwt.return_ok )
+            download_to ~uri:(Uri.of_string url) bug_file_ch
+            |> Lwt_result.map_error (fun error -> DownloadError {url; error}) )
       )
       >>= fun () ->
       let open Lwt.Infix in
diff --git a/src/helpers.ml b/src/helpers.ml
index 4c0ca0f2..d870fcb8 100644
--- a/src/helpers.ml
+++ b/src/helpers.ml
@@ -137,12 +137,14 @@ let github_repo_of_gitlab_url ~gitlab_mapping ~http_repo_url =
            ~gitlab_repo_full_name )
 
 let download_cps ~uri ~with_file =
+  let open Lwt.Infix in
   let rec inner_download uri =
     let* resp, body = Client.get uri in
     match Response.status resp with
     | `OK ->
         let stream = Body.to_stream body in
         with_file (fun chan -> Lwt_stream.iter_s (Lwt_io.write chan) stream)
+        >>= Lwt.return_ok
     | `Moved_permanently
     | `Found
     | `See_other
@@ -156,14 +158,14 @@ let download_cps ~uri ~with_file =
             Printf.sprintf "Redirected from %s, but no Location header found"
               (Uri.to_string uri)
           in
-          Lwt.fail_with msg )
+          Lwt.return_error msg )
     | status_code ->
         let msg =
           Printf.sprintf "HTTP request to %s failed with status code: %s"
             (Uri.to_string uri)
             (Code.string_of_status status_code)
         in
-        Lwt.fail_with msg
+        Lwt.return_error msg
   in
   inner_download uri
 
diff --git a/src/helpers.mli b/src/helpers.mli
index 9f5e988b..f5c65e3c 100644
--- a/src/helpers.mli
+++ b/src/helpers.mli
@@ -36,6 +36,7 @@ val github_repo_of_gitlab_url :
   -> http_repo_url:string
   -> (string * string, string) result
 
-val download : uri:Uri.t -> string -> unit Lwt.t
+val download : uri:Uri.t -> string -> (unit, string) Lwt_result.t
 
-val download_to : uri:Uri.t -> Lwt_io.output_channel -> unit Lwt.t
+val download_to :
+  uri:Uri.t -> Lwt_io.output_channel -> (unit, string) Lwt_result.t

From e29aa307d08890c9cad261a011f2896a30b0f0ec Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 15:38:22 -0800
Subject: [PATCH 05/13] Add opam camlzip dep to opam

1.08 is the earliest version with documentation at
https://ocaml.org/p/camlzip, and it seems to have all the necessary
functions.
---
 bot-components.opam | 1 +
 dune-project        | 1 +
 2 files changed, 2 insertions(+)

diff --git a/bot-components.opam b/bot-components.opam
index f96a21d5..c08b9c63 100644
--- a/bot-components.opam
+++ b/bot-components.opam
@@ -23,6 +23,7 @@ depends: [
   "x509" {>= "0.11.2"}
   "cstruct" {>= "5.0.0"}
   "ISO8601" {>= "0.2.0"}
+  "camlzip" {>= "1.08"}
   "odoc" {>= "1.5.2" & with-doc}
 ]
 build: [
diff --git a/dune-project b/dune-project
index bfdb5abf..80011b81 100644
--- a/dune-project
+++ b/dune-project
@@ -50,5 +50,6 @@
   (x509 (>= 0.11.2))
   (cstruct (>= 5.0.0))
   (ISO8601 (>= 0.2.0))
+  (camlzip (>= 1.08))
   (odoc (and (>= 1.5.2) :with-doc)))
 )

From 7d0727c4e08c2719aaec64ea2db14143039dcef9 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 15:57:54 -0800
Subject: [PATCH 06/13] Slightly more compact errors

---
 src/actions.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/actions.ml b/src/actions.ml
index a403423f..6dd34b2c 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -782,7 +782,6 @@ let run_ci_minimization_error_to_string = function
         f
           "Could not resume minimization because [artifact %s/%s:%s](%s) \
            failed to download:\n\
-           Error:\n\
            %s"
           artifact_owner artifact_repo artifact_id artifact_url error )
   | DownloadError {url; error} ->

From 3a69d803165eeff284e9ed412ee6bf8bd28436cc Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 16:06:38 -0800
Subject: [PATCH 07/13] More general regex

---
 src/actions.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/actions.ml b/src/actions.ml
index 6dd34b2c..98345cec 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -744,14 +744,14 @@ let parse_github_artifact_url url =
   let github_prefix = "https://github.com/" in
   let regexp =
     Str.quote github_prefix
-    ^ "\\([^/]+\\)/\\([^/]+\\)/suites/.*/artifacts/\\([0-9]+\\)"
+    ^ "\\([^/]+\\)/\\([^/]+\\)/\\(actions/runs\\|suites\\)/.*/artifacts/\\([0-9]+\\)"
   in
   if string_match ~regexp url then
     Some
       (ArtifactInfo
          { artifact_owner= Str.matched_group 1 url
          ; artifact_repo= Str.matched_group 2 url
-         ; artifact_id= Str.matched_group 3 url } )
+         ; artifact_id= Str.matched_group 4 url } )
   else None
 
 type artifact_error =

From 2cb888e15fa47efe17ee4822871bd21d865f539a Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 18:16:58 -0800
Subject: [PATCH 08/13] Better reporting of zip errors

---
 bot-components/GitHub_queries.ml  |  4 ++++
 bot-components/GitHub_queries.mli |  4 +++-
 bot-components/Utils.ml           | 27 ++++++++++++++++-----------
 bot-components/Utils.mli          |  2 +-
 src/actions.ml                    | 10 +++++++---
 5 files changed, 31 insertions(+), 16 deletions(-)

diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml
index 74853d20..2575ac18 100644
--- a/bot-components/GitHub_queries.ml
+++ b/bot-components/GitHub_queries.ml
@@ -1022,8 +1022,12 @@ let get_project_field_values ~bot_info ~organization ~project ~field ~options =
   | Error err ->
       Lwt.return_error err
 
+type zip_error = {zip_name: string; entry_name: string; message: string}
+
 let get_artifact_blob ~bot_info ~owner ~repo ~artifact_id =
   generic_get_zip ~bot_info
     (f "repos/%s/%s/actions/artifacts/%s/zip" owner repo artifact_id)
     (let open Zip in
     List.map ~f:(fun (entry, contents) -> (entry.filename, contents)) )
+  |> Lwt_result.map_error (fun (zip_name, entry_name, message) ->
+         {zip_name; entry_name; message} )
diff --git a/bot-components/GitHub_queries.mli b/bot-components/GitHub_queries.mli
index 969e4ba6..2bc3faf9 100644
--- a/bot-components/GitHub_queries.mli
+++ b/bot-components/GitHub_queries.mli
@@ -152,9 +152,11 @@ val get_project_field_values :
      result
      Lwt.t
 
+type zip_error = {zip_name: string; entry_name: string; message: string}
+
 val get_artifact_blob :
      bot_info:Bot_info.t
   -> owner:string
   -> repo:string
   -> artifact_id:string
-  -> ((string * string) list, string) result Lwt.t
+  -> ((string * string) list, zip_error) result Lwt.t
diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index 8317e308..b0507b6d 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -45,24 +45,29 @@ let handle_json action body =
       Error (f "Json type error: %s\n" err)
 
 let handle_zip action body_stream =
+  let open Lwt_result.Infix in
   Lwt_io.with_temp_file (fun (tmp_name, tmp_channel) ->
+      let open Lwt.Infix in
       body_stream
       |> Lwt_stream.iter_s (Lwt_io.write tmp_channel)
       >>= fun () ->
       Lwt_io.close tmp_channel
       >>= Lwt_preemptive.detach (fun () ->
-              let zip_entries =
-                let zf = Zip.open_in tmp_name in
-                let entries =
-                  Zip.entries zf
-                  |> List.filter ~f:(fun entry -> not entry.is_directory)
-                  |> List.map ~f:(fun entry ->
-                         (entry, Zip.read_entry zf entry) )
+              try
+                let zip_entries =
+                  let zf = Zip.open_in tmp_name in
+                  let entries =
+                    Zip.entries zf
+                    |> List.filter ~f:(fun entry -> not entry.is_directory)
+                    |> List.map ~f:(fun entry ->
+                           (entry, Zip.read_entry zf entry) )
+                  in
+                  Zip.close_in zf ; entries
                 in
-                Zip.close_in zf ; entries
-              in
-              zip_entries ) )
-  >|= action >>= Lwt.return_ok
+                Ok zip_entries
+              with Zip.Error (zip_name, entry_name, message) ->
+                Error (zip_name, entry_name, message) ) )
+  >|= action
 
 (* GitHub specific *)
 
diff --git a/bot-components/Utils.mli b/bot-components/Utils.mli
index 0766d2c0..e1e361d2 100644
--- a/bot-components/Utils.mli
+++ b/bot-components/Utils.mli
@@ -33,4 +33,4 @@ val generic_get_zip :
   -> string
   -> ?header_list:(string * string) list
   -> ((Zip.entry * string) list -> 'a)
-  -> ('a, string) result Lwt.t
+  -> ('a, string * string * string) result Lwt.t
diff --git a/src/actions.ml b/src/actions.ml
index 98345cec..bc498ea2 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -833,11 +833,15 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
                      ; artifact
                      ; artifact_error=
                          ArtifactContainsMultipleFiles artifact_filenames } )
-            | Error err ->
+            | Error {zip_name; entry_name; message} ->
                 Lwt.return_error
                   (ArtifactError
-                     {url; artifact; artifact_error= ArtifactDownloadError err}
-                  ) )
+                     { url
+                     ; artifact
+                     ; artifact_error=
+                         ArtifactDownloadError
+                           (f "Zip.Error(%s, %s, %s)" zip_name entry_name
+                              message ) } ) )
         | None ->
             download_to ~uri:(Uri.of_string url) bug_file_ch
             |> Lwt_result.map_error (fun error -> DownloadError {url; error}) )

From f0fe79df32b8c81a5917cda5dc2420eb22889d8c Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 18:23:37 -0800
Subject: [PATCH 09/13] Don't write by streams (maybe this is messing things
 up?)

---
 bot-components/Utils.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index b0507b6d..e8879bf9 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -44,12 +44,11 @@ let handle_json action body =
   | Yojson.Basic.Util.Type_error (err, _) ->
       Error (f "Json type error: %s\n" err)
 
-let handle_zip action body_stream =
+let handle_zip action body =
   let open Lwt_result.Infix in
   Lwt_io.with_temp_file (fun (tmp_name, tmp_channel) ->
       let open Lwt.Infix in
-      body_stream
-      |> Lwt_stream.iter_s (Lwt_io.write tmp_channel)
+      Lwt_io.write tmp_channel body
       >>= fun () ->
       Lwt_io.close tmp_channel
       >>= Lwt_preemptive.detach (fun () ->
@@ -97,5 +96,5 @@ let generic_get_zip ~bot_info relative_uri ?(header_list = []) zip_handler =
     headers (header_list @ github_header bot_info) bot_info.github_name
   in
   Client.get ~headers uri
-  >>= fun (_response, body) ->
-  Cohttp_lwt.Body.to_stream body |> handle_zip zip_handler
+  >>= (fun (_response, body) -> Cohttp_lwt.Body.to_string body)
+  >>= handle_zip zip_handler

From f954b80470ca36c08074cfe6e8369a7ac615760a Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 19:05:33 -0800
Subject: [PATCH 10/13] Allow more expressive errors

---
 bot-components/GitHub_queries.ml  | 7 ++++---
 bot-components/GitHub_queries.mli | 3 ++-
 bot-components/Utils.ml           | 2 +-
 bot-components/Utils.mli          | 2 +-
 src/actions.ml                    | 3 ++-
 5 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml
index 2575ac18..d606fbd7 100644
--- a/bot-components/GitHub_queries.ml
+++ b/bot-components/GitHub_queries.ml
@@ -1022,12 +1022,13 @@ let get_project_field_values ~bot_info ~organization ~project ~field ~options =
   | Error err ->
       Lwt.return_error err
 
-type zip_error = {zip_name: string; entry_name: string; message: string}
+type zip_error =
+  {zip_contents: string; zip_name: string; entry_name: string; message: string}
 
 let get_artifact_blob ~bot_info ~owner ~repo ~artifact_id =
   generic_get_zip ~bot_info
     (f "repos/%s/%s/actions/artifacts/%s/zip" owner repo artifact_id)
     (let open Zip in
     List.map ~f:(fun (entry, contents) -> (entry.filename, contents)) )
-  |> Lwt_result.map_error (fun (zip_name, entry_name, message) ->
-         {zip_name; entry_name; message} )
+  |> Lwt_result.map_error (fun (zip_contents, zip_name, entry_name, message) ->
+         {zip_contents; zip_name; entry_name; message} )
diff --git a/bot-components/GitHub_queries.mli b/bot-components/GitHub_queries.mli
index 2bc3faf9..995cf3b4 100644
--- a/bot-components/GitHub_queries.mli
+++ b/bot-components/GitHub_queries.mli
@@ -152,7 +152,8 @@ val get_project_field_values :
      result
      Lwt.t
 
-type zip_error = {zip_name: string; entry_name: string; message: string}
+type zip_error =
+  {zip_contents: string; zip_name: string; entry_name: string; message: string}
 
 val get_artifact_blob :
      bot_info:Bot_info.t
diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index e8879bf9..f360a116 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -65,7 +65,7 @@ let handle_zip action body =
                 in
                 Ok zip_entries
               with Zip.Error (zip_name, entry_name, message) ->
-                Error (zip_name, entry_name, message) ) )
+                Error (body, zip_name, entry_name, message) ) )
   >|= action
 
 (* GitHub specific *)
diff --git a/bot-components/Utils.mli b/bot-components/Utils.mli
index e1e361d2..c92bfb7d 100644
--- a/bot-components/Utils.mli
+++ b/bot-components/Utils.mli
@@ -33,4 +33,4 @@ val generic_get_zip :
   -> string
   -> ?header_list:(string * string) list
   -> ((Zip.entry * string) list -> 'a)
-  -> ('a, string * string * string) result Lwt.t
+  -> ('a, string * string * string * string) result Lwt.t
diff --git a/src/actions.ml b/src/actions.ml
index bc498ea2..91d584e7 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -833,7 +833,8 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
                      ; artifact
                      ; artifact_error=
                          ArtifactContainsMultipleFiles artifact_filenames } )
-            | Error {zip_name; entry_name; message} ->
+            | Error {zip_contents= _zip_contents; zip_name; entry_name; message}
+              ->
                 Lwt.return_error
                   (ArtifactError
                      { url

From 025ae8e69e1262a2ee52580068490c7cb5591a2c Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 19:31:57 -0800
Subject: [PATCH 11/13] Follow redirects on get

---
 bot-components/GitHub_queries.ml  |  5 ---
 bot-components/GitHub_queries.mli |  5 +--
 bot-components/Utils.ml           | 51 +++++++++++++++++++++++--------
 bot-components/Utils.mli          |  4 +--
 src/actions.ml                    |  8 ++---
 5 files changed, 44 insertions(+), 29 deletions(-)

diff --git a/bot-components/GitHub_queries.ml b/bot-components/GitHub_queries.ml
index d606fbd7..74853d20 100644
--- a/bot-components/GitHub_queries.ml
+++ b/bot-components/GitHub_queries.ml
@@ -1022,13 +1022,8 @@ let get_project_field_values ~bot_info ~organization ~project ~field ~options =
   | Error err ->
       Lwt.return_error err
 
-type zip_error =
-  {zip_contents: string; zip_name: string; entry_name: string; message: string}
-
 let get_artifact_blob ~bot_info ~owner ~repo ~artifact_id =
   generic_get_zip ~bot_info
     (f "repos/%s/%s/actions/artifacts/%s/zip" owner repo artifact_id)
     (let open Zip in
     List.map ~f:(fun (entry, contents) -> (entry.filename, contents)) )
-  |> Lwt_result.map_error (fun (zip_contents, zip_name, entry_name, message) ->
-         {zip_contents; zip_name; entry_name; message} )
diff --git a/bot-components/GitHub_queries.mli b/bot-components/GitHub_queries.mli
index 995cf3b4..969e4ba6 100644
--- a/bot-components/GitHub_queries.mli
+++ b/bot-components/GitHub_queries.mli
@@ -152,12 +152,9 @@ val get_project_field_values :
      result
      Lwt.t
 
-type zip_error =
-  {zip_contents: string; zip_name: string; entry_name: string; message: string}
-
 val get_artifact_blob :
      bot_info:Bot_info.t
   -> owner:string
   -> repo:string
   -> artifact_id:string
-  -> ((string * string) list, zip_error) result Lwt.t
+  -> ((string * string) list, string) result Lwt.t
diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index f360a116..227d6495 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -65,7 +65,7 @@ let handle_zip action body =
                 in
                 Ok zip_entries
               with Zip.Error (zip_name, entry_name, message) ->
-                Error (body, zip_name, entry_name, message) ) )
+                Error (f "Zip.Error(%s, %s, %s)" zip_name entry_name message) ) )
   >|= action
 
 (* GitHub specific *)
@@ -81,20 +81,47 @@ let api_json_header = [("Accept", "application/vnd.github+json")]
 let github_header bot_info =
   [("Authorization", "bearer " ^ github_token bot_info)]
 
-let generic_get ~bot_info relative_uri ?(header_list = []) json_handler =
-  let uri = "https://api.github.com/" ^ relative_uri |> Uri.of_string in
-  let headers =
-    headers (header_list @ github_header bot_info) bot_info.github_name
-  in
+let rec client_get ?(follow_redirects = true) ~headers uri =
   Client.get ~headers uri
-  >>= (fun (_response, body) -> Cohttp_lwt.Body.to_string body)
-  >|= handle_json json_handler
+  >>= fun (resp, body) ->
+  match Response.status resp with
+  | `OK ->
+      Lwt.return_ok body
+  | `Moved_permanently
+  | `Found
+  | `See_other
+  | `Temporary_redirect
+  | `Permanent_redirect
+    when follow_redirects -> (
+    match Header.get_location (Response.headers resp) with
+    | Some new_uri ->
+        client_get ~follow_redirects ~headers new_uri
+    | None ->
+        let msg =
+          f "Redirected from %s, but no Location header found"
+            (Uri.to_string uri)
+        in
+        Lwt.return_error msg )
+  | status_code ->
+      let msg =
+        f "HTTP request to %s failed with status code: %s" (Uri.to_string uri)
+          (Code.string_of_status status_code)
+      in
+      Lwt.return_error msg
 
-let generic_get_zip ~bot_info relative_uri ?(header_list = []) zip_handler =
+let generic_get ~bot_info relative_uri ?(header_list = []) handler =
+  let open Lwt_result.Infix in
   let uri = "https://api.github.com/" ^ relative_uri |> Uri.of_string in
   let headers =
     headers (header_list @ github_header bot_info) bot_info.github_name
   in
-  Client.get ~headers uri
-  >>= (fun (_response, body) -> Cohttp_lwt.Body.to_string body)
-  >>= handle_zip zip_handler
+  client_get ~headers uri
+  >>= (fun body -> Cohttp_lwt.Body.to_string body |> Lwt_result.ok)
+  >>= handler
+
+let generic_get_json ~bot_info relative_uri ?(header_list = []) json_handler =
+  generic_get ~bot_info relative_uri ~header_list (fun body ->
+      body |> handle_json json_handler |> Lwt.return )
+
+let generic_get_zip ~bot_info relative_uri ?(header_list = []) zip_handler =
+  generic_get ~bot_info relative_uri ~header_list (handle_zip zip_handler)
diff --git a/bot-components/Utils.mli b/bot-components/Utils.mli
index c92bfb7d..747b0cdc 100644
--- a/bot-components/Utils.mli
+++ b/bot-components/Utils.mli
@@ -21,7 +21,7 @@ val api_json_header : (string * string) list
 
 val github_header : Bot_info.t -> (string * string) list
 
-val generic_get :
+val generic_get_json :
      bot_info:Bot_info.t
   -> string
   -> ?header_list:(string * string) list
@@ -33,4 +33,4 @@ val generic_get_zip :
   -> string
   -> ?header_list:(string * string) list
   -> ((Zip.entry * string) list -> 'a)
-  -> ('a, string * string * string * string) result Lwt.t
+  -> ('a, string) result Lwt.t
diff --git a/src/actions.ml b/src/actions.ml
index 91d584e7..00a7744a 100644
--- a/src/actions.ml
+++ b/src/actions.ml
@@ -833,16 +833,12 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
                      ; artifact
                      ; artifact_error=
                          ArtifactContainsMultipleFiles artifact_filenames } )
-            | Error {zip_contents= _zip_contents; zip_name; entry_name; message}
-              ->
+            | Error message ->
                 Lwt.return_error
                   (ArtifactError
                      { url
                      ; artifact
-                     ; artifact_error=
-                         ArtifactDownloadError
-                           (f "Zip.Error(%s, %s, %s)" zip_name entry_name
-                              message ) } ) )
+                     ; artifact_error= ArtifactDownloadError message } ) )
         | None ->
             download_to ~uri:(Uri.of_string url) bug_file_ch
             |> Lwt_result.map_error (fun error -> DownloadError {url; error}) )

From a7093ff262f3dcc59fe76f5ab24033a61e5d52a9 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 22:42:53 -0800
Subject: [PATCH 12/13] Fix issue with headers

---
 bot-components/Utils.ml | 40 ++++++++++++++++++++++++++--------------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/bot-components/Utils.ml b/bot-components/Utils.ml
index 227d6495..f7c932c7 100644
--- a/bot-components/Utils.ml
+++ b/bot-components/Utils.ml
@@ -81,7 +81,13 @@ let api_json_header = [("Accept", "application/vnd.github+json")]
 let github_header bot_info =
   [("Authorization", "bearer " ^ github_token bot_info)]
 
-let rec client_get ?(follow_redirects = true) ~headers uri =
+let headers_of_list = headers
+
+(* when following a redirect from GitHub to Azure, passing along the
+   Authorization header results in 403 Forbidden.  So we strip the
+   headers when we recurse by default. *)
+let rec client_get ?(follow_redirects = true)
+    ?(include_headers_in_redirects = false) ~user_agent ~headers uri =
   Client.get ~headers uri
   >>= fun (resp, body) ->
   match Response.status resp with
@@ -93,15 +99,22 @@ let rec client_get ?(follow_redirects = true) ~headers uri =
   | `Temporary_redirect
   | `Permanent_redirect
     when follow_redirects -> (
-    match Header.get_location (Response.headers resp) with
-    | Some new_uri ->
-        client_get ~follow_redirects ~headers new_uri
-    | None ->
-        let msg =
-          f "Redirected from %s, but no Location header found"
-            (Uri.to_string uri)
-        in
-        Lwt.return_error msg )
+      let headers =
+        if include_headers_in_redirects then headers
+        else headers_of_list [] user_agent
+      in
+      match Header.get_location (Response.headers resp) with
+      | Some new_uri ->
+          Lwt_io.printlf "Following redirect to %s" (Uri.to_string new_uri)
+          >>= fun () ->
+          client_get ~follow_redirects ~include_headers_in_redirects ~headers
+            ~user_agent new_uri
+      | None ->
+          let msg =
+            f "Redirected from %s, but no Location header found"
+              (Uri.to_string uri)
+          in
+          Lwt.return_error msg )
   | status_code ->
       let msg =
         f "HTTP request to %s failed with status code: %s" (Uri.to_string uri)
@@ -112,10 +125,9 @@ let rec client_get ?(follow_redirects = true) ~headers uri =
 let generic_get ~bot_info relative_uri ?(header_list = []) handler =
   let open Lwt_result.Infix in
   let uri = "https://api.github.com/" ^ relative_uri |> Uri.of_string in
-  let headers =
-    headers (header_list @ github_header bot_info) bot_info.github_name
-  in
-  client_get ~headers uri
+  let user_agent = bot_info.github_name in
+  let headers = headers (header_list @ github_header bot_info) user_agent in
+  client_get ~headers ~user_agent uri
   >>= (fun body -> Cohttp_lwt.Body.to_string body |> Lwt_result.ok)
   >>= handler
 

From 1dfcc64597e0562dd56f048a3401ffe68f31e35e Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 27 Jan 2024 23:30:48 -0800
Subject: [PATCH 13/13] Adjust formatting a bit

---
 src/helpers.ml | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

diff --git a/src/helpers.ml b/src/helpers.ml
index d870fcb8..00076b35 100644
--- a/src/helpers.ml
+++ b/src/helpers.ml
@@ -154,18 +154,13 @@ let download_cps ~uri ~with_file =
       | Some new_uri ->
           inner_download new_uri
       | None ->
-          let msg =
-            Printf.sprintf "Redirected from %s, but no Location header found"
-              (Uri.to_string uri)
-          in
-          Lwt.return_error msg )
-    | status_code ->
-        let msg =
-          Printf.sprintf "HTTP request to %s failed with status code: %s"
+          f "Redirected from %s, but no Location header found"
             (Uri.to_string uri)
-            (Code.string_of_status status_code)
-        in
-        Lwt.return_error msg
+          |> Lwt.return_error )
+    | status_code ->
+        f "HTTP request to %s failed with status code: %s" (Uri.to_string uri)
+          (Code.string_of_status status_code)
+        |> Lwt.return_error
   in
   inner_download uri