Add support for @coqbot inline-stdlib=yes resume ci minimize ci-foo (…

…#262) Also for `@coqbot extra-arg=--inline-coqlib resume ci minimize ci-foo` and `@coqbot extra-arg=--inline-coqlib ci minimize ci-foo` For coq/coq#16967 (comment), in conjunction with JasonGross/coq-tools#144
coq · Jan 25, 2023 · 3deea7d · 3deea7d
2 parents fb0e357 + 5212d20
commit 3deea7d
Show file tree

Hide file tree

Showing 7 changed files with 107 additions and 53 deletions.
diff --git a/coq_bug_minimizer.sh b/coq_bug_minimizer.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
-# usage: coq_bug_minimizer.sh 'script' comment_thread_id comment_author github_token bot_name bot_domain owner repo coq_version ocaml_version
+# usage: coq_bug_minimizer.sh 'script' comment_thread_id comment_author github_token bot_name bot_domain owner repo coq_version ocaml_version minimizer_extra_arguments
 
 set -ex
 
-if [ $# != 10 ]; then >&2 echo Bad argument count; exit 1; fi
+if [ $# != 11 ]; then >&2 echo Bad argument count; exit 1; fi
 
 script=$1
 comment_thread_id=$2
@@ -16,6 +16,7 @@ owner=$7
 repo=$8
 coq_version=$9
 ocaml_version=${10}
+minimizer_extra_arguments=${11}
 branch_id=$(($(od -A n -t uI -N 5 /dev/urandom | tr -d ' ')))
 repo_name="coq-community/run-coq-bug-minimizer"
 branch_name="run-coq-bug-minimizer-$branch_id"
@@ -29,6 +30,7 @@ pushd "$wtree"
 printf "%s %s %s %s %s %s" "$comment_thread_id" "$comment_author" "$repo_name" "$branch_name" "$owner" "$repo" > coqbot-request-stamp
 test -z "${coq_version}" || sed -i 's~^\(\s*\)[^:\s]*coq_version:.*$~\1coq_version: '"'${coq_version}'~" .github/workflows/main.yml
 test -z "${ocaml_version}" || sed -i 's~^\(\s*\)[^:\s]*ocaml_version:.*$~\1ocaml_version: '"'${ocaml_version}'~" .github/workflows/main.yml
+printf "%s" "${minimizer_extra_arguments}" | tr ' ' '\n' > coqbot.extra-args
 printf "%s\n" "$script" > coqbot.sh
 sed -i 's/\r$//g' coqbot.sh
 echo "https://$bot_domain/coq-bug-minimizer" > coqbot.url

diff --git a/run_ci_minimization.sh b/run_ci_minimization.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
-# usage: coq_bug_minimizer.sh comment_thread_id github_token bot_name bot_domain owner repo pr_number docker_image target opam_switch failing_urls passing_urls base head [bug_file]
+# usage: coq_bug_minimizer.sh comment_thread_id github_token bot_name bot_domain owner repo pr_number docker_image target opam_switch failing_urls passing_urls base head minimizer_extra_arguments [bug_file]
 
 set -ex
 
-if [ $# != 14 ] && [ $# != 15 ]; then >&2 echo Bad argument count; exit 1; fi
+if [ $# != 15 ] && [ $# != 16 ]; then >&2 echo Bad argument count; exit 1; fi
 
 comment_thread_id=$1
 token=$2
@@ -20,7 +20,8 @@ failing_urls=${11}
 passing_urls=${12}
 base=${13}
 head=${14}
-bug_file=${15}
+minimizer_extra_arguments=${15}
+bug_file=${16}
 branch_id=$(($(od -A n -t uI -N 5 /dev/urandom | tr -d ' ')))
 repo_name="coq-community/run-coq-bug-minimizer"
 branch_name="run-coq-bug-minimizer-$branch_id"
@@ -33,6 +34,7 @@ resumption_args=(
     "${passing_urls}"
     "${base}"
     "${head}"
+    "${minimizer_extra_arguments}"
 )
 
 if [ -f "${bug_file}" ]; then
@@ -56,6 +58,7 @@ echo "${passing_urls}" >  coqbot.passing-artifact-urls
 echo "${head}" > coqbot.failing-sha
 echo "${base}" > coqbot.passing-sha
 echo "${pr_number}" > coqbot.issue-number
+printf "%s" "${minimizer_extra_arguments}" | tr ' ' '\n' > coqbot.extra-args
 echo "https://$bot_domain/ci-minimization" > coqbot.url
 echo "https://$bot_domain/resume-ci-minimization" > coqbot.resume-minimization-url
 rm -f coqbot.resumption-args

diff --git a/src/actions.ml b/src/actions.ml
@@ -736,7 +736,8 @@ type ci_minimization_info =
   ; passing_urls: string }
 
 let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
-    ~base ~head ~ci_minimization_infos ~bug_file_contents =
+    ~base ~head ~ci_minimization_infos ~bug_file_contents
+    ~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 *)
@@ -752,7 +753,7 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
         (fun {target; opam_switch; failing_urls; passing_urls; docker_image} ->
           git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo
             ~pr_number ~docker_image ~target ~opam_switch ~failing_urls
-            ~passing_urls ~base ~head ~bug_file_name
+            ~passing_urls ~base ~head ~minimizer_extra_arguments ~bug_file_name
           >>= fun result -> Lwt.return (target, result) )
         ci_minimization_infos )
   >>= fun results ->
@@ -1176,9 +1177,43 @@ let suggest_ci_minimization_for_pr = function
   | _ ->
       Suggest
 
+let format_options_for_getopts options =
+  " " ^ options ^ " " |> Str.global_replace (Str.regexp "[\n\r\t]") " "
+
+let getopts options ~opt =
+  map_string_matches
+    ~regexp:(f " %s\\(\\.\\|[ =:-]\\|: \\)\\([^ ]+\\) " opt)
+    ~f:(fun () -> Str.matched_group 2 options)
+    options
+
+let getopt options ~opt =
+  options |> getopts ~opt |> List.hd |> Option.value ~default:""
+
+let accumulate_extra_minimizer_arguments options =
+  let extra_args = getopts ~opt:"extra-arg" options in
+  let inline_stdlib = getopt ~opt:"inline-stdlib" options in
+  ( if String.equal inline_stdlib "yes" then Lwt.return ["--inline-coqlib"]
+  else
+    ( if not (String.equal inline_stdlib "") then
+      Lwt_io.printlf
+        "Ignoring invalid option to inline-stdlib '%s' not equal to 'yes'"
+        inline_stdlib
+    else Lwt.return_unit )
+    >>= fun () -> Lwt.return_nil )
+  >>= 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
-    ?base_sha ?head_sha () =
+    ~options ?base_sha ?head_sha () =
+  let options = format_options_for_getopts options in
+  accumulate_extra_minimizer_arguments options
+  >>= fun minimizer_extra_arguments ->
+  Lwt_io.printlf
+    "Parsed options for the bug minimizer at %s/%s#%d from '%s' into \
+     {minimizer_extra_arguments: '%s'}"
+    owner repo pr_number options
+    (String.concat ~sep:" " minimizer_extra_arguments)
+  >>= fun () ->
   fetch_ci_minimization_info ~bot_info ~owner ~repo ~pr_number
     ~head_pipeline_summary ?base_sha ?head_sha ()
   >>= function
@@ -1264,7 +1299,8 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
       >>= fun () ->
       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 ~bug_file_contents
+        ~ci_minimization_infos:jobs_to_minimize ~minimizer_extra_arguments
+        ~bug_file_contents
       >>= fun (jobs_minimized, jobs_that_could_not_be_minimized) ->
       let pluralize word ?plural ls =
         match (ls, plural) with
@@ -1717,7 +1753,7 @@ let minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
         "Error while attempting to find jobs to minimize from PR #%d:\n%s"
         pr_number err
 
-let ci_minimize ~bot_info ~comment_info ~requests ~comment_on_error
+let ci_minimize ~bot_info ~comment_info ~requests ~comment_on_error ~options
     ~bug_file_contents =
   minimize_failed_tests ~bot_info ~owner:comment_info.issue.issue.owner
     ~repo:comment_info.issue.issue.repo ~pr_number:comment_info.issue.number
@@ -1730,7 +1766,7 @@ let ci_minimize ~bot_info ~comment_info ~requests ~comment_on_error
           RequestAll
       | requests ->
           RequestExplicit requests )
-    ~comment_on_error ~bug_file_contents ()
+    ~comment_on_error ~options ~bug_file_contents ()
 
 let pipeline_action ~bot_info pipeline_info ~gitlab_mapping : unit Lwt.t =
   let gitlab_full_name = pipeline_info.project_path in
@@ -1862,7 +1898,7 @@ let pipeline_action ~bot_info pipeline_info ~gitlab_mapping : unit Lwt.t =
               | "coq", "coq", "failed", Some pr_number ->
                   minimize_failed_tests ~bot_info ~owner ~repo ~pr_number
                     ~head_pipeline_summary:(Some summary) ~request:Auto
-                    ~comment_on_error:false ~bug_file_contents:None
+                    ~comment_on_error:false ~options:"" ~bug_file_contents:None
                     ?base_sha:pipeline_info.common_info.base_commit
                     ~head_sha:pipeline_info.common_info.head_commit ()
               | _ ->
@@ -1874,25 +1910,21 @@ type coqbot_minimize_script_data =
 
 let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
     ~owner ~repo ~options =
-  let options =
-    " " ^ options ^ " " |> Str.global_replace (Str.regexp "[\n\r\t]") " "
+  let options = format_options_for_getopts options in
+  let getopt_version opt =
+    options |> getopt ~opt |> Str.replace_first (Str.regexp "^[vV]") ""
   in
-  let getopt opt =
-    if
-      string_match
-        ~regexp:(f " %s\\(\\.\\|[ =:-]\\|: \\)[vV]?\\([^ ]+\\) " opt)
-        options
-    then Str.matched_group 2 options
-    else ""
-  in
-  let coq_version = getopt "[Cc]oq" in
-  let ocaml_version = getopt "[Oo][Cc]aml" in
+  accumulate_extra_minimizer_arguments options
+  >>= fun minimizer_extra_arguments ->
+  let coq_version = getopt_version "[Cc]oq" in
+  let ocaml_version = getopt_version "[Oo][Cc]aml" in
   Lwt_io.printlf
     "Parsed options for the bug minimizer at %s/%s@%s from '%s' into \
-     {coq_version: '%s'; ocaml_version: '%s'}"
+     {coq_version: '%s'; ocaml_version: '%s'; minimizer_extra_arguments: '%s'}"
     owner repo
     (GitHub_ID.to_string comment_thread_id)
     options coq_version ocaml_version
+    (String.concat ~sep:" " minimizer_extra_arguments)
   >>= fun () ->
   ( match script with
   | MinimizeScript {quote_kind; body} ->
@@ -1912,7 +1944,7 @@ let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
   )
   |> fun script ->
   git_coq_bug_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
-    ~owner ~repo ~coq_version ~ocaml_version
+    ~owner ~repo ~coq_version ~ocaml_version ~minimizer_extra_arguments
   >>= function
   | Ok () ->
       GitHub_mutations.post_comment ~id:comment_thread_id
@@ -1972,12 +2004,12 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
       ; pr_number ] -> (
         message |> String.split ~on:'\n'
         |> function
-        | docker_image
-          :: target
-             :: opam_switch
-                :: failing_urls
-                   :: passing_urls :: base :: head :: bug_file_lines ->
-            (let bug_file_contents = String.concat ~sep:"\n" bug_file_lines in
+        | docker_image :: target :: opam_switch :: failing_urls :: passing_urls
+          :: base :: head :: extra_arguments_joined :: bug_file_lines ->
+            (let minimizer_extra_arguments =
+               String.split ~on:' ' extra_arguments_joined
+             in
+             let bug_file_contents = String.concat ~sep:"\n" bug_file_lines in
              fun () ->
                init_git_bare_repository ~bot_info
                >>= fun () ->
@@ -1986,6 +2018,7 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
                  (run_ci_minimization
                     ~comment_thread_id:(GitHub_ID.of_string comment_thread_id)
                     ~owner ~repo ~base ~pr_number ~head
+                    ~minimizer_extra_arguments
                     ~ci_minimization_infos:
                       [ { target
                         ; opam_switch
@@ -2430,7 +2463,7 @@ let run_ci_action ~bot_info ~comment_info ?full_ci ~gitlab_mapping
             Lwt_io.printl "Unauthorized user: doing nothing." |> Lwt_result.ok
           )
     |> Fn.flip Lwt_result.bind_lwt_err (fun err ->
-           Lwt_io.printf "Error: %s\n" err ))
+           Lwt_io.printf "Error: %s\n" err ) )
     >>= fun _ -> Lwt.return_unit )
   |> Lwt.async ;
   Server.respond_string ~status:`OK

diff --git a/src/actions.mli b/src/actions.mli
@@ -87,6 +87,7 @@ val ci_minimize :
   -> comment_info:GitHub_types.comment_info
   -> requests:string list
   -> comment_on_error:bool
+  -> options:string
   -> bug_file_contents:string option
   -> unit Lwt.t
 

diff --git a/src/bot.ml b/src/bot.ml
@@ -105,20 +105,23 @@ let callback _conn req body =
       if
         string_match
           ~regexp:
-            ( f "@%s:? [Cc][Ii][- ][Mm]inimize:?\\([^\n]*\\)"
+            ( f "@%s:?\\( [^\n]*\\)\\b[Cc][Ii][- ][Mm]inimize:?\\([^\n]*\\)"
             @@ Str.quote bot_name )
           body
       then
-        let requests = Str.matched_group 1 body in
-        Some (requests |> parse_minimiation_requests)
+        let options, requests =
+          (Str.matched_group 1 body, Str.matched_group 2 body)
+        in
+        Some (options, requests |> parse_minimiation_requests)
       else None
     in
     let coqbot_resume_ci_minimize_text_of_body body =
       if
         string_match
           ~regexp:
             ( f
-                "@%s:? resume [Cc][Ii][- ][Mm]inimiz\\(e\\|ation\\):?\\([^\n\
+                "@%s:?\\( [^\n\
+                 ]*\\)\\bresume [Cc][Ii][- ][Mm]inimiz\\(e\\|ation\\):?\\([^\n\
                  ]*\\)\n\
                  +```[^\n\
                  ]*\n\
@@ -127,11 +130,15 @@ let callback _conn req body =
             @@ Str.quote bot_name )
           body
       then
