From d34d2b77ea135fe6ca7ced2e164586cc980fb3d4 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Thu, 30 Jul 2026 11:17:45 +0200
Subject: [PATCH 01/14] Restructure comment parsing

This change technically changes the semantics of the matching because
the new algorithm commits to a `Some` branch before it checks
permissions and other conditions. If those fail, we go directly to the
failure case instead of trying to parse other commands.
---
 src/webhooks/github.ml | 267 +++++++++++++++++++++++------------------
 1 file changed, 151 insertions(+), 116 deletions(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 9fac3441..17265a71 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -90,125 +90,160 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
                 "https://github.com/rocq-community/run-coq-bug-minimizer/actions" ) )
       |> Lwt.async ;
       Server.respond_string ~status:`OK ~body:"Handling minimization." ()
-  | None -> (
-    (* 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 resume_ci_minimize_text_of_body body with
-    | Some (options, requests, bug_file) ->
-        (fun () ->
-          init_git_bare_repository ~bot_info
-          >>= fun () ->
-          Bot_components.Github_installations.action_as_github_app ~bot_info
-            ~key ~app_id ~owner:comment_info.issue.issue.owner (fun ~bot_info ->
+  | None ->
+
+    let parse_run_ci body =
+      if string_match
+        ~regexp:
+          ( f "@%s:? [Rr]un \\(full\\|light\\|\\) ?[Cc][Ii]"
+            @@ Str.quote github_bot_name )
+        body
+      then
+        let full_ci =
+          match Str.matched_group 1 body with
+          | "full" -> Some true
+          | "light" -> Some false
+          | "" -> None
+          | _ -> failwith "Impossible group value."
+        in
+        Some (`RunCI full_ci)
+      else
+        None
+    in
+   let parse_merge body =
+     if string_match
+       ~regexp:(f "@%s:? [Mm]erge now" @@ Str.quote github_bot_name)
+       body
+     then
+       Some `Merge
+     else
+       None
+    in
+
+    let parse_bench_native body =
+      if
+        string_match
+          ~regexp:(f "@%s:? [Bb]ench native" @@ Str.quote github_bot_name)
+          body
+      then
+        Some `BenchNative
+      else
+        None
+    in
+
+    let parse_bench body =
+      if
+        string_match
+          ~regexp:(f "@%s:? [Bb]ench" @@ Str.quote github_bot_name)
+          body
+      then
+        Some `Bench
+      else
+        None
+    in
+    let parse () =
+      let open Option in
+      let rec first_success body fns =
+        match fns with
+        | fn :: fns ->
+          let res = fn body in
+          if Option.is_some res then res else first_success body fns
+        | [] -> None
+      in
+    (* 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 *)
+      first_success body [
+        (fun body -> resume_ci_minimize_text_of_body body >>| fun x -> `ResumeMinimize x);
+        (fun body -> ci_minimize_text_of_body body >>| fun x -> `Minimize x);
+        parse_run_ci;
+        parse_merge;
+        parse_bench_native;
+        parse_bench
+      ]
+    in
+    match parse () with
+    | Some (`ResumeMinimize (options, requests, bug_file)) ->
+      (fun () ->
+        init_git_bare_repository ~bot_info
+        >>= fun () ->
+        Bot_components.Github_installations.action_as_github_app ~bot_info
+          ~key ~app_id ~owner:comment_info.issue.issue.owner (fun ~bot_info ->
+            Minimization.ci_minimize ~bot_info ~comment_info ~requests
+              ~comment_on_error:true ~options ~bug_file:(Some bug_file) ) )
+      |> Lwt.async ;
+      Server.respond_string ~status:`OK
+        ~body:"Handling CI minimization resumption." ()
+    | Some (`Minimize (options, requests)) ->
+      (fun () ->
+         init_git_bare_repository ~bot_info
+         >>= fun () ->
+         Bot_components.Github_installations.action_as_github_app ~bot_info
+           ~key ~app_id ~owner:comment_info.issue.issue.owner
+           (fun ~bot_info ->
               Minimization.ci_minimize ~bot_info ~comment_info ~requests
-                ~comment_on_error:true ~options ~bug_file:(Some bug_file) ) )
-        |> Lwt.async ;
-        Server.respond_string ~status:`OK
-          ~body:"Handling CI minimization resumption." ()
-    | None -> (
-      match ci_minimize_text_of_body body with
-      | Some (options, requests) ->
-          (fun () ->
-            init_git_bare_repository ~bot_info
-            >>= fun () ->
-            Bot_components.Github_installations.action_as_github_app ~bot_info
-              ~key ~app_id ~owner:comment_info.issue.issue.owner
-              (fun ~bot_info ->
-                Minimization.ci_minimize ~bot_info ~comment_info ~requests
-                  ~comment_on_error:true ~options ~bug_file:None ) )
-          |> Lwt.async ;
-          Server.respond_string ~status:`OK ~body:"Handling CI minimization." ()
-      | None ->
-          if
-            string_match
-              ~regexp:
-                ( f "@%s:? [Rr]un \\(full\\|light\\|\\) ?[Cc][Ii]"
-                @@ Str.quote github_bot_name )
-              body
-            && comment_info.issue.pull_request
-            && String.equal comment_info.issue.issue.owner "rocq-prover"
-            && String.equal comment_info.issue.issue.repo "rocq"
-            && Option.is_some install_id
-          then
-            let full_ci =
-              match Str.matched_group 1 body with
-              | "full" ->
-                  Some true
-              | "light" ->
-                  Some false
-              | "" ->
-                  None
-              | _ ->
-                  failwith "Impossible group value."
-            in
-            init_git_bare_repository ~bot_info
-            >>= fun () ->
-            Bot_components.Github_installations.action_as_github_app ~bot_info
-              ~key ~app_id ~owner:comment_info.issue.issue.owner
-              (Pr_sync.run_ci_action ~comment_info ?full_ci ~gitlab_mapping
-                 ~github_mapping () )
-          else if
-            string_match
-              ~regexp:(f "@%s:? [Mm]erge now" @@ Str.quote github_bot_name)
-              body
-            && comment_info.issue.pull_request
-            && String.equal comment_info.issue.issue.owner "rocq-prover"
-            && String.equal comment_info.issue.issue.repo "rocq"
-            && Option.is_some install_id
-          then (
-            (fun () ->
-              Bot_components.Github_installations.action_as_github_app ~bot_info
-                ~key ~app_id ~owner:comment_info.issue.issue.owner
-                (fun ~bot_info ->
-                  GitHub_automation.merge_pull_request_action ~bot_info
-                    comment_info ) )
-            |> Lwt.async ;
-            Server.respond_string ~status:`OK
-              ~body:(f "Received a request to merge the PR.")
-              () )
-          else if
-            string_match
-              ~regexp:(f "@%s:? [Bb]ench native" @@ Str.quote github_bot_name)
-              body
-            && comment_info.issue.pull_request
-            && String.equal comment_info.issue.issue.owner "rocq-prover"
-            && String.equal comment_info.issue.issue.repo "rocq"
-            && Option.is_some install_id
-          then (
-            (fun () ->
-              Bot_components.Github_installations.action_as_github_app ~bot_info
-                ~key ~app_id ~owner:comment_info.issue.issue.owner
-                (fun ~bot_info ->
-                  Bench.run_bench ~bot_info
-                    ~key_value_pairs:[("coq_native", "yes")]
-                    comment_info ) )
-            |> Lwt.async ;
-            Server.respond_string ~status:`OK
-              ~body:(f "Received a request to start the bench.")
-              () )
-          else if
-            string_match
-              ~regexp:(f "@%s:? [Bb]ench" @@ Str.quote github_bot_name)
-              body
-            && comment_info.issue.pull_request
+                ~comment_on_error:true ~options ~bug_file:None ) )
+      |> Lwt.async ;
+      Server.respond_string ~status:`OK ~body:"Handling CI minimization." ()
+    | Some (`RunCI full_ci) when
+        comment_info.issue.pull_request
+        && String.equal comment_info.issue.issue.owner "rocq-prover"
+        && String.equal comment_info.issue.issue.repo "rocq"
+        && Option.is_some install_id ->
+      init_git_bare_repository ~bot_info
+      >>= fun () ->
+      Bot_components.Github_installations.action_as_github_app ~bot_info
+        ~key ~app_id ~owner:comment_info.issue.issue.owner
+        (Pr_sync.run_ci_action ~comment_info ?full_ci ~gitlab_mapping
+           ~github_mapping () )
+    | Some `Merge when
+        comment_info.issue.pull_request
+        && String.equal comment_info.issue.issue.owner "rocq-prover"
+        && String.equal comment_info.issue.issue.repo "rocq"
+        && Option.is_some install_id ->
+      (fun () ->
+         Bot_components.Github_installations.action_as_github_app ~bot_info
+           ~key ~app_id ~owner:comment_info.issue.issue.owner
+           (fun ~bot_info ->
+              GitHub_automation.merge_pull_request_action ~bot_info
+                comment_info ) )
+      |> Lwt.async ;
+      Server.respond_string ~status:`OK
+        ~body:(f "Received a request to merge the PR.")
+        ()
+    | Some `BenchNative when
+        comment_info.issue.pull_request
+        && String.equal comment_info.issue.issue.owner "rocq-prover"
+        && String.equal comment_info.issue.issue.repo "rocq"
+        && Option.is_some install_id ->
+      (fun () ->
+         Bot_components.Github_installations.action_as_github_app ~bot_info
+           ~key ~app_id ~owner:comment_info.issue.issue.owner
+           (fun ~bot_info ->
+              Bench.run_bench ~bot_info
+                ~key_value_pairs:[("coq_native", "yes")]
+                comment_info ) )
+      |> Lwt.async ;
+      Server.respond_string ~status:`OK
+        ~body:(f "Received a request to start the bench.")
+        ()
+    | Some `Bench when
+            comment_info.issue.pull_request
             && String.equal comment_info.issue.issue.owner "rocq-prover"
             && String.equal comment_info.issue.issue.repo "rocq"
-            && Option.is_some install_id
-          then (
-            (fun () ->
-              Bot_components.Github_installations.action_as_github_app ~bot_info
-                ~key ~app_id ~owner:comment_info.issue.issue.owner
-                (fun ~bot_info -> Bench.run_bench ~bot_info comment_info ) )
-            |> Lwt.async ;
-            Server.respond_string ~status:`OK
-              ~body:(f "Received a request to start the bench.")
-              () )
-          else
-            Server.respond_string ~status:`OK
-              ~body:(f "Unhandled comment: %s" body)
-              () ) )
+            && Option.is_some install_id ->
+      (fun () ->
+         Bot_components.Github_installations.action_as_github_app ~bot_info
+           ~key ~app_id ~owner:comment_info.issue.issue.owner
+           (fun ~bot_info -> Bench.run_bench ~bot_info comment_info ) )
+      |> Lwt.async ;
+      Server.respond_string ~status:`OK
+        ~body:(f "Received a request to start the bench.")
+        ()
+    | _ ->
+      Server.respond_string ~status:`OK
+        ~body:(f "Unhandled comment: %s" body)
+        ()
 
 let handle_github_webhook ~bot_info ~key ~app_id ~github_bot_name
     ~gitlab_mapping ~github_mapping ~repo_config_table ~github_webhook_secret

From d96054e8a4968d97a6702b865dcaecd4e5f70fce Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Thu, 30 Jul 2026 12:12:04 +0200
Subject: [PATCH 02/14] Add bench argument parsers

---
 bot-components/utils/String_utils.ml  | 104 +++++++++++++++++++++
 bot-components/utils/String_utils.mli |  16 ++++
 tests/test_string_utils.ml            | 125 ++++++++++++++++++++++++++
 3 files changed, 245 insertions(+)

diff --git a/bot-components/utils/String_utils.ml b/bot-components/utils/String_utils.ml
index 0ea0bc13..489bb160 100644
--- a/bot-components/utils/String_utils.ml
+++ b/bot-components/utils/String_utils.ml
@@ -48,6 +48,110 @@ let first_line_of_string s =
 let remove_between s i j =
   String.sub ~pos:0 ~len:i s ^ String.sub s ~pos:j ~len:(String.length s - j)
 
+let split_shell_words ~preserve_syntax input =
+  let is_whitespace = function
+    | ' ' | '\t' | '\n' | '\r' | '\011' | '\012' ->
+        true
+    | _ ->
+        false
+  in
+  let buffer = Buffer.create (String.length input) in
+  let add_syntax char = if preserve_syntax then Buffer.add_char buffer char in
+  let finish_token token_started tokens =
+    if token_started then Buffer.contents buffer :: tokens else tokens
+  in
+  let length = String.length input in
+  let rec split index quote token_started tokens =
+    if index = length then
+      match quote with
+      | Some delimiter ->
+          Error (Printf.sprintf "unterminated %c quote" delimiter)
+      | None ->
+          Ok (List.rev (finish_token token_started tokens))
+    else
+      let char = input.[index] in
+      match quote with
+      | None when is_whitespace char ->
+          let tokens = finish_token token_started tokens in
+          Buffer.clear buffer ;
+          split (index + 1) None false tokens
+      | None when Char.equal char '\\' ->
+          if index + 1 = length then Error "trailing escape character"
+          else
+            let escaped = input.[index + 1] in
+            if Char.equal escaped '\n' then
+              split (index + 2) None token_started tokens
+            else (
+              add_syntax char ;
+              Buffer.add_char buffer escaped ;
+              split (index + 2) None true tokens )
+      | None when Char.equal char '\'' || Char.equal char '"' ->
+          add_syntax char ;
+          split (index + 1) (Some char) true tokens
+      | None ->
+          Buffer.add_char buffer char ;
+          split (index + 1) None true tokens
+      | Some '\'' when Char.equal char '\'' ->
+          add_syntax char ;
+          split (index + 1) None true tokens
+      | Some '\'' ->
+          Buffer.add_char buffer char ;
+          split (index + 1) quote true tokens
+      | Some '"' when Char.equal char '"' ->
+          add_syntax char ;
+          split (index + 1) None true tokens
+      | Some '"' when Char.equal char '\\' ->
+          if index + 1 = length then Error "unterminated \" quote"
+          else
+            let escaped = input.[index + 1] in
+            if Char.equal escaped '\n' then
+              split (index + 2) quote true tokens
+            else if
+              List.mem ['"'; '\\'; '$'; '`'] escaped ~equal:Char.equal
+            then (
+              add_syntax char ;
+              Buffer.add_char buffer escaped ;
+              split (index + 2) quote true tokens )
+            else (
+              Buffer.add_char buffer char ;
+              split (index + 1) quote true tokens )
+      | Some '"' ->
+          Buffer.add_char buffer char ;
+          split (index + 1) quote true tokens
+      | Some _ ->
+          failwith "unsupported quote delimiter"
+  in
+  split 0 None false []
+
+let split_on_unquoted_whitespace input =
+  split_shell_words ~preserve_syntax:true input
+
+let parse_key_value_arguments input =
+  match split_shell_words ~preserve_syntax:false input with
+  | Error _ as error ->
+      error
+  | Ok arguments ->
+      let rec parse parsed = function
+        | [] ->
+            Ok (List.rev parsed)
+        | argument :: arguments -> (
+          match Stdlib.String.index_opt argument '=' with
+          | None when String.is_empty argument ->
+              Error (Printf.sprintf "argument %S has an empty key" argument)
+          | None ->
+              parse ((argument, None) :: parsed) arguments
+          | Some 0 ->
+              Error (Printf.sprintf "argument %S has an empty key" argument)
+          | Some separator ->
+              let key = String.sub argument ~pos:0 ~len:separator in
+              let value =
+                String.sub argument ~pos:(separator + 1)
+                  ~len:(String.length argument - separator - 1)
+              in
+              parse ((key, Some value) :: parsed) arguments )
+      in
+      parse [] arguments
+
 (******************************************************************************)
 (* Formatting Functions                                                       *)
 (******************************************************************************)
