@@ -6,6 +6,7 @@ open Utils
66open HTTP_utils
77open String_utils
88open Lwt.Infix
9+ open Repo_config
910
1011let parse_quantity table table_name =
1112 let regexp = {|.* TOP \([0-9 ]* \)| } in
@@ -151,8 +152,8 @@ let bench_comment ~bot_info ~owner ~repo ~number ~gitlab_url ?check_url
151152 Lwt_io. printlf " Unable to get_pull_request_id for bench for pr #%d: %s"
152153 number e
153154
154- let update_bench_status ~bot_info ~job_info ( gh_owner , gh_repo ) ~ external_id
155- ~number =
155+ let update_bench_status ~bot_info ~repo_config_table ~ job_info
156+ ( gh_owner , gh_repo ) ~ external_id ~number =
156157 let open Lwt.Syntax in
157158 match number with
158159 | None ->
@@ -163,11 +164,28 @@ let update_bench_status ~bot_info ~job_info (gh_owner, gh_repo) ~external_id
163164 | Error e ->
164165 Lwt_io. printlf " No repo id for bench job: %s" e
165166 | Ok repo_id -> (
166- Lwt_io. printl " Pushing status check for bench job."
167- < &>
167+ let repo_config =
168+ get_repo_config_opt ~owner: gh_owner ~repo: gh_repo repo_config_table
169+ in
170+ (* Original: hardcoded GitLab URL "https://gitlab.inria.fr/coq/coq/-/jobs/%d"
171+ Now: use repo_config if available, fallback to hardcoded value *)
168172 let gitlab_url =
169- f " https://gitlab.inria.fr/coq/coq/-/jobs/%d" job_info.build_id
173+ match repo_config with
174+ | Some config -> (
175+ match
176+ (config.gitlab_domain, config.gitlab_owner, config.gitlab_repo)
177+ with
178+ | Some domain , Some gl_owner , Some gl_repo ->
179+ f " https://%s/%s/%s/-/jobs/%d" domain gl_owner gl_repo
180+ job_info.build_id
181+ | _ ->
182+ f " https://gitlab.inria.fr/coq/coq/-/jobs/%d"
183+ job_info.build_id )
184+ | None ->
185+ f " https://gitlab.inria.fr/coq/coq/-/jobs/%d" job_info.build_id
170186 in
187+ Lwt_io. printl " Pushing status check for bench job."
188+ < &>
171189 let summary =
172190 f " ## GitLab Job URL:\n [GitLab Bench Job](%s)\n " gitlab_url
173191 in
@@ -231,14 +249,41 @@ let update_bench_status ~bot_info ~job_info (gh_owner, gh_repo) ~external_id
231249 | _ ->
232250 Lwt_io. printlf " Unknown state for bench job: %s" state ) )
233251
234- let run_bench ~bot_info ?(org = " rocq-prover" ) ?(team = " contributors" )
235- ?(gitlab_domain = " gitlab.inria.fr" ) ?key_value_pairs comment_info =
252+ let run_bench ~bot_info ~repo_config_table ?key_value_pairs comment_info =
236253 (* Do we want to use this more often? *)
237254 let open Lwt.Syntax in
238255 let pr = comment_info.issue in
239256 let owner = pr.issue.owner in
240257 let repo = pr.issue.repo in
241258 let pr_number = pr.number in
259+ let repo_config = get_repo_config_opt ~owner ~repo repo_config_table in
260+ (* Original: hardcoded org="rocq-prover", team="contributors", gitlab_domain="gitlab.inria.fr"
261+ Now: use repo_config if available, fallback to hardcoded values *)
262+ let org =
263+ match repo_config with
264+ | Some config -> (
265+ match config.org_name with Some org -> org | None -> " rocq-prover" )
266+ | None ->
267+ " rocq-prover"
268+ in
269+ let team =
270+ match repo_config with
271+ | Some config -> (
272+ match config.team_name with Some team -> team | None -> " contributors" )
273+ | None ->
274+ " contributors"
275+ in
276+ let gitlab_domain =
277+ match repo_config with
278+ | Some config -> (
279+ match config.gitlab_domain with
280+ | Some domain ->
281+ domain
282+ | None ->
283+ " gitlab.inria.fr" )
284+ | None ->
285+ " gitlab.inria.fr"
286+ in
242287 (* We need the GitLab build_id and project_id. Currently there is no good way
243288 to query this data so we have to jump through some somewhat useless hoops in
244289 order to get our hands on this information. TODO: do this more directly.*)
@@ -263,10 +308,24 @@ let run_bench ~bot_info ?(org = "rocq-prover") ?(team = "contributors")
263308 Lwt.return_error err
264309 | Ok summary -> (
265310 try
311+ (* Original: hardcoded GitLab URL " https :// gitlab.inria.fr/ coq/ coq/-/ jobs/ "
312+ Now: use repo_config if available, fallback to hardcoded value *)
313+ let gitlab_url_prefix =
314+ match repo_config with
315+ | Some config -> (
316+ match
317+ (config.gitlab_domain, config.gitlab_owner, config.gitlab_repo)
318+ with
319+ | Some domain, Some gl_owner, Some gl_repo ->
320+ f " https://% s/% s/% s/-/ jobs/ " domain gl_owner gl_repo
321+ | _ ->
322+ " https:// gitlab.inria.fr/ coq/ coq/-/ jobs/ " )
323+ | None ->
324+ " https:// gitlab.inria.fr/ coq/ coq/-/ jobs/ "
325+ in
266326 let build_id =
267327 let regexp =
268- f {|.*%s\( [0-9]*\) |}
269- (Str.quote " [bench](https://gitlab.inria.fr/coq/coq/-/jobs/" )
328+ f {|.*%s\([0-9]*\)|} (Str.quote (f " [bench](% s" gitlab_url_prefix))
270329 in
271330 ( if String_utils.string_match ~regexp summary then
272331 Str.matched_group 1 summary
0 commit comments