Remove the optional of github_token, make github_pat optional (#361)

Author: lykimq

README.md

@@ -196,25 +196,6 @@ you are interested in hearing about it.
 
 ## How to use the **@coqbot** instance ##
 
-### As a GitHub App
-
-This is the recommended installation method, as this is both easier to
-set up and it gives access to new features (related to GitHub Checks).
-
-Notes:
-
-- Installation as a GitHub App is still in an experimental stage
-and you may frequently receive requests to expand permissions.
-
-- All the repositories that use the bot and belong to the same
-owner must install the bot using the same method (GitHub App or
-regular user).
-
-- If you were previously using the legacy installation method,
-make sure you disable any previously set up GitHub webhooks when
-switching to the GitHub App, otherwise the bot will receive every
-request twice.
-
 The bot can be installed as a GitHub App to either your account or
 organization ([link to app](https://github.com/apps/coqbot-app)).
 Once you finish the installation, follow these steps:
@@ -271,32 +252,6 @@ Once you finish the installation, follow these steps:
   configuration file becomes `BOT_NAME.toml` where `BOT_NAME` is the name
   of the bot.
 
-### As a regular user account (legacy)
-
-The bot used to be given access to each of your GitHub repositories as a
-regular GitHub user account (**@coqbot**). This installation method is
-still supported for repositories that haven't migrated to the GitHub App
-yet. Here are the steps to follow in addition to those described in the 
-`As GitHub App` section:
-
-- In your GitHub repository:
-
-  - go to "Settings" / "Manage access" to add
-    [**@coqbot**](https://github.com/coqbot) as a collaborator with
-    the "Write" role (so that it can push status checks, and set
-    labels).
-
-    Currently, every invitation requires a manual validation, so there
-    may be some lag before **@coqbot** can push status checks
-    to your repository.
-
-  - go to "Settings" / "Webhooks" and add one webhook with URL
-    <https://coqbot.herokuapp.com/github> that will only be triggered
-    at least by pull request events, and if you want to use the issue
-    milestone feature, by issue events as well.  Make sure you change
-    the "content/type" value to "application/json".
-
-  
 
 ## Architecture ##
 
@@ -352,14 +307,16 @@ to [Heroku](https://www.heroku.com/). Simply follow the official
 The bot will need to read a few environment variables so make sure
 these are configured in your Heroku app:
 
-- `GITHUB_ACCESS_TOKEN` (can also be defined in the configuration file as `github.api_token`)
 - `GITLAB_ACCESS_TOKEN` (can also be defined for each GitLab instance through the configuration file as `api_token` or through an environment variable whose name is defined in the configuration file as `api_token_env_var`)
 - `GITHUB_WEBHOOK_SECRET` (can also be defined in the configuration file as `github.webhook_secret`)
 - `GITLAB_WEBHOOK_SECRET` (can also be defined in the configuration file as `gitlab.webhook_secret`, will default to `GITHUB_WEBHOOK_SECRET` if not defined)
 - `DAILY_SCHEDULE_SECRET` (can also be defined in the configuration file as `github.daily_schedule_secret`, will default to `GITHUB_WEBHOOK_SECRET` if not defined)
 - `GITHUB_APP_ID` (can also be defined in the configuration file as `github.app_id`)
 - `GITHUB_PRIVATE_KEY` (a private key of your GitHub app)
 - `PORT` (can also be defined in the configuration file as `server.port`)
+- (optional) `GITHUB_ACCESS_TOKEN` / `github.api_token` in config: only needed
+  for Rocq minimization flows that must act as the `coqbot` user rather than
+  the GitHub App
 
 Then, you must configure the bot with a configuration file. Here is an example
 to adapt to your needs [`example-config.toml`](example-config.toml).

bot-components/Bot_info.ml

@@ -2,19 +2,23 @@ open Base
 
 type t =
   { gitlab_instances: (string, string * string) Hashtbl.t
-  ; github_pat: string
-  ; github_install_token: string option
+  ; github_pat: string option
+  ; github_install_token: string
   ; github_name: string
   ; email: string
   ; domain: string
   ; app_id: int }
 
-let github_token bot_info =
-  match bot_info.github_install_token with
-  | Some t ->
-      t
+let github_pat bot_info =
+  match bot_info.github_pat with
+  | Some pat ->
+      pat
   | None ->
-      bot_info.github_pat
+      failwith
+        "No GitHub PAT available. This operation requires a GitHub PAT. Please \
+         ensure the PAT is set in the configuration."
+
+let github_token bot_info = bot_info.github_install_token
 
 let gitlab_name_and_token bot_info gitlab_domain =
   match Hashtbl.find bot_info.gitlab_instances gitlab_domain with

bot-components/Bot_info.mli

@@ -1,12 +1,14 @@
 type t =
   { gitlab_instances: (string, string * string) Base.Hashtbl.t
-  ; github_pat: string
-  ; github_install_token: string option
+  ; github_pat: string option
+  ; github_install_token: string
   ; github_name: string
   ; email: string
   ; domain: string
   ; app_id: int }
 
+val github_pat : t -> string
+
 val github_token : t -> string
 
 val gitlab_token : t -> string -> (string, string) Result.t

bot-components/GitHub_subscriptions.ml

@@ -235,6 +235,10 @@ let github_event ~event json =
   | _ ->
       Ok (UnsupportedEvent (f "Unsupported GitHub event %s." event))
 
+let legacy_webhook_log =
+  "Error: received GitHub webhook without installation.id (legacy installation \
+   method)"
+
 let receive_github ~secret headers body =
   let open Result.Monad_infix in
   match Header.get headers "X-GitHub-Event" with
@@ -258,6 +262,11 @@ let receive_github ~secret headers body =
               Error "Webhook comes from a GitHub App, but it is not signed."
         with Yojson.Json_error _ | Type_error _ -> Ok None )
       >>= fun install_id ->
+      ( match install_id with
+      | None ->
+          Stdio.eprintf "%s\n" legacy_webhook_log
+      | Some _ ->
+          () ) ;
       github_event ~event json |> Result.map ~f:(fun r -> (install_id, r))
     with
     | Yojson.Json_error err ->

bot-components/GitHub_subscriptions.mli

@@ -16,6 +16,8 @@ type msg =
   | PushEvent of push_info
   | UnsupportedEvent of string
 
+val legacy_webhook_log : string
+
 val receive_github :
      secret:string
   -> Cohttp.Header.t

bot-components/Github_installations.ml

@@ -19,7 +19,7 @@ let action_with_new_installation_token ~bot_info ~key ~app_id ~install_id action
           ~data:(install_token, expiration_date)
       in
       let bot_info : Bot_info.t =
-        {bot_info with github_install_token= Some install_token}
+        {bot_info with github_install_token= install_token}
       in
       action ~bot_info
   | Error err ->
@@ -42,7 +42,7 @@ let action_as_github_app_from_install_id ~bot_info ~key ~app_id ~install_id
           action )
       else
         let bot_info : Bot_info.t =
-          {bot_info with github_install_token= Some install_token}
+          {bot_info with github_install_token= install_token}
         in
         action ~bot_info
   | None ->

bot-components/GraphQL_query.ml

@@ -19,7 +19,7 @@ let send_graphql_query ~bot_info ?(extra_headers = []) ?(ignore_errors = false)
   | GitLab gitlab_domain ->
       gitlab_name_and_token bot_info gitlab_domain
   | GitHub ->
-      Ok (bot_info.github_name, github_token bot_info) )
+      Ok (bot_info.github_name, bot_info.github_install_token) )
   |> Lwt.return
   >>= fun (name, token) ->
   let headers =

bot-components/HTTP_utils.ml

@@ -21,7 +21,7 @@ let headers_of_list = headers
 
 (* GitHub authorization header builder *)
 let github_header bot_info =
-  [("Authorization", "bearer " ^ github_token bot_info)]
+  [("Authorization", "bearer " ^ bot_info.github_install_token)]
 
 (* GitHub API preview headers *)
 let project_api_preview_header =

src/actions_job.ml

@@ -47,19 +47,19 @@ let job_action ~bot_info
                     Lwt.return_unit )
             in
             Ci_job_status.job_failure ~bot_info job_info ~pr_num