diff --git a/bot-components/utils/String_utils.mli b/bot-components/utils/String_utils.mli
index 05e27c4e..450f44ad 100644
--- a/bot-components/utils/String_utils.mli
+++ b/bot-components/utils/String_utils.mli
@@ -23,6 +23,22 @@ val first_line_of_string : string -> string
 
 val remove_between : string -> int -> int -> string
 
+(** [split_on_unquoted_whitespace input] splits [input] at ASCII whitespace
+    outside single or double quotes. Shell quote and escape syntax is recognized
+    and preserved in the returned tokens.
+
+    Returns an error for an unterminated quote or a trailing backslash. *)
+val split_on_unquoted_whitespace : string -> (string list, string) Result.t
+
+(** [parse_key_value_arguments input] parses shell-style [key=value] words.
+    Quote and escape syntax is consumed. A missing equal sign produces a [None]
+    value; an equal sign produces [Some value], including [Some ""] for an
+    explicitly empty value. Values may contain additional equal signs.
+
+    Returns an error if quoting is malformed or an argument has an empty key. *)
+val parse_key_value_arguments :
+  string -> ((string * string option) list, string) Result.t
+
 (* ========================================================================== *)
 (* Formatting Functions *)
 (* ========================================================================== *)
diff --git a/tests/test_string_utils.ml b/tests/test_string_utils.ml
index 7a7fb3a7..c8ebaa6a 100644
--- a/tests/test_string_utils.ml
+++ b/tests/test_string_utils.ml
@@ -1,4 +1,6 @@
 open Alcotest