-        let requests, body =
-          (Str.matched_group 2 body, Str.matched_group 3 body)
+        let options, requests, body =
+          ( Str.matched_group 1 body
+          , Str.matched_group 3 body
+          , Str.matched_group 4 body )
         in
         Some
-          (requests |> parse_minimiation_requests, body |> extract_minimize_file)
+          ( options
+          , requests |> parse_minimiation_requests
+          , body |> extract_minimize_file )
       else None
     in
     ( coqbot_minimize_text_of_body
@@ -298,34 +305,38 @@ let callback _conn req body =
               Server.respond_string ~status:`OK ~body:"Handling minimization."
                 ()
           | None -> (
-            match coqbot_ci_minimize_text_of_body body with
-            | Some requests ->
+            (* Since both ci minimization resumption and ci
+               minimization will match the resumption string, and we
+               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) ->
                 (fun () ->
                   init_git_bare_repository ~bot_info
                   >>= fun () ->
                   action_as_github_app ~bot_info ~key ~app_id
                     ~owner:comment_info.issue.issue.owner
                     ~repo:comment_info.issue.issue.repo
                     (ci_minimize ~comment_info ~requests ~comment_on_error:true
-                       ~bug_file_contents:None ) )
+                       ~options ~bug_file_contents:(Some bug_file_contents) ) )
                 |> Lwt.async ;
                 Server.respond_string ~status:`OK
-                  ~body:"Handling CI minimization." ()
+                  ~body:"Handling CI minimization resumption." ()
             | None -> (
-              match coqbot_resume_ci_minimize_text_of_body body with
-              | Some (requests, bug_file_contents) ->
+              match coqbot_ci_minimize_text_of_body body with
+              | Some (options, requests) ->
                   (fun () ->
                     init_git_bare_repository ~bot_info
                     >>= fun () ->
                     action_as_github_app ~bot_info ~key ~app_id
                       ~owner:comment_info.issue.issue.owner
                       ~repo:comment_info.issue.issue.repo
                       (ci_minimize ~comment_info ~requests
-                         ~comment_on_error:true
-                         ~bug_file_contents:(Some bug_file_contents) ) )
+                         ~comment_on_error:true ~options ~bug_file_contents:None )
+                    )
                   |> Lwt.async ;
                   Server.respond_string ~status:`OK
-                    ~body:"Handling CI minimization resumption." ()
+                    ~body:"Handling CI minimization." ()
               | None ->
                   if
                     string_match

diff --git a/src/git_utils.ml b/src/git_utils.ml
@@ -130,7 +130,7 @@ let git_test_modified ~base ~head pattern =
       Error (f "%s stopped by signal %d." command signal)
 
 let git_coq_bug_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
-    ~owner ~repo ~coq_version ~ocaml_version =
+    ~owner ~repo ~coq_version ~ocaml_version ~minimizer_extra_arguments =
   (* To push a new branch we need to identify as coqbot the GitHub
      user, who is a collaborator on the run-coq-bug-minimizer repo,
      not coqbot the GitHub App *)
@@ -144,12 +144,13 @@ let git_coq_bug_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
     ; owner
     ; repo
     ; coq_version
-    ; ocaml_version ]
+    ; ocaml_version
+    ; minimizer_extra_arguments |> String.concat ~sep:" " ]
   |> execute_cmd
 
 let git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
     ~docker_image ~target ~opam_switch ~failing_urls ~passing_urls ~base ~head
-    ~bug_file_name =
+    ~minimizer_extra_arguments ~bug_file_name =
   (* To push a new branch we need to identify as coqbot the GitHub
      user, who is a collaborator on the run-coq-bug-minimizer repo,
      not coqbot the GitHub App *)
@@ -166,7 +167,8 @@ let git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
     ; failing_urls
     ; passing_urls
     ; base
-    ; head ]
+    ; head
+    ; minimizer_extra_arguments |> String.concat ~sep:" " ]
   @
   match bug_file_name with Some bug_file_name -> [bug_file_name] | None -> [] )
   |> Stdlib.Filename.quote_command "./run_ci_minimization.sh"