Add support for mirroring GitHub repositories to GitLab.

For now, the list of repositories is hardcoded. If we want to make
this configurable per repository, we need to ensure that the GitLab
repository does belong to the claimed GitHub owner, e.g., by checking
the configuration file both on GitHub and GitLab, or by requiring the
use of a specific GitLab project description with a backlink to the
GitHub repository.

Co-authored-by: Erik Martin-Dorel <[email protected]>

README.md

@@ -221,14 +221,24 @@ Once you finish the installation, follow these steps:
 
 - Create a repository on GitLab.com which will be used to run CI jobs.
 
-  The bot will only take care of mirroring the PRs and reporting
-  status checks back so you may still want to activate the mirroring
-  feature for the main branches.  To do so, the easiest way is to
-  choose the "CI/CD for external repo" option when creating the GitLab
-  repository.  However, you should opt to give the repo by URL rather
-  than with the GitHub button, because we won't need GitLab's own
-  status check reporting feature. (If it is already activated, you can
-  disable this integration in the "Settings" / "Integration" menu).
+  By default, the bot will only take care of mirroring the PRs and
+  reporting status checks back. So you may still want to activate:
+
+  - either GitLab's mirroring feature for the main branches.
+    (A drawback is the
+    [sync lag](https://docs.gitlab.com/ee/user/project/repository/mirror/#update-a-mirror)
+    (between 5' and 30') that occurs with this pull-based mirroring.)
+    If you do so, the easiest way is to choose the "CI/CD for external
+    repo" option when creating the GitLab repository.  However, you
+    should opt to give the repo by URL rather than with the GitHub
+    button, because we won't need GitLab's own status check reporting
+    feature. (If it is already activated, you can disable this
+    integration in the "Settings" / "Integration" menu).
+
+  - or **@coqbot**'s mirroring feature (it is a push-based mirroring).
+    For now, this requires hardcoding the GitHub / GitLab mapping in
+    the bot's source code.  Please open an issue if you would like to
+    use this feature. We plan to make this configurable in the future.
 
 - In your GitLab repository:
 

bot-components/GitHub_subscriptions.ml

@@ -143,11 +143,12 @@ let push_event_info_of_json json =
   in
   let repo = json |> member "repository" |> member "name" |> to_string in
   let base_ref = json |> member "ref" |> to_string in
+  let head_sha = json |> member "after" |> to_string in
   let commits = json |> member "commits" |> to_list in
   let commits_msg =
     List.map commits ~f:(fun c -> c |> member "message" |> to_string)
   in
-  {owner; repo; base_ref; commits_msg}
+  {owner; repo; base_ref; head_sha; commits_msg}
 
 type msg =
   | IssueOpened of issue_info

bot-components/GitHub_types.mli

@@ -85,7 +85,11 @@ type comment_info =
   ; id: GitHub_ID.t }
 
 type push_info =
-  {owner: string; repo: string; base_ref: string; commits_msg: string list}
+  { owner: string
+  ; repo: string
+  ; base_ref: string
+  ; head_sha: string
+  ; commits_msg: string list }
 
 type check_run_status = COMPLETED | IN_PROGRESS | QUEUED
 

src/actions.ml

@@ -2289,6 +2289,30 @@ let remove_labels_if_present ~bot_info (issue : issue_info) labels =
     |> add_remove_labels ~bot_info ~add:false issue )
   |> Lwt.async
 