+open Base
+open String_utils
 
 let test_strip_quoted_bot_name () =
   let input =
@@ -16,3 +18,126 @@ let () =
   run "String_utils tests"
     [ ( "strip_quoted_bot_name"
       , [test_case "quoted bot name" `Quick test_strip_quoted_bot_name] ) ]
+
+let tokens = Alcotest.list Alcotest.string
+let key_values =
+  Alcotest.list (Alcotest.pair Alcotest.string (Alcotest.option Alcotest.string))
+
+let check_split ~input ~expected () =
+  match split_on_unquoted_whitespace input with
+  | Ok actual ->
+      Alcotest.check tokens input expected actual
+  | Error error ->
+      Alcotest.failf "expected %S to parse, but got: %s" input error
+
+let check_split_error ~input ~expected () =
+  match split_on_unquoted_whitespace input with
+  | Error actual ->
+      Alcotest.(check string) input expected actual
+  | Ok actual ->
+      Alcotest.failf "expected %S to fail, but got: [%s]" input
+        (String.concat ~sep:"; " actual)
+
+let check_arguments ~input ~expected () =
+  match parse_key_value_arguments input with
+  | Ok actual ->
+      Alcotest.check key_values input expected actual
+  | Error error ->
+      Alcotest.failf "expected %S to parse, but got: %s" input error
+
+let check_argument_error ~input ~expected () =
+  match parse_key_value_arguments input with
+  | Error actual ->
+      Alcotest.(check string) input expected actual
+  | Ok _ ->
+      Alcotest.failf "expected %S to fail" input
+
+let () =
+  Alcotest.run "String_utils tests"
+    [ ( "split_on_unquoted_whitespace"
+      , [ ( "empty input"
+          , `Quick
+          , check_split ~input:"" ~expected:[] )
+        ; ( "unquoted arguments"
+          , `Quick
+          , check_split ~input:"x=foo y=true" ~expected:["x=foo"; "y=true"] )
+        ; ( "double-quoted whitespace"
+          , `Quick
+          , check_split ~input:{|x="foo bar" y=true|}
+              ~expected:[{|x="foo bar"|}; "y=true"] )
+        ; ( "single-quoted whitespace"
+          , `Quick
+          , check_split ~input:"x='foo bar' y=true"
+              ~expected:["x='foo bar'"; "y=true"] )
+        ; ( "repeated whitespace"
+          , `Quick
+          , check_split ~input:"  x=foo\t\ty=true  "
+              ~expected:["x=foo"; "y=true"] )
+        ; ( "escaped quote"
+          , `Quick
+          , check_split ~input:{|x="foo \"bar\" baz" y=true|}
+              ~expected:[{|x="foo \"bar\" baz"|}; "y=true"] )
+        ; ( "escaped whitespace"
+          , `Quick
+          , check_split ~input:{|x=foo\ bar y=true|}
+              ~expected:[{|x=foo\ bar|}; "y=true"] )
+        ; ( "empty quoted arguments"
+          , `Quick
+          , check_split ~input:{|"" ''|} ~expected:[{|""|}; "''"] )
+        ; ( "unterminated double quote"
+          , `Quick
+          , check_split_error ~input:{|x="foo bar|}
+              ~expected:"unterminated \" quote" )
+        ; ( "trailing escape"
+          , `Quick
+          , check_split_error ~input:{|x=foo\|}
+              ~expected:"trailing escape character" ) ] )
+    ; ( "parse_key_value_arguments"
+      , [ ( "quoted value"
+          , `Quick
+          , check_arguments ~input:{|x="foo bar" y=true|}
+              ~expected:[("x", Some "foo bar"); ("y", Some "true")] )
+        ; ( "single-quoted value"
+          , `Quick
+          , check_arguments ~input:"x='foo bar' y=true"
+              ~expected:[("x", Some "foo bar"); ("y", Some "true")] )
+        ; ( "concatenated quoted text"
+          , `Quick
+          , check_arguments ~input:{|x=foo" bar" y='true'|}
+              ~expected:[("x", Some "foo bar"); ("y", Some "true")] )
+        ; ( "quoted whole argument"
+          , `Quick
+          , check_arguments ~input:{|"x=foo bar" y=true|}
+              ~expected:[("x", Some "foo bar"); ("y", Some "true")] )
+        ; ( "escaped whitespace"
+          , `Quick
+          , check_arguments ~input:{|x=foo\ bar y=true|}
+              ~expected:[("x", Some "foo bar"); ("y", Some "true")] )
+        ; ( "escaped quote"
+          , `Quick
+          , check_arguments ~input:{|x="foo \"bar\""|}
+              ~expected:[("x", Some {|foo "bar"|})] )
+        ; ( "literal nested quotes"
+          , `Quick
+          , check_arguments ~input:{|x='"foo bar"'|}
+              ~expected:[("x", Some {|"foo bar"|})] )
+        ; ( "explicit empty values"
+          , `Quick
+          , check_arguments ~input:{|x= y=""|}
+              ~expected:[("x", Some ""); ("y", Some "")] )
+        ; ( "additional equal signs"
+          , `Quick
+          , check_arguments ~input:"x=foo=bar"
+              ~expected:[("x", Some "foo=bar")] )
+        ; ( "missing value"
+          , `Quick
+          , check_arguments ~input:"x=foo missing"
+              ~expected:[("x", Some "foo"); ("missing", None)] )
+        ; ( "empty key"
+          , `Quick
+          , check_argument_error ~input:"=value"
+              ~expected:"argument \"=value\" has an empty key" )
+        ; ( "empty quoted key"
+          , `Quick
+          , check_argument_error ~input:{|""|}
+              ~expected:"argument \"\" has an empty key" ) ] ) ]

From b206c44e4c5ec65ac8a24c2ea59280ec84d8f550 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Thu, 30 Jul 2026 12:15:56 +0200
Subject: [PATCH 03/14] Merge `bench` commands; accept extra job arguments to
 `bench` command

This means instead of `bench native` we now have to write `bench coq_native`.
This works because arguments keys without values are mapped to `"yes"`
values.
---
 src/webhooks/github.ml | 30 ++++++++++++++----------------
 1 file changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 17265a71..8ffe7eeb 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -120,24 +120,18 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
        None
     in
 
-    let parse_bench_native body =
-      if
-        string_match
-          ~regexp:(f "@%s:? [Bb]ench native" @@ Str.quote github_bot_name)
-          body
-      then
-        Some `BenchNative
-      else
-        None
-    in
-
     let parse_bench body =
       if
         string_match
-          ~regexp:(f "@%s:? [Bb]ench" @@ Str.quote github_bot_name)
+          ~regexp:(f {|@%s:? [Bb]ench\( *$\| +\([^\n]+\) *\(\n\|$\)\)|} @@ Str.quote github_bot_name)
           body
       then
-        Some `Bench
+        match Str.matched_group 2 body with
+        | exception _ -> Some (`Bench [])
+        | args ->
+          match parse_key_value_arguments args with
+          | Result.Ok args -> Some (`Bench args)
+          | _ -> None
       else
         None
     in
@@ -158,7 +152,6 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
         (fun body -> ci_minimize_text_of_body body >>| fun x -> `Minimize x);
         parse_run_ci;
         parse_merge;
-        parse_bench_native;
         parse_bench
       ]
     in
@@ -227,15 +220,20 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
       Server.respond_string ~status:`OK
         ~body:(f "Received a request to start the bench.")
         ()
-    | Some `Bench when
+    | Some (`Bench args) when
             comment_info.issue.pull_request
             && String.equal comment_info.issue.issue.owner "rocq-prover"
             && String.equal comment_info.issue.issue.repo "rocq"
             && Option.is_some install_id ->
+      let key_value_pairs = List.map ~f:(fun (k,v) -> (k, Option.value ~default:"yes" v)) args in
       (fun () ->
          Bot_components.Github_installations.action_as_github_app ~bot_info
            ~key ~app_id ~owner:comment_info.issue.issue.owner
-           (fun ~bot_info -> Bench.run_bench ~bot_info comment_info ) )
+           (fun ~bot_info ->
+              Bench.run_bench ~bot_info
+                ~key_value_pairs
+                comment_info )
+      )
       |> Lwt.async ;
       Server.respond_string ~status:`OK
         ~body:(f "Received a request to start the bench.")

From e43775f05039d24fafd10516d787f11b44b50533 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 11:48:42 +0200
Subject: [PATCH 04/14] Use ADT for command parsing output; remove BenchNative
 branch

---
 src/webhooks/github.ml | 52 ++++++++++++++++++++----------------------
 1 file changed, 25 insertions(+), 27 deletions(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 8ffe7eeb..57701496 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -65,6 +65,20 @@ let handle_push_event_for_repos ~bot_info ~key ~app_id ~install_id ~owner ~repo
   | _ ->
       Server.respond_string ~status:`OK ~body:"Ignoring push event." ()
 
+module Commands = struct
+
+  type bench_args = (string * string option) list
+
+  type t =
+    | RunCI of { full_ci : bool option }
+    | Merge
+    | Bench of bench_args
+    | ResumeMinimize of (string * string list * Minimize_parser.minimize_parsed)
+    | Minimize of (string * string list)
+end
+
+open Commands
+
 (* Handles all comment-related events (minimization, CI commands, bench commands, etc.)*)
 let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
     ~gitlab_mapping ~github_mapping ~install_id
@@ -106,7 +120,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
           | "" -> None
           | _ -> failwith "Impossible group value."
         in
-        Some (`RunCI full_ci)
+        Some (RunCI {full_ci})
       else
         None
     in
@@ -115,7 +129,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
        ~regexp:(f "@%s:? [Mm]erge now" @@ Str.quote github_bot_name)
        body
      then
-       Some `Merge
+       Some Merge
      else
        None
     in
@@ -127,10 +141,10 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
           body
       then
         match Str.matched_group 2 body with
-        | exception _ -> Some (`Bench [])
+        | exception _ -> Some (Bench [])
         | args ->
           match parse_key_value_arguments args with
-          | Result.Ok args -> Some (`Bench args)
+          | Result.Ok args -> Some (Bench args)
           | _ -> None
       else
         None
@@ -148,15 +162,15 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
        resumption string, and we don't want to parse "resume" as an option, we
        test resumption first *)
       first_success body [
-        (fun body -> resume_ci_minimize_text_of_body body >>| fun x -> `ResumeMinimize x);
-        (fun body -> ci_minimize_text_of_body body >>| fun x -> `Minimize x);
+        (fun body -> resume_ci_minimize_text_of_body body >>| fun x -> ResumeMinimize x);
+        (fun body -> ci_minimize_text_of_body body >>| fun x -> Minimize x);
         parse_run_ci;
         parse_merge;
         parse_bench
       ]
     in
     match parse () with
-    | Some (`ResumeMinimize (options, requests, bug_file)) ->
+    | Some (ResumeMinimize (options, requests, bug_file)) ->
       (fun () ->
         init_git_bare_repository ~bot_info
         >>= fun () ->
@@ -167,7 +181,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
       |> Lwt.async ;
       Server.respond_string ~status:`OK
         ~body:"Handling CI minimization resumption." ()
-    | Some (`Minimize (options, requests)) ->
+    | Some (Minimize (options, requests)) ->
       (fun () ->
          init_git_bare_repository ~bot_info
          >>= fun () ->
@@ -178,7 +192,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
                 ~comment_on_error:true ~options ~bug_file:None ) )
       |> Lwt.async ;
       Server.respond_string ~status:`OK ~body:"Handling CI minimization." ()
-    | Some (`RunCI full_ci) when
+    | Some (RunCI {full_ci}) when
         comment_info.issue.pull_request
         && String.equal comment_info.issue.issue.owner "rocq-prover"
         && String.equal comment_info.issue.issue.repo "rocq"
