Skip to content

Commit

Permalink
Allow customization of Coq version
Browse files Browse the repository at this point in the history
Not entirely clear what the protocol should be, see also #183.  We
currently allow things like `coq-8.14` and `coq.dev` and `coq: dev` and
`ocaml: 4.11`, etc.
  • Loading branch information
JasonGross committed Nov 18, 2022
1 parent 9ac8fcf commit d2c6908
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 17 deletions.
31 changes: 26 additions & 5 deletions src/actions.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1836,9 +1836,27 @@ let pipeline_action ~bot_info pipeline_info ~gitlab_mapping : unit Lwt.t =
Lwt.return_unit ) ) )

let run_coq_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
~owner ~repo =
~owner ~repo ~options =
let options = " " ^ options ^ " " in
let getopt opt =
if
string_match
~regexp:(f " %s\\(\\.\\|[ -]\\|: \\)\\([^ ]+\\) " 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
Lwt_io.printlf
"Parsed options for the bug minimizer at %s/%s@%s from '%s' into \
{coq_version: '%s'; ocaml_version: '%s'}"
owner repo
(GitHub_ID.to_string comment_thread_id)
options coq_version ocaml_version
>>= fun () ->
git_coq_bug_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
~owner ~repo
~owner ~repo ~coq_version ~ocaml_version
>>= function
| Ok () ->
GitHub_mutations.post_comment ~id:comment_thread_id
Expand Down Expand Up @@ -1898,8 +1916,11 @@ 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 ->
| 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
fun () ->
init_git_bare_repository ~bot_info
Expand Down Expand Up @@ -2351,7 +2372,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
Expand Down
1 change: 1 addition & 0 deletions src/actions.mli
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ val run_coq_minimizer :
-> comment_author:string
-> owner:string
-> repo:string
-> options:string
-> unit Lwt.t

val coq_bug_minimizer_results_action :
Expand Down
20 changes: 11 additions & 9 deletions src/bot.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,10 +57,13 @@ let callback _conn req body =
if
string_match
~regexp:
( f "@%s:? [Mm]inimize[^`]*```[^\n]*\n\\(\\(.\\|\n\\)+\\)"
( f "@%s:? [Mm]inimize\\([^`]*\\)```[^\n]*\n\\(\\(.\\|\n\\)+\\)"
@@ Str.quote bot_name )
body
then Some (Str.matched_group 1 body |> extract_minimize_file)
then
Some
( Str.matched_group 1 body
, Str.matched_group 2 body |> extract_minimize_file )
else None
in
let strip_quoted_bot_name body =
Expand Down Expand Up @@ -184,16 +187,16 @@ let callback _conn req body =
| Ok (_, IssueOpened ({body= Some body} as issue_info)) -> (
let body = body |> Helpers.trim_comments |> strip_quoted_bot_name in
match coqbot_minimize_text_of_body body with
| Some script ->
| Some (options, script) ->
(fun () ->
init_git_bare_repository ~bot_info
>>= fun () ->
action_as_github_app ~bot_info ~key ~app_id
~owner:issue_info.issue.owner ~repo:issue_info.issue.repo
(run_coq_minimizer ~script ~comment_thread_id:issue_info.id
~comment_author:issue_info.user
~owner:issue_info.issue.owner ~repo:issue_info.issue.repo )
)
~owner:issue_info.issue.owner ~repo:issue_info.issue.repo
~options ) )
|> Lwt.async ;
Server.respond_string ~status:`OK ~body:"Handling minimization."
()
Expand All @@ -206,7 +209,7 @@ let callback _conn req body =
comment_info.body |> Helpers.trim_comments |> strip_quoted_bot_name
in
match coqbot_minimize_text_of_body body with
| Some script ->
| Some (options, script) ->
(fun () ->
init_git_bare_repository ~bot_info
>>= fun () ->
Expand All @@ -217,7 +220,7 @@ let callback _conn req body =
~comment_thread_id:comment_info.issue.id
~comment_author:comment_info.author
~owner:comment_info.issue.issue.owner
~repo:comment_info.issue.issue.repo ) )
~repo:comment_info.issue.issue.repo ~options ) )
|> Lwt.async ;
Server.respond_string ~status:`OK ~body:"Handling minimization."
()
Expand Down Expand Up @@ -344,8 +347,7 @@ let callback _conn req body =
action_as_github_app ~bot_info ~key ~app_id
~owner:comment_info.issue.issue.owner
~repo:comment_info.issue.issue.repo
(run_bench
~key_value_pairs:[("coq_native", "yes")]
(run_bench ~key_value_pairs:[("coq_native", "yes")]
comment_info ) )
|> Lwt.async ;
Server.respond_string ~status:`OK
Expand Down
4 changes: 1 addition & 3 deletions src/git_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -130,12 +130,10 @@ 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 =
~owner ~repo ~coq_version ~ocaml_version =
(* 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 *)
let coq_version = "" in
let ocaml_version = "" in
Stdlib.Filename.quote_command "./coq_bug_minimizer.sh"
[ script
; GitHub_ID.to_string comment_thread_id
Expand Down
2 changes: 2 additions & 0 deletions src/git_utils.mli
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ val git_coq_bug_minimizer :
-> comment_author:string
-> owner:string
-> repo:string
-> coq_version:string
-> ocaml_version:string
-> (unit, string) result Lwt.t

val git_run_ci_minimization :
Expand Down

0 comments on commit d2c6908

Please sign in to comment.