+(* TODO: ensure there's no race condition for 2 push with very close timestamps *)
+let mirror_action ~bot_info ?(force = true) ~owner ~repo ~base_ref ~head_sha ()
+    =
+  (let open Lwt_result.Infix in
+  let local_ref = head_sha in
+  let gh_ref =
+    {repo_url= f "https://github.com/%s/%s" owner repo; name= base_ref}
+  in
+  (* TODO: generalize to case where mapping is not one-to-one *)
+  let gl_ref =
+    { repo_url= gitlab_repo ~bot_info ~gitlab_full_name:(owner ^ "/" ^ repo)
+    ; name= base_ref }
+  in
+  git_fetch gh_ref local_ref |> execute_cmd
+  >>= fun () -> git_push ~force ~remote_ref:gl_ref ~local_ref () |> execute_cmd
+  )
+  >>= function
+  | Ok () ->
+      Lwt.return_unit
+  | Error e ->
+      Lwt_io.printlf "Error while mirroring branch %s of repository %s/%s: %s"
+        base_ref owner repo e
+
+(* TODO: ensure there's no race condition for 2 push with very close timestamps *)
 let update_pr ?full_ci ?(skip_author_check = false) ~bot_info
     (pr_info : issue_info pull_request_info) ~gitlab_mapping ~github_mapping =
   let open Lwt_result.Infix in
@@ -2599,7 +2623,7 @@ let project_action ~bot_info ~(issue : issue) ~column_id =
   | _ ->
       Lwt_io.printf "This was not a request inclusion column: ignoring.\n"
 
-let push_action ~bot_info ~base_ref ~commits_msg =
+let coq_push_action ~bot_info ~base_ref ~commits_msg =
   Stdio.printf "Merge and backport commit messages:\n" ;
   let commit_action commit_msg =
     if string_match ~regexp:"^Merge PR #\\([0-9]*\\):" commit_msg then

src/actions.mli

@@ -76,12 +76,22 @@ val adjust_milestone :
 val project_action :
   bot_info:Bot_info.t -> issue:GitHub_types.issue -> column_id:int -> unit Lwt.t
 
-val push_action :
+val coq_push_action :
      bot_info:Bot_info.t
   -> base_ref:string
   -> commits_msg:string list
   -> unit Lwt.t
 
+val mirror_action :
+     bot_info:Bot_info.t
+  -> ?force:bool
+  -> owner:string
+  -> repo:string
+  -> base_ref:string
+  -> head_sha:string
+  -> unit
+  -> unit Lwt.t
+
 val ci_minimize :
      bot_info:Bot_info.t
   -> comment_info:GitHub_types.comment_info

src/bot.ml

@@ -207,14 +207,38 @@ let callback _conn req body =
         GitHub_subscriptions.receive_github ~secret:github_webhook_secret
           (Request.headers req) body
       with
-      | Ok (_, PushEvent {owner; repo; base_ref; commits_msg}) ->
+      | Ok (true, PushEvent {owner= "coq"; repo= "coq"; base_ref; commits_msg})
+        ->
           (fun () ->
             init_git_bare_repository ~bot_info
             >>= fun () ->
-            action_as_github_app ~bot_info ~key ~app_id ~owner ~repo
-              (push_action ~base_ref ~commits_msg) )
+            action_as_github_app ~bot_info ~key ~app_id ~owner:"coq" ~repo:"coq"
+              (coq_push_action ~base_ref ~commits_msg) )
           |> Lwt.async ;
-          Server.respond_string ~status:`OK ~body:"Processing push event." ()
+          Server.respond_string ~status:`OK
+            ~body:
+              "Processing push event on Coq repository: analyzing merge / \
+               backporting info."
+            ()
+      | Ok (true, PushEvent {owner; repo; base_ref; head_sha; _}) -> (
+        match (owner, repo) with
+        | "coq-community", ("docker-base" | "docker-coq")
+        (*| "math-comp", ("docker-mathcomp" | "math-comp")*) ->
+            (fun () ->
+              init_git_bare_repository ~bot_info
+              >>= fun () ->
+              action_as_github_app ~bot_info ~key ~app_id ~owner ~repo
+                (mirror_action ~owner ~repo ~base_ref ~head_sha ()) )
+            |> Lwt.async ;
+            Server.respond_string ~status:`OK
+              ~body:
+                (f
+                   "Processing push event on %s/%s repository: mirroring \
+                    branch on GitLab."
+                   owner repo )
+              ()
+        | _ ->
+            Server.respond_string ~status:`OK ~body:"Ignoring push event." () )
       | Ok (_, PullRequestUpdated (PullRequestClosed, pr_info)) ->
           (fun () ->
             init_git_bare_repository ~bot_info

src/git_utils.ml

@@ -57,7 +57,7 @@ let gitlab_ref ~bot_info ~(issue : issue) ~github_mapping ~gitlab_mapping =
   | Some r ->
       Lwt.return r )
   >|= fun gitlab_full_name ->
-  { name= f "pr-%d" issue.number
+  { name= f "refs/heads/pr-%d" issue.number
   ; repo_url= gitlab_repo ~gitlab_full_name ~bot_info }
 
 let ( |&& ) command1 command2 = command1 ^ " && " ^ command2
@@ -83,7 +83,7 @@ let git_fetch ?(force = true) remote_ref local_branch_name =
     (Stdlib.Filename.quote local_branch_name)
 
 let git_push ?(force = true) ?(options = "") ~remote_ref ~local_ref () =
-  f "git push %s %s%s:refs/heads/%s %s" remote_ref.repo_url
+  f "git push %s %s%s:%s %s" remote_ref.repo_url
     (if force then " +" else " ")
     (Stdlib.Filename.quote local_ref)
     (Stdlib.Filename.quote remote_ref.name)

src/git_utils.mli

@@ -1,3 +1,6 @@
+val gitlab_repo :
+  bot_info:Bot_components.Bot_info.t -> gitlab_full_name:string -> string
+
 val gitlab_ref :
      bot_info:Bot_components.Bot_info.t
   -> issue:Bot_components.GitHub_types.issue