@@ -189,7 +203,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
         ~key ~app_id ~owner:comment_info.issue.issue.owner
         (Pr_sync.run_ci_action ~comment_info ?full_ci ~gitlab_mapping
            ~github_mapping () )
-    | Some `Merge when
+    | Some Merge when
         comment_info.issue.pull_request
         && String.equal comment_info.issue.issue.owner "rocq-prover"
         && String.equal comment_info.issue.issue.repo "rocq"
@@ -204,23 +218,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
       Server.respond_string ~status:`OK
         ~body:(f "Received a request to merge the PR.")
         ()
-    | Some `BenchNative when
-        comment_info.issue.pull_request
-        && String.equal comment_info.issue.issue.owner "rocq-prover"
-        && String.equal comment_info.issue.issue.repo "rocq"
-        && Option.is_some install_id ->
-      (fun () ->
-         Bot_components.Github_installations.action_as_github_app ~bot_info
-           ~key ~app_id ~owner:comment_info.issue.issue.owner
-           (fun ~bot_info ->
-              Bench.run_bench ~bot_info
-                ~key_value_pairs:[("coq_native", "yes")]
-                comment_info ) )
-      |> Lwt.async ;
-      Server.respond_string ~status:`OK
-        ~body:(f "Received a request to start the bench.")
-        ()
-    | Some (`Bench args) when
+    | Some (Bench args) when
             comment_info.issue.pull_request
             && String.equal comment_info.issue.issue.owner "rocq-prover"
             && String.equal comment_info.issue.issue.repo "rocq"

From f8cd5d226e4f384bae1d9e16b63543c66f191f3c Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 11:54:06 +0200
Subject: [PATCH 05/14] Distinguish unknown commands from permission failures

---
 src/webhooks/github.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 57701496..5ef54307 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -236,7 +236,11 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
       Server.respond_string ~status:`OK
         ~body:(f "Received a request to start the bench.")
         ()
-    | _ ->
+    | Some (RunCI _ | Merge | Bench _) ->
+      Server.respond_string ~status:`OK
+        ~body:"Command recognized but not allowed in this context."
+        ()
+    | None ->
       Server.respond_string ~status:`OK
         ~body:(f "Unhandled comment: %s" body)
         ()

From a757d05f461fbdb53bfc402b64eebd517b73c23f Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 11:56:30 +0200
Subject: [PATCH 06/14] Use `List.find_map` instead of custom `first_success`
 helper

---
 src/webhooks/github.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 5ef54307..3f135f37 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -151,17 +151,10 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
     in
     let parse () =
       let open Option in
-      let rec first_success body fns =
-        match fns with
-        | fn :: fns ->
-          let res = fn body in
-          if Option.is_some res then res else first_success body fns
-        | [] -> None
-      in
     (* 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 *)
-      first_success body [
+      List.find_map ~f:(fun fn -> fn body) [
         (fun body -> resume_ci_minimize_text_of_body body >>| fun x -> ResumeMinimize x);
         (fun body -> ci_minimize_text_of_body body >>| fun x -> Minimize x);
         parse_run_ci;

From 8166dfcf4889bc44ede4b879e0e751314fdfb4ed Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 11:59:50 +0200
Subject: [PATCH 07/14] Test opam package parsing for the bench command

---
 tests/test_string_utils.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/test_string_utils.ml b/tests/test_string_utils.ml
index c8ebaa6a..723923ce 100644
--- a/tests/test_string_utils.ml
+++ b/tests/test_string_utils.ml
@@ -140,4 +140,10 @@ let () =
         ; ( "empty quoted key"
           , `Quick
           , check_argument_error ~input:{|""|}
-              ~expected:"argument \"\" has an empty key" ) ] ) ]
+              ~expected:"argument \"\" has an empty key" )
+        ; ( "coq_opam_packages"
+          , `Quick
+          , check_arguments
+              ~input:{|coq_opam_packages="a b c" coq_native|}
+              ~expected:[("coq_opam_packages", Some "a b c"); ("coq_native", None)])
+        ] ) ]

From 1c015400c67d0bcc476c863375147b8cf96fa002 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 12:04:21 +0200
Subject: [PATCH 08/14] Use ADT for quote state

---
 bot-components/utils/String_utils.ml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/bot-components/utils/String_utils.ml b/bot-components/utils/String_utils.ml
index 489bb160..83d7813a 100644
--- a/bot-components/utils/String_utils.ml
+++ b/bot-components/utils/String_utils.ml
@@ -48,6 +48,8 @@ let first_line_of_string s =
 let remove_between s i j =
   String.sub ~pos:0 ~len:i s ^ String.sub s ~pos:j ~len:(String.length s - j)
 
+type quote = Single | Double
+
 let split_shell_words ~preserve_syntax input =
   let is_whitespace = function
     | ' ' | '\t' | '\n' | '\r' | '\011' | '\012' ->
@@ -65,7 +67,7 @@ let split_shell_words ~preserve_syntax input =
     if index = length then
       match quote with
       | Some delimiter ->
-          Error (Printf.sprintf "unterminated %c quote" delimiter)
+          Error (Printf.sprintf "unterminated %c quote" (match delimiter with Single -> '\'' | Double -> '"'))
       | None ->
           Ok (List.rev (finish_token token_started tokens))
     else
@@ -85,22 +87,25 @@ let split_shell_words ~preserve_syntax input =
               add_syntax char ;
               Buffer.add_char buffer escaped ;
               split (index + 2) None true tokens )
-      | None when Char.equal char '\'' || Char.equal char '"' ->
+      | None when Char.equal char '\'' ->
+          add_syntax char ;
+          split (index + 1) (Some Single) true tokens
+      | None when Char.equal char '"' ->
           add_syntax char ;
-          split (index + 1) (Some char) true tokens
+          split (index + 1) (Some Double) true tokens
       | None ->
           Buffer.add_char buffer char ;
           split (index + 1) None true tokens
-      | Some '\'' when Char.equal char '\'' ->
+      | Some Single when Char.equal char '\'' ->
           add_syntax char ;
           split (index + 1) None true tokens
-      | Some '\'' ->
+      | Some Single ->
           Buffer.add_char buffer char ;
           split (index + 1) quote true tokens
-      | Some '"' when Char.equal char '"' ->
+      | Some Double when Char.equal char '"' ->
           add_syntax char ;
           split (index + 1) None true tokens
-      | Some '"' when Char.equal char '\\' ->
+      | Some Double when Char.equal char '\\' ->
           if index + 1 = length then Error "unterminated \" quote"
           else
             let escaped = input.[index + 1] in
@@ -115,11 +120,9 @@ let split_shell_words ~preserve_syntax input =
             else (
               Buffer.add_char buffer char ;
               split (index + 1) quote true tokens )
-      | Some '"' ->
+      | Some Double ->
           Buffer.add_char buffer char ;
           split (index + 1) quote true tokens
-      | Some _ ->
-          failwith "unsupported quote delimiter"
   in
   split 0 None false []
 

From 513232c555cb1aefde6e188ef008892fe473f58e Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 12:15:34 +0200
Subject: [PATCH 09/14] Introduce `ParseError` variant to communicate parse
 errors to users

---
 src/webhooks/github.ml | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 3f135f37..95c45cb2 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -75,6 +75,7 @@ module Commands = struct
     | Bench of bench_args
     | ResumeMinimize of (string * string list * Minimize_parser.minimize_parsed)
     | Minimize of (string * string list)
+    | ParseError of string
 end
 
 open Commands
@@ -113,14 +114,11 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
             @@ Str.quote github_bot_name )
         body
       then
-        let full_ci =
-          match Str.matched_group 1 body with
-          | "full" -> Some true
-          | "light" -> Some false
-          | "" -> None
-          | _ -> failwith "Impossible group value."
-        in
-        Some (RunCI {full_ci})
+        match Str.matched_group 1 body with
+        | "full" -> Some (RunCI {full_ci=Some true})
+        | "light" -> Some (RunCI {full_ci=Some false})
+        | "" -> Some (RunCI {full_ci=None})
+        | conf -> Some (ParseError (f "run ci command: unknown CI configuration %S" conf))
       else
         None
     in
@@ -145,7 +143,8 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
         | args ->
           match parse_key_value_arguments args with
           | Result.Ok args -> Some (Bench args)
-          | _ -> None
+          | Result.Error error ->
+            Some (ParseError (f "bench command could not parse key-value arguments: %s" error))
       else
         None
     in
