Skip to content

Commit 924e70f

Browse files
Adapt to rocq-prover/rocq#19925 (artifacts have _install_ci) (#336)
Co-authored-by: Jason Gross <[email protected]>
1 parent e838d62 commit 924e70f

File tree

4 files changed

+62
-33
lines changed

4 files changed

+62
-33
lines changed

run_ci_minimization.sh

+12-9
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
#!/usr/bin/env bash
22

3-
# 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]
3+
# usage: coq_bug_minimizer.sh comment_thread_id github_token bot_name bot_domain owner repo pr_number docker_image target ci-targets opam_switch failing_urls passing_urls base head minimizer_extra_arguments [bug_file]
44

55
set -e
66

7-
if [ $# != 15 ] && [ $# != 16 ]; then >&2 echo Bad argument count; exit 1; fi
7+
if [ $# != 16 ] && [ $# != 17 ]; then >&2 echo Bad argument count; exit 1; fi
88

99
comment_thread_id=$1
1010
token=$2
@@ -15,20 +15,22 @@ repo=$6
1515
pr_number=$7
1616
docker_image=$8
1717
target=$9
18-
opam_switch=${10}
19-
failing_urls=${11}
20-
passing_urls=${12}
21-
base=${13}
22-
head=${14}
23-
minimizer_extra_arguments=${15}
24-
bug_file=${16}
18+
ci_targets=${10}
19+
opam_switch=${11}
20+
failing_urls=${12}
21+
passing_urls=${13}
22+
base=${14}
23+
head=${15}
24+
minimizer_extra_arguments=${16}
25+
bug_file=${17}
2526
branch_id=$(($(od -A n -t uI -N 5 /dev/urandom | tr -d ' ')))
2627
repo_name="coq-community/run-coq-bug-minimizer"
2728
branch_name="run-coq-bug-minimizer-$branch_id"
2829
nl=$'\n'
2930
resumption_args=(
3031
"${docker_image}"
3132
"${target}"
33+
"${ci_targets}"
3234
"${opam_switch}"
3335
"${failing_urls}"
3436
"${passing_urls}"
@@ -52,6 +54,7 @@ pushd "$wtree"
5254
printf "%s %s %s %s %s %s %s" "$comment_thread_id" "<>" "$repo_name" "$branch_name" "$owner" "$repo" "$pr_number" > coqbot-request-stamp
5355
sed -i 's~^\(\s*\)[^:\s]*custom_image:.*$~\1custom_image: '"'${docker_image}'~" .github/workflows/main.yml
5456
echo "${target}" > coqbot.ci-target
57+
echo "${ci_targets}" > coqbot.ci-targets
5558
echo "${opam_switch}" > coqbot.compiler
5659
echo "${failing_urls}" > coqbot.failing-artifact-urls
5760
echo "${passing_urls}" > coqbot.passing-artifact-urls

src/actions.ml

+46-22
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ open Lwt.Syntax
1313
type coq_job_info =
1414
{ docker_image: string
1515
; dependencies: string list
16+
; targets: string list
1617
; compiler: string
1718
; opam_variant: string }
1819

@@ -88,22 +89,29 @@ let send_status_check ~bot_info job_info ~pr_num (gh_owner, gh_repo)
8889
; "options=Options(docker='\\([^']+\\)')" ]
8990
>>= fun docker_image ->
9091
let dependencies = find_all ["^Downloading artifacts for \\([^ ]+\\)"] in
92+
(* The CI script prints "CI_TARGETS=foo bar" through "env" if it is non-default,
93+
then "CI_TARGETS = foo bar" even if it is the default (from job name).
94+
We use the later. *)
95+
find ["^CI_TARGETS = \\(.*\\)"]
96+
>>= fun targets ->
97+
let targets = String.split ~on:' ' targets in
9198
find ["^COMPILER=\\(.*\\)"]
9299
>>= fun compiler ->
93100
find ["^OPAM_VARIANT=\\(.*\\)"]
94101
>>= fun opam_variant ->
95-
Some {docker_image; dependencies; compiler; opam_variant}
102+
Some {docker_image; dependencies; targets; compiler; opam_variant}
96103
in
97104
let* summary_tail_prefix =
98105
match coq_job_info with
99-
| Some {docker_image; dependencies; compiler; opam_variant} ->
106+
| Some {docker_image; dependencies; targets; compiler; opam_variant} ->
100107
let switch_name = compiler ^ opam_variant in
101108
let dependencies = String.concat ~sep:"` `" dependencies in
109+
let targets = String.concat ~sep:"` `" targets in
102110
Lwt.return
103111
(f
104-
"This job ran on the Docker image `%s` with OCaml `%s` and depended on jobs \
105-
`%s` .\n\n"
106-
docker_image switch_name dependencies )
112+
"This job ran on the Docker image `%s` with OCaml `%s` and \
113+
depended on jobs `%s`. It built targets `%s`.\n\n"
114+
docker_image switch_name dependencies targets )
107115
| None ->
108116
Lwt.return ""
109117
in
@@ -734,6 +742,7 @@ let create_pipeline_summary ?summary_top pipeline_info pipeline_url =
734742
type ci_minimization_info =
735743
{ target: string
736744
; full_target: string
745+
; ci_targets: string list
737746
; docker_image: string
738747
; opam_switch: string
739748
; failing_urls: string
@@ -857,10 +866,16 @@ let run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
857866
>>= fun () ->
858867
let bug_file_name = Option.map ~f:(fun _ -> bug_file_name) bug_file in
859868
Lwt_list.map_s
860-
(fun {target; opam_switch; failing_urls; passing_urls; docker_image} ->
869+
(fun { target
870+
; ci_targets
871+
; opam_switch
872+
; failing_urls
873+
; passing_urls
874+
; docker_image } ->
861875
git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo
862-
~pr_number ~docker_image ~target ~opam_switch ~failing_urls
863-
~passing_urls ~base ~head ~minimizer_extra_arguments ~bug_file_name
876+
~pr_number ~docker_image ~ci_targets ~target ~opam_switch
877+
~failing_urls ~passing_urls ~base ~head ~minimizer_extra_arguments
878+
~bug_file_name
864879
>>= fun result -> Lwt.return (target, result) )
865880
ci_minimization_infos
866881
>>= Lwt.return_ok )
@@ -917,16 +932,19 @@ let ci_minimization_extract_job_specific_info ~head_pipeline_summary
917932
if
918933
string_match
919934
~regexp:
920-
"This job ran on the Docker image `\\([^`]+\\)` with OCaml `\\([^`]+\\)` and depended on jobs \
921-
\\(\\(`[^`]+` ?\\)+\\) .\n\n"
935+
"This job ran on the Docker image `\\([^`]+\\)` with OCaml \
936+
`\\([^`]+\\)` and depended on jobs \\(\\(`[^`]+` ?\\)+\\). It \
937+
built targets \\(\\(`[^`]+` ?\\)+\\).\n\n"
922938
summary
923939
then
924-
let docker_image, opam_switch, dependencies =
940+
let docker_image, opam_switch, dependencies, targets =
925941
( Str.matched_group 1 summary
926942
, Str.matched_group 2 summary
927-
, Str.matched_group 3 summary )
943+
, Str.matched_group 3 summary
944+
, Str.matched_group 4 summary )
928945
in
929946
let dependencies = Str.split (Str.regexp "[ `]+") dependencies in
947+
let ci_targets = Str.split (Str.regexp "[ `]+") targets in
930948
let missing_error, non_v_file =
931949
if
932950
string_match
@@ -943,18 +961,20 @@ let ci_minimization_extract_job_specific_info ~head_pipeline_summary
943961
else (true, None)
944962
in
945963
let extract_artifacts url =
946-
List.partition_map ~f:(fun name ->
964+
List.partition_map
965+
~f:(fun name ->
947966
match extract_artifact_url name url with
948-
| Some v -> First v
949-
| None -> Second name)
950-
(name::dependencies)
967+
| Some v ->
968+
First v
969+
| None ->
970+
Second name )
971+
(name :: dependencies)
951972
in
952973
match
953974
( extract_artifacts base_pipeline_summary
954975
, extract_artifacts head_pipeline_summary )
955976
with
956-
| ( (base_urls, [])
957-
, (head_urls, []) ) ->
977+
| (base_urls, []), (head_urls, []) ->
958978
Ok
959979
( { base_job_failed
960980
; base_job_errored
@@ -965,17 +985,18 @@ let ci_minimization_extract_job_specific_info ~head_pipeline_summary
965985
; job_target= target (*; overlayed= false (* XXX FIXME *)*) }
966986
, { target
967987
; full_target= name
988+
; ci_targets
968989
; docker_image
969990
; opam_switch
970991
; failing_urls= String.concat ~sep:" " head_urls
971992
; passing_urls= String.concat ~sep:" " base_urls } )
972-
| (_, ((_ :: _) as base_failed)), _ ->
993+
| (_, (_ :: _ as base_failed)), _ ->
973994
Error
974995
(f "Could not find base dependencies artifacts for %s in:\n%s"
975996
(String.concat ~sep:" " base_failed)
976997
(collapse_summary "Base Pipeline Summary"
977998
base_pipeline_summary ) )
978-
| _, (_, ((_ :: _) as head_failed)) ->
999+
| _, (_, (_ :: _ as head_failed)) ->
9791000
Error
9801001
(f "Could not find head dependencies artifacts for %s in:\n%s"
9811002
(String.concat ~sep:" " head_failed)
@@ -2156,11 +2177,13 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
21562177
; pr_number ] -> (
21572178
message |> String.split ~on:'\n'
21582179
|> function
2159-
| docker_image :: target :: opam_switch :: failing_urls :: passing_urls
2160-
:: base :: head :: extra_arguments_joined :: bug_file_lines ->
2180+
| docker_image :: target :: ci_targets_joined :: opam_switch
2181+
:: failing_urls :: passing_urls :: base :: head
2182+
:: extra_arguments_joined :: bug_file_lines ->
21612183
(let minimizer_extra_arguments =
21622184
String.split ~on:' ' extra_arguments_joined
21632185
in
2186+
let ci_targets = String.split ~on:' ' ci_targets_joined in
21642187
let bug_file_contents = String.concat ~sep:"\n" bug_file_lines in
21652188
fun () ->
21662189
init_git_bare_repository ~bot_info
@@ -2173,6 +2196,7 @@ let coq_bug_minimizer_resume_ci_minimization_action ~bot_info ~key ~app_id body
21732196
~minimizer_extra_arguments
21742197
~ci_minimization_infos:
21752198
[ { target
2199+
; ci_targets
21762200
; opam_switch
21772201
; failing_urls
21782202
; passing_urls

src/git_utils.ml

+3-2
Original file line numberDiff line numberDiff line change
@@ -182,8 +182,8 @@ let git_coq_bug_minimizer ~bot_info ~script ~comment_thread_id ~comment_author
182182
|> execute_cmd ~mask:[bot_info.github_pat]
183183

184184
let git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
185-
~docker_image ~target ~opam_switch ~failing_urls ~passing_urls ~base ~head
186-
~minimizer_extra_arguments ~bug_file_name =
185+
~docker_image ~target ~ci_targets ~opam_switch ~failing_urls ~passing_urls
186+
~base ~head ~minimizer_extra_arguments ~bug_file_name =
187187
(* To push a new branch we need to identify as coqbot the GitHub
188188
user, who is a collaborator on the run-coq-bug-minimizer repo,
189189
not coqbot the GitHub App *)
@@ -196,6 +196,7 @@ let git_run_ci_minimization ~bot_info ~comment_thread_id ~owner ~repo ~pr_number
196196
; pr_number
197197
; docker_image
198198
; target
199+
; ci_targets |> String.concat ~sep:" "
199200
; opam_switch
200201
; failing_urls
201202
; passing_urls

src/git_utils.mli

+1
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ val git_run_ci_minimization :
6161
-> pr_number:string
6262
-> docker_image:string
6363
-> target:string
64+
-> ci_targets:string list
6465
-> opam_switch:string
6566
-> failing_urls:string
6667
-> passing_urls:string

0 commit comments

Comments
 (0)