-              (gh_owner, gh_repo) ~github_repo_full_name ~gitlab_domain
-              ~gitlab_repo_full_name ~context ~failure_reason ~external_id
-              ~summary_builder ~allow_failure_handler ()
+              (gh_owner, gh_repo) ~gitlab_domain ~gitlab_repo_full_name ~context
+              ~failure_reason ~external_id ~summary_builder
+              ~allow_failure_handler ()
         | "success" as state ->
             Ci_job_status.job_success_or_pending ~bot_info (gh_owner, gh_repo)
-              job_info ~github_repo_full_name ~gitlab_domain
-              ~gitlab_repo_full_name ~context ~state ~external_id
+              job_info ~gitlab_domain ~gitlab_repo_full_name ~context ~state
+              ~external_id
             <&> Ci_documentation.send_doc_url ~bot_info job_info
                   ~github_repo_full_name
         | ("created" | "running") as state ->
             Ci_job_status.job_success_or_pending ~bot_info (gh_owner, gh_repo)
-              job_info ~github_repo_full_name ~gitlab_domain
-              ~gitlab_repo_full_name ~context ~state ~external_id
+              job_info ~gitlab_domain ~gitlab_repo_full_name ~context ~state
+              ~external_id
         | "cancelled" | "canceled" | "pending" ->
             (* Ideally we should check if a status was already reported for
                this job.  But it is important to avoid making dozens of

src/actions_pr_sync.ml

@@ -1,6 +1,5 @@
 open Base
 open Bot_components
-open Bot_components.Bot_info
 open Bot_components.GitHub_types
 open Bot_components.GitHub_GitLab_sync
 open Cohttp_lwt_unix
@@ -145,38 +144,25 @@ let update_pr ?full_ci ?(skip_author_check = false) ~bot_info
     (* Add rebase label if it exists *)
     GitHub_automation.add_labels_if_absent ~bot_info pr_info.issue [rebase_label] ;
     (* Add fail status check *)
-    match bot_info.github_install_token with
-    | None ->
-        GitHub_mutations.send_status_check
-          ~repo_full_name:
-            (f "%s/%s" pr_info.issue.issue.owner pr_info.issue.issue.repo)
-          ~commit:pr_info.head.sha ~state:"error" ~url:""
-          ~context:"GitLab CI pipeline (pull request)"
-          ~description:
-            "Pipeline did not run on GitLab CI because PR has conflicts with \
-             base branch."
-          ~bot_info
+    let open Lwt.Infix in
+    let open Lwt.Syntax in
+    GitHub_queries.get_repository_id ~bot_info ~owner:pr_info.issue.issue.owner
+      ~repo:pr_info.issue.issue.repo
+    >>= function
+    | Ok repo_id ->
+        (let+ _ =
+           GitHub_mutations.create_check_run ~bot_info
+             ~name:"GitLab CI pipeline (pull request)" ~status:COMPLETED
+             ~repo_id ~head_sha:pr_info.head.sha ~conclusion:FAILURE
+             ~title:
+               "Pipeline did not run on GitLab CI because PR has conflicts \
+                with base branch."
+             ~details_url:"" ~summary:"" ()
+         in
+         () )
         |> Lwt_result.ok
-    | Some _ -> (
-        let open Lwt.Infix in
-        let open Lwt.Syntax in
-        GitHub_queries.get_repository_id ~bot_info
-          ~owner:pr_info.issue.issue.owner ~repo:pr_info.issue.issue.repo
-        >>= function
-        | Ok repo_id ->
-            (let+ _ =
-               GitHub_mutations.create_check_run ~bot_info
-                 ~name:"GitLab CI pipeline (pull request)" ~status:COMPLETED
-                 ~repo_id ~head_sha:pr_info.head.sha ~conclusion:FAILURE
-                 ~title:
-                   "Pipeline did not run on GitLab CI because PR has conflicts \
-                    with base branch."
-                 ~details_url:"" ~summary:"" ()
-             in
-             () )
-            |> Lwt_result.ok
-        | Error e ->
-            Lwt.return (Error e) ) )
+    | Error e ->
+        Lwt.return (Error e) )
 
 let run_ci_action ~bot_info ~comment_info ?full_ci ~gitlab_mapping
     ~github_mapping () =