@@ -229,6 +228,14 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
       Server.respond_string ~status:`OK
         ~body:(f "Received a request to start the bench.")
         ()
+    | Some (ParseError error) ->
+      (fun () ->
+         GitHub_mutations.post_comment ~bot_info
+           ~message:(error)
+           ~id:comment_info.issue.id
+         >>= Utils.report_on_posting_comment)
+      |> Lwt.async;
+      Server.respond_string ~status:`OK ~body:"Invalid bench arguments." ()
     | Some (RunCI _ | Merge | Bench _) ->
       Server.respond_string ~status:`OK
         ~body:"Command recognized but not allowed in this context."

From e4649531eb17ea15e751afc8e3b8f9959350d2f1 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Tue, 11 Aug 2026 12:28:01 +0200
Subject: [PATCH 10/14] Run `dune fmt`

---
 bot-components/utils/String_utils.ml  |  10 +-
 bot-components/utils/String_utils.mli |   6 +-
 src/webhooks/github.ml                | 285 +++++++++++++-------------
 tests/test_string_utils.ml            |  20 +-
 4 files changed, 164 insertions(+), 157 deletions(-)

diff --git a/bot-components/utils/String_utils.ml b/bot-components/utils/String_utils.ml
index 83d7813a..92a17a97 100644
--- a/bot-components/utils/String_utils.ml
+++ b/bot-components/utils/String_utils.ml
@@ -67,7 +67,9 @@ let split_shell_words ~preserve_syntax input =
     if index = length then
       match quote with
       | Some delimiter ->
-          Error (Printf.sprintf "unterminated %c quote" (match delimiter with Single -> '\'' | Double -> '"'))
+          Error
+            (Printf.sprintf "unterminated %c quote"
+               (match delimiter with Single -> '\'' | Double -> '"') )
       | None ->
           Ok (List.rev (finish_token token_started tokens))
     else
@@ -109,10 +111,8 @@ let split_shell_words ~preserve_syntax input =
           if index + 1 = length then Error "unterminated \" quote"
           else
             let escaped = input.[index + 1] in
-            if Char.equal escaped '\n' then
-              split (index + 2) quote true tokens
-            else if
-              List.mem ['"'; '\\'; '$'; '`'] escaped ~equal:Char.equal
+            if Char.equal escaped '\n' then split (index + 2) quote true tokens
+            else if List.mem ['"'; '\\'; '$'; '`'] escaped ~equal:Char.equal
             then (
               add_syntax char ;
               Buffer.add_char buffer escaped ;
diff --git a/bot-components/utils/String_utils.mli b/bot-components/utils/String_utils.mli
index 450f44ad..48cac01d 100644
--- a/bot-components/utils/String_utils.mli
+++ b/bot-components/utils/String_utils.mli
@@ -23,21 +23,21 @@ val first_line_of_string : string -> string
 
 val remove_between : string -> int -> int -> string
 
+val split_on_unquoted_whitespace : string -> (string list, string) Result.t
 (** [split_on_unquoted_whitespace input] splits [input] at ASCII whitespace
     outside single or double quotes. Shell quote and escape syntax is recognized
     and preserved in the returned tokens.
 
     Returns an error for an unterminated quote or a trailing backslash. *)
-val split_on_unquoted_whitespace : string -> (string list, string) Result.t
 
+val parse_key_value_arguments :
+  string -> ((string * string option) list, string) Result.t
 (** [parse_key_value_arguments input] parses shell-style [key=value] words.
     Quote and escape syntax is consumed. A missing equal sign produces a [None]
     value; an equal sign produces [Some value], including [Some ""] for an
     explicitly empty value. Values may contain additional equal signs.
 
     Returns an error if quoting is malformed or an argument has an empty key. *)
-val parse_key_value_arguments :
-  string -> ((string * string option) list, string) Result.t
 
 (* ========================================================================== *)
 (* Formatting Functions *)
diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 95c45cb2..3b007a28 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -66,11 +66,10 @@ let handle_push_event_for_repos ~bot_info ~key ~app_id ~install_id ~owner ~repo
       Server.respond_string ~status:`OK ~body:"Ignoring push event." ()
 
 module Commands = struct
-
   type bench_args = (string * string option) list
 
   type t =
-    | RunCI of { full_ci : bool option }
+    | RunCI of {full_ci: bool option}
     | Merge
     | Bench of bench_args
     | ResumeMinimize of (string * string list * Minimize_parser.minimize_parsed)
@@ -105,145 +104,153 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
                 "https://github.com/rocq-community/run-coq-bug-minimizer/actions" ) )
       |> Lwt.async ;
       Server.respond_string ~status:`OK ~body:"Handling minimization." ()
-  | None ->
-
-    let parse_run_ci body =
-      if string_match
-        ~regexp:
-          ( f "@%s:? [Rr]un \\(full\\|light\\|\\) ?[Cc][Ii]"
-            @@ Str.quote github_bot_name )
-        body
-      then
-        match Str.matched_group 1 body with
-        | "full" -> Some (RunCI {full_ci=Some true})
-        | "light" -> Some (RunCI {full_ci=Some false})
-        | "" -> Some (RunCI {full_ci=None})
-        | conf -> Some (ParseError (f "run ci command: unknown CI configuration %S" conf))
-      else
-        None
-    in
-   let parse_merge body =
-     if string_match
-       ~regexp:(f "@%s:? [Mm]erge now" @@ Str.quote github_bot_name)
-       body
-     then
-       Some Merge
-     else
-       None
-    in
-
-    let parse_bench body =
-      if
-        string_match
-          ~regexp:(f {|@%s:? [Bb]ench\( *$\| +\([^\n]+\) *\(\n\|$\)\)|} @@ Str.quote github_bot_name)
-          body
-      then
-        match Str.matched_group 2 body with
-        | exception _ -> Some (Bench [])
-        | args ->
-          match parse_key_value_arguments args with
-          | Result.Ok args -> Some (Bench args)
-          | Result.Error error ->
-            Some (ParseError (f "bench command could not parse key-value arguments: %s" error))
-      else
-        None
-    in
-    let parse () =
-      let open Option in
-    (* Since both ci minimization resumption and ci minimization will match the
+  | None -> (
+      let parse_run_ci body =
+        if
+          string_match
+            ~regexp:
+              ( f "@%s:? [Rr]un \\(full\\|light\\|\\) ?[Cc][Ii]"
+              @@ Str.quote github_bot_name )
+            body
+        then
+          match Str.matched_group 1 body with
+          | "full" ->
+              Some (RunCI {full_ci= Some true})
+          | "light" ->
+              Some (RunCI {full_ci= Some false})
+          | "" ->
+              Some (RunCI {full_ci= None})
+          | conf ->
+              Some
+                (ParseError
+                   (f "run ci command: unknown CI configuration %S" conf) )
+        else None
+      in
+      let parse_merge body =
+        if
+          string_match
+            ~regexp:(f "@%s:? [Mm]erge now" @@ Str.quote github_bot_name)
+            body
+        then Some Merge
+        else None
+      in
+      let parse_bench body =
+        if
+          string_match
+            ~regexp:
+              ( f {|@%s:? [Bb]ench\( *$\| +\([^\n]+\) *\(\n\|$\)\)|}
+              @@ Str.quote github_bot_name )
+            body
+        then
+          match Str.matched_group 2 body with
+          | exception _ ->
+              Some (Bench [])
+          | args -> (
+            match parse_key_value_arguments args with
+            | Result.Ok args ->
+                Some (Bench args)
+            | Result.Error error ->
+                Some
+                  (ParseError
+                     (f "bench command could not parse key-value arguments: %s"
+                        error ) ) )
+        else None
+      in
+      let parse () =
+        let open Option in
+        (* 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 *)
-      List.find_map ~f:(fun fn -> fn body) [
-        (fun body -> resume_ci_minimize_text_of_body body >>| fun x -> ResumeMinimize x);
-        (fun body -> ci_minimize_text_of_body body >>| fun x -> Minimize x);
-        parse_run_ci;
-        parse_merge;
-        parse_bench
-      ]
-    in
-    match parse () with
-    | Some (ResumeMinimize (options, requests, bug_file)) ->
-      (fun () ->
-        init_git_bare_repository ~bot_info
-        >>= fun () ->
-        Bot_components.Github_installations.action_as_github_app ~bot_info
-          ~key ~app_id ~owner:comment_info.issue.issue.owner (fun ~bot_info ->
-            Minimization.ci_minimize ~bot_info ~comment_info ~requests
-              ~comment_on_error:true ~options ~bug_file:(Some bug_file) ) )
-      |> Lwt.async ;
-      Server.respond_string ~status:`OK
-        ~body:"Handling CI minimization resumption." ()
-    | Some (Minimize (options, requests)) ->
-      (fun () ->
-         init_git_bare_repository ~bot_info
-         >>= fun () ->
-         Bot_components.Github_installations.action_as_github_app ~bot_info
-           ~key ~app_id ~owner:comment_info.issue.issue.owner
-           (fun ~bot_info ->
-              Minimization.ci_minimize ~bot_info ~comment_info ~requests
-                ~comment_on_error:true ~options ~bug_file:None ) )
-      |> Lwt.async ;
-      Server.respond_string ~status:`OK ~body:"Handling CI minimization." ()
-    | Some (RunCI {full_ci}) when
-        comment_info.issue.pull_request
-        && String.equal comment_info.issue.issue.owner "rocq-prover"
-        && String.equal comment_info.issue.issue.repo "rocq"
-        && Option.is_some install_id ->
-      init_git_bare_repository ~bot_info
-      >>= fun () ->
-      Bot_components.Github_installations.action_as_github_app ~bot_info
-        ~key ~app_id ~owner:comment_info.issue.issue.owner
-        (Pr_sync.run_ci_action ~comment_info ?full_ci ~gitlab_mapping
-           ~github_mapping () )
-    | Some Merge when
-        comment_info.issue.pull_request
-        && String.equal comment_info.issue.issue.owner "rocq-prover"
-        && String.equal comment_info.issue.issue.repo "rocq"
-        && Option.is_some install_id ->
-      (fun () ->
-         Bot_components.Github_installations.action_as_github_app ~bot_info
-           ~key ~app_id ~owner:comment_info.issue.issue.owner
-           (fun ~bot_info ->
-              GitHub_automation.merge_pull_request_action ~bot_info
-                comment_info ) )
-      |> Lwt.async ;
-      Server.respond_string ~status:`OK
-        ~body:(f "Received a request to merge the PR.")
-        ()
-    | Some (Bench args) when
-            comment_info.issue.pull_request
-            && String.equal comment_info.issue.issue.owner "rocq-prover"
-            && String.equal comment_info.issue.issue.repo "rocq"
-            && Option.is_some install_id ->
-      let key_value_pairs = List.map ~f:(fun (k,v) -> (k, Option.value ~default:"yes" v)) args in
-      (fun () ->
-         Bot_components.Github_installations.action_as_github_app ~bot_info
-           ~key ~app_id ~owner:comment_info.issue.issue.owner
-           (fun ~bot_info ->
-              Bench.run_bench ~bot_info
-                ~key_value_pairs
-                comment_info )
-      )
-      |> Lwt.async ;
-      Server.respond_string ~status:`OK
-        ~body:(f "Received a request to start the bench.")
-        ()
-    | Some (ParseError error) ->
-      (fun () ->
-         GitHub_mutations.post_comment ~bot_info
-           ~message:(error)
-           ~id:comment_info.issue.id
-         >>= Utils.report_on_posting_comment)
-      |> Lwt.async;
-      Server.respond_string ~status:`OK ~body:"Invalid bench arguments." ()
-    | Some (RunCI _ | Merge | Bench _) ->
-      Server.respond_string ~status:`OK
-        ~body:"Command recognized but not allowed in this context."
-        ()
-    | None ->
-      Server.respond_string ~status:`OK
-        ~body:(f "Unhandled comment: %s" body)
-        ()
+        List.find_map
+          ~f:(fun fn -> fn body)
+          [ (fun body ->
+              resume_ci_minimize_text_of_body body >>| fun x -> ResumeMinimize x )
+          ; (fun body -> ci_minimize_text_of_body body >>| fun x -> Minimize x)
+          ; parse_run_ci
+          ; parse_merge
+          ; parse_bench ]
+      in
+      match parse () with
+      | Some (ResumeMinimize (options, requests, bug_file)) ->
+          (fun () ->
+            init_git_bare_repository ~bot_info
+            >>= fun () ->
+            Bot_components.Github_installations.action_as_github_app ~bot_info
+              ~key ~app_id ~owner:comment_info.issue.issue.owner
+              (fun ~bot_info ->
+                Minimization.ci_minimize ~bot_info ~comment_info ~requests
+                  ~comment_on_error:true ~options ~bug_file:(Some bug_file) ) )
+          |> Lwt.async ;
+          Server.respond_string ~status:`OK
+            ~body:"Handling CI minimization resumption." ()
+      | Some (Minimize (options, requests)) ->
+          (fun () ->
+            init_git_bare_repository ~bot_info
+            >>= fun () ->
+            Bot_components.Github_installations.action_as_github_app ~bot_info
+              ~key ~app_id ~owner:comment_info.issue.issue.owner
+              (fun ~bot_info ->
+                Minimization.ci_minimize ~bot_info ~comment_info ~requests
+                  ~comment_on_error:true ~options ~bug_file:None ) )
+          |> Lwt.async ;
+          Server.respond_string ~status:`OK ~body:"Handling CI minimization." ()
+      | Some (RunCI {full_ci})
+        when comment_info.issue.pull_request
+             && String.equal comment_info.issue.issue.owner "rocq-prover"
+             && String.equal comment_info.issue.issue.repo "rocq"
+             && Option.is_some install_id ->
+          init_git_bare_repository ~bot_info
+          >>= fun () ->
+          Bot_components.Github_installations.action_as_github_app ~bot_info
+            ~key ~app_id ~owner:comment_info.issue.issue.owner
+            (Pr_sync.run_ci_action ~comment_info ?full_ci ~gitlab_mapping
+               ~github_mapping () )
+      | Some Merge
+        when comment_info.issue.pull_request
+             && String.equal comment_info.issue.issue.owner "rocq-prover"
+             && String.equal comment_info.issue.issue.repo "rocq"
+             && Option.is_some install_id ->
+          (fun () ->
+            Bot_components.Github_installations.action_as_github_app ~bot_info
+              ~key ~app_id ~owner:comment_info.issue.issue.owner
+              (fun ~bot_info ->
+                GitHub_automation.merge_pull_request_action ~bot_info
+                  comment_info ) )
+          |> Lwt.async ;
+          Server.respond_string ~status:`OK
+            ~body:(f "Received a request to merge the PR.")
+            ()
+      | Some (Bench args)
+        when comment_info.issue.pull_request
+             && String.equal comment_info.issue.issue.owner "rocq-prover"
+             && String.equal comment_info.issue.issue.repo "rocq"
+             && Option.is_some install_id ->
+          let key_value_pairs =
+            List.map ~f:(fun (k, v) -> (k, Option.value ~default:"yes" v)) args
+          in
+          (fun () ->
+            Bot_components.Github_installations.action_as_github_app ~bot_info
+              ~key ~app_id ~owner:comment_info.issue.issue.owner
+              (fun ~bot_info ->
+                Bench.run_bench ~bot_info ~key_value_pairs comment_info ) )
+          |> Lwt.async ;
+          Server.respond_string ~status:`OK
+            ~body:(f "Received a request to start the bench.")
+            ()
+      | Some (ParseError error) ->
+          (fun () ->
+            GitHub_mutations.post_comment ~bot_info ~message:error
+              ~id:comment_info.issue.id
+            >>= Utils.report_on_posting_comment )
+          |> Lwt.async ;
+          Server.respond_string ~status:`OK ~body:"Invalid bench arguments." ()
+      | Some (RunCI _ | Merge | Bench _) ->
+          Server.respond_string ~status:`OK
+            ~body:"Command recognized but not allowed in this context." ()
+      | None ->
+          Server.respond_string ~status:`OK
+            ~body:(f "Unhandled comment: %s" body)
+            () )
 
 let handle_github_webhook ~bot_info ~key ~app_id ~github_bot_name
     ~gitlab_mapping ~github_mapping ~repo_config_table ~github_webhook_secret
diff --git a/tests/test_string_utils.ml b/tests/test_string_utils.ml
index 723923ce..7fcac753 100644
--- a/tests/test_string_utils.ml
+++ b/tests/test_string_utils.ml
@@ -20,8 +20,10 @@ let () =
       , [test_case "quoted bot name" `Quick test_strip_quoted_bot_name] ) ]
 
 let tokens = Alcotest.list Alcotest.string
+
 let key_values =
-  Alcotest.list (Alcotest.pair Alcotest.string (Alcotest.option Alcotest.string))
+  Alcotest.list
+    (Alcotest.pair Alcotest.string (Alcotest.option Alcotest.string))
 
 let check_split ~input ~expected () =
   match split_on_unquoted_whitespace input with
@@ -55,9 +57,7 @@ let check_argument_error ~input ~expected () =
 let () =
   Alcotest.run "String_utils tests"
     [ ( "split_on_unquoted_whitespace"
-      , [ ( "empty input"
-          , `Quick
-          , check_split ~input:"" ~expected:[] )
+      , [ ("empty input", `Quick, check_split ~input:"" ~expected:[])
         ; ( "unquoted arguments"
           , `Quick
           , check_split ~input:"x=foo y=true" ~expected:["x=foo"; "y=true"] )
@@ -127,8 +127,8 @@ let () =
               ~expected:[("x", Some ""); ("y", Some "")] )
         ; ( "additional equal signs"
           , `Quick
-          , check_arguments ~input:"x=foo=bar"
-              ~expected:[("x", Some "foo=bar")] )
+          , check_arguments ~input:"x=foo=bar" ~expected:[("x", Some "foo=bar")]
+          )
         ; ( "missing value"
           , `Quick
           , check_arguments ~input:"x=foo missing"
@@ -143,7 +143,7 @@ let () =
               ~expected:"argument \"\" has an empty key" )
         ; ( "coq_opam_packages"
           , `Quick
-          , check_arguments
-              ~input:{|coq_opam_packages="a b c" coq_native|}
-              ~expected:[("coq_opam_packages", Some "a b c"); ("coq_native", None)])
-        ] ) ]
+          , check_arguments ~input:{|coq_opam_packages="a b c" coq_native|}
+              ~expected:
+                [("coq_opam_packages", Some "a b c"); ("coq_native", None)] ) ]
+      ) ]

From 793b97b3ad702389f6b7042468fb1723e91673c1 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Wed, 12 Aug 2026 17:57:03 +0200
Subject: [PATCH 11/14] Merge Alcotest.run calls

---
 tests/test_string_utils.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/tests/test_string_utils.ml b/tests/test_string_utils.ml
index 7fcac753..883da232 100644
--- a/tests/test_string_utils.ml
+++ b/tests/test_string_utils.ml
@@ -14,11 +14,6 @@ let test_strip_quoted_bot_name () =
   in
   (check string) "strip_quoted_bot_name" expected got
 
-let () =
-  run "String_utils tests"
-    [ ( "strip_quoted_bot_name"
-      , [test_case "quoted bot name" `Quick test_strip_quoted_bot_name] ) ]
-
 let tokens = Alcotest.list Alcotest.string
 
 let key_values =
@@ -56,7 +51,9 @@ let check_argument_error ~input ~expected () =
 
 let () =
   Alcotest.run "String_utils tests"
-    [ ( "split_on_unquoted_whitespace"
+    [ ( "strip_quoted_bot_name"
+      , [test_case "quoted bot name" `Quick test_strip_quoted_bot_name] )
+    ; ( "split_on_unquoted_whitespace"
       , [ ("empty input", `Quick, check_split ~input:"" ~expected:[])
         ; ( "unquoted arguments"
           , `Quick

From bc9bbd3a9031fad1cf7ce74b6a61ce087c9e7bc8 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Fri, 14 Aug 2026 15:55:16 +0200
Subject: [PATCH 12/14] Fix bench regexp to stop at double newlines or end of
 string

---
 src/webhooks/github.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index 3b007a28..c6ac53fb 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -138,7 +138,7 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
         if
           string_match
             ~regexp:
-              ( f {|@%s:? [Bb]ench\( *$\| +\([^\n]+\) *\(\n\|$\)\)|}
+              ( f "@%s:? [Bb]ench\\( *$\\| +\\(.*\\(\n.+\\)*\\)\\(\n\n\\|$\\)\\)"
               @@ Str.quote github_bot_name )
             body
         then

From 734f8e2c671cbcc82d355c4095ea884197a64891 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Fri, 14 Aug 2026 17:13:47 +0200
Subject: [PATCH 13/14] Fix, refactor, and test bench command parser

---
 src/utils/bench.ml     | 71 ++++++++++++++++++++++++++++++++++++++++++
 src/utils/bench.mli    |  4 +++
 src/utils/dune         |  3 ++
 src/webhooks/github.ml | 32 +++++--------------
 4 files changed, 86 insertions(+), 24 deletions(-)

diff --git a/src/utils/bench.ml b/src/utils/bench.ml
index 0170555f..1cf74857 100644
--- a/src/utils/bench.ml
+++ b/src/utils/bench.ml
@@ -7,6 +7,77 @@ open HTTP_utils
 open String_utils
 open Lwt.Infix
 
+type args = (string * string option) list
+
+let parse ~github_bot_name body =
+  if
+    string_match
+      ~regexp:
+        ( f "@%s:? [Bb]ench\\( *$\\| +\\(.*\\(\n.+\\)*\\)\\(\n\n\\|$\\)\\)"
+        @@ Str.quote github_bot_name )
+      body
+  then
+    match Str.matched_group 2 body with
+    | exception _ ->
+        Some (Result.Ok [])
+    | args ->
+        Some
+          (Result.map_error (parse_key_value_arguments args) ~f:(fun error ->
+               f "bench command could not parse key-value arguments: %s" error )
+          )
+  else None
+
+let%test "parses a command without arguments" =
+  match parse ~github_bot_name:"coqbot" "@coqbot bench" with
+  | Some (Result.Ok []) ->
+      true
+  | _ ->
+      false
+
+let%test "parses arguments through the end of the comment" =
+  match
+    parse ~github_bot_name:"coqbot"
+      "@coqbot bench coq_native\ncoq_opam_packages=\"a b\""
+  with
+  | Some (Result.Ok [("coq_native", None); ("coq_opam_packages", Some "a b")])
+    ->
+      true
+  | _ ->
+      false
+
+let%test "parses multiline arguments until an empty line" =
+  match
+    parse ~github_bot_name:"coqbot"
+      "@coqbot: Bench coq_native=yes\n\
+       coq_opam_packages='a b'\n\n\
+       This text is not part of the command."
+  with
+  | Some
+      (Result.Ok [("coq_native", Some "yes"); ("coq_opam_packages", Some "a b")])
+    ->
+      true
+  | _ ->
+      false
+
+let%test "reports malformed arguments" =
+  match
+    parse ~github_bot_name:"coqbot" "@coqbot bench value=\"unterminated"
+  with
+  | Some
+      (Result.Error
+         "bench command could not parse key-value arguments: unterminated \" \
+          quote" ) ->
+      true
+  | _ ->
+      false
+
+let%test "does not parse another command" =
+  match parse ~github_bot_name:"coqbot" "@coqbot benchmark" with
+  | None ->
+      true
+  | Some _ ->
+      false
+
 let parse_quantity table table_name =
   let regexp = {|.*TOP \([0-9]*\)|} in
   if string_match ~regexp table then
diff --git a/src/utils/bench.mli b/src/utils/bench.mli
index b53fe4b8..ab003801 100644
--- a/src/utils/bench.mli
+++ b/src/utils/bench.mli
@@ -1,5 +1,9 @@
 open Base
 
+type args = (string * string option) list
+
+val parse : github_bot_name:string -> string -> (args, string) Result.t option
+
 module BenchResults : sig
   type t =
     { summary_table: string
diff --git a/src/utils/dune b/src/utils/dune
index 4626b6c0..9593e03b 100644
--- a/src/utils/dune
+++ b/src/utils/dune
@@ -2,5 +2,8 @@
  (name utils)
  (public_name coq-bot.utils)
  (libraries base bot-components)
+ (inline_tests)
+ (preprocess
+  (pps ppx_expect))
  (wrapped false)
  (modules bench coq))
diff --git a/src/webhooks/github.ml b/src/webhooks/github.ml
index c6ac53fb..832dff45 100644
--- a/src/webhooks/github.ml
+++ b/src/webhooks/github.ml
@@ -66,7 +66,7 @@ let handle_push_event_for_repos ~bot_info ~key ~app_id ~install_id ~owner ~repo
       Server.respond_string ~status:`OK ~body:"Ignoring push event." ()
 
 module Commands = struct
-  type bench_args = (string * string option) list
+  type bench_args = Bench.args
 
   type t =
     | RunCI of {full_ci: bool option}
@@ -134,28 +134,6 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
         then Some Merge
         else None
       in
-      let parse_bench body =
-        if
-          string_match
-            ~regexp:
-              ( f "@%s:? [Bb]ench\\( *$\\| +\\(.*\\(\n.+\\)*\\)\\(\n\n\\|$\\)\\)"
-              @@ Str.quote github_bot_name )
-            body
-        then
-          match Str.matched_group 2 body with
-          | exception _ ->
-              Some (Bench [])
-          | args -> (
-            match parse_key_value_arguments args with
-            | Result.Ok args ->
-                Some (Bench args)
-            | Result.Error error ->
-                Some
-                  (ParseError
-                     (f "bench command could not parse key-value arguments: %s"
-                        error ) ) )
-        else None
-      in
       let parse () =
         let open Option in
         (* Since both ci minimization resumption and ci minimization will match the
@@ -168,7 +146,13 @@ let handle_comment_created ~bot_info ~key ~app_id ~github_bot_name
           ; (fun body -> ci_minimize_text_of_body body >>| fun x -> Minimize x)
           ; parse_run_ci
           ; parse_merge
-          ; parse_bench ]
+          ; (fun body ->
+              Bench.parse ~github_bot_name body
+              >>| function
+              | Result.Ok args ->
+                  Commands.Bench args
+              | Result.Error error ->
+                  ParseError error ) ]
       in
       match parse () with
       | Some (ResumeMinimize (options, requests, bug_file)) ->

From b2a6df0d58a197171dadebd2596ebed38b7408ea Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@skylabs-ai.com>
Date: Mon, 17 Aug 2026 11:11:56 +0200
Subject: [PATCH 14/14] Extract bench parser tests to a separate file

---
 src/utils/bench.ml  | 51 ---------------------------------------------
 src/utils/dune      |  3 ---
 tests/dune          |  5 +++++
 tests/test_bench.ml | 46 ++++++++++++++++++++++++++++++++++++++++
 4 files changed, 51 insertions(+), 54 deletions(-)
 create mode 100644 tests/test_bench.ml

diff --git a/src/utils/bench.ml b/src/utils/bench.ml
index 1cf74857..b167f2ce 100644
--- a/src/utils/bench.ml
+++ b/src/utils/bench.ml
@@ -27,57 +27,6 @@ let parse ~github_bot_name body =
           )
   else None
 
-let%test "parses a command without arguments" =
-  match parse ~github_bot_name:"coqbot" "@coqbot bench" with
-  | Some (Result.Ok []) ->
-      true
-  | _ ->
-      false
-
-let%test "parses arguments through the end of the comment" =
-  match
-    parse ~github_bot_name:"coqbot"
-      "@coqbot bench coq_native\ncoq_opam_packages=\"a b\""
-  with
-  | Some (Result.Ok [("coq_native", None); ("coq_opam_packages", Some "a b")])
-    ->
-      true
-  | _ ->
-      false
-
-let%test "parses multiline arguments until an empty line" =
-  match
-    parse ~github_bot_name:"coqbot"
-      "@coqbot: Bench coq_native=yes\n\
-       coq_opam_packages='a b'\n\n\
-       This text is not part of the command."
-  with
-  | Some
-      (Result.Ok [("coq_native", Some "yes"); ("coq_opam_packages", Some "a b")])
-    ->
-      true
-  | _ ->
-      false
-
-let%test "reports malformed arguments" =
-  match
-    parse ~github_bot_name:"coqbot" "@coqbot bench value=\"unterminated"
-  with
-  | Some
-      (Result.Error
-         "bench command could not parse key-value arguments: unterminated \" \
-          quote" ) ->
-      true
-  | _ ->
-      false
-
-let%test "does not parse another command" =
-  match parse ~github_bot_name:"coqbot" "@coqbot benchmark" with
-  | None ->
-      true
-  | Some _ ->
-      false
-
 let parse_quantity table table_name =
   let regexp = {|.*TOP \([0-9]*\)|} in
   if string_match ~regexp table then
diff --git a/src/utils/dune b/src/utils/dune
index 9593e03b..4626b6c0 100644
--- a/src/utils/dune
+++ b/src/utils/dune
@@ -2,8 +2,5 @@
  (name utils)
  (public_name coq-bot.utils)
  (libraries base bot-components)
- (inline_tests)
- (preprocess
-  (pps ppx_expect))
  (wrapped false)
  (modules bench coq))
diff --git a/tests/dune b/tests/dune
index 58458a8e..27a1da26 100644
--- a/tests/dune
+++ b/tests/dune
@@ -48,3 +48,8 @@
  (name test_string_utils)
  (modules test_string_utils)
  (libraries alcotest bot-components base))
+
+(test
+ (name test_bench)
+ (modules test_bench)
+ (libraries alcotest coq-bot.utils))
diff --git a/tests/test_bench.ml b/tests/test_bench.ml
new file mode 100644
index 00000000..1bfdb1c1
--- /dev/null
+++ b/tests/test_bench.ml
@@ -0,0 +1,46 @@
+open Alcotest
+
+let args = list (pair string (option string))
+
+let parse_result = option (result args string)
+
+let check_parse ~body ~expected () =
+  check parse_result body expected (Bench.parse ~github_bot_name:"coqbot" body)
+
+let () =
+  run "Bench parser tests"
+    [ ( "parse"
+      , [ ( "command without arguments"
+          , `Quick
+          , check_parse ~body:"@coqbot bench" ~expected:(Some (Ok [])) )
+        ; ( "arguments through end of comment"
+          , `Quick
+          , check_parse
+              ~body:"@coqbot bench coq_native\ncoq_opam_packages=\"a b\""
+              ~expected:
+                (Some
+                   (Ok [("coq_native", None); ("coq_opam_packages", Some "a b")])
+                ) )
+        ; ( "multiline arguments until empty line"
+          , `Quick
+          , check_parse
+              ~body:
+                "@coqbot: Bench coq_native=yes\n\
+                 coq_opam_packages='a b'\n\n\
+                 This text is not part of the command."
+              ~expected:
+                (Some
+                   (Ok
+                      [ ("coq_native", Some "yes")
+                      ; ("coq_opam_packages", Some "a b") ] ) ) )
+        ; ( "malformed arguments"
+          , `Quick
+          , check_parse ~body:"@coqbot bench value=\"unterminated"
+              ~expected:
+                (Some
+                   (Error
+                      "bench command could not parse key-value arguments: \
+                       unterminated \" quote" ) ) )
+        ; ( "another command"
+          , `Quick
+          , check_parse ~body:"@coqbot benchmark" ~expected:None ) ] ) ]