Remove Legacy bot installation using PAT #354
Conversation
…them directly to use in bot
…ations, prepare for removal later
…nstallation.id and without it
…AT, remove GITHUB_ACCESS_TOKEN
lykimq
force-pushed
the
quyen@remove_legacy_isntallation
branch
from
ff51f3a to
600d086
Compare
|
There are still some commits that look like they are coming from previous PRs, making the diff view less usable to review this particular PR. |
bot-components/Git_utils.ml
Outdated
| let init_git_bare_repository ~bot_info = | ||
| let* () = Lwt_io.printl "Initializing repository..." in | ||
| let github_token = Bot_info.github_token bot_info in | ||
| "git init --bare" | ||
| |&& f {|git config user.email "%s"|} bot_info.email | ||
| |&& f {|git config user.name "%s"|} bot_info.github_name | ||
| |> execute_cmd ~mask:[bot_info.github_pat] (* TODO: direct PAT usage *) | ||
| |> execute_cmd ~mask:[github_token] |
There was a problem hiding this comment.
In this case, I think we should just simplify this by removing the ~mask argument (which probably served no purpose in this case).
| (* To delete the 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 *) | ||
| (* TODO: direct PAT usage *) | ||
| (f "git push https://%s:%[email protected]/%s.git --delete '%s" | ||
| bot_info.github_name bot_info.github_pat repo_name | ||
| branch_name ) | ||
| bot_info.github_name | ||
| (Bot_info.github_token bot_info) | ||
| repo_name branch_name ) |
There was a problem hiding this comment.
I was looking for things like this: here the reason for the direct PAT usage is precisely that we need to do this action as a GitHub account rather than as a GitHub App. So the GitHub PAT should actually not be removed, but its use should be confined to these very specific use cases.
| (* 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 github_token = github_token bot_info in | ||
| Stdlib.Filename.quote_command "./coq_bug_minimizer.sh" | ||
| [ script | ||
| ; GitHub_ID.to_string comment_thread_id | ||
| ; comment_author | ||
| ; bot_info.github_pat | ||
| ; github_token | ||
| ; bot_info.github_name | ||
| ; bot_info.domain | ||
| ; owner | ||
| ; repo | ||
| ; coq_version | ||
| ; ocaml_version | ||
| ; String.concat ~sep:" " minimizer_extra_arguments ] | ||
| |> execute_cmd ~mask:[bot_info.github_pat] | ||
| |> execute_cmd ~mask:[github_token] |
There was a problem hiding this comment.
Again, this is a legitimate use of the GitHub PAT (as explained by the comment). (And same thing, later in this file.)
src/webhook_github.ml
Outdated
| "[WARNING: Legacy Mode] Webhook received WITHOUT installation.id - \n\n\ | ||
| \ Will attempt PAT fallback (will fail with invalid token)" ) | ||
| "[INFO] Webhook received without installation.id (legacy webhook \ | ||
| format, GitHub App installation required for actions)" ) |
There was a problem hiding this comment.
Why not turn this into an error?
| type t = | ||
| { gitlab_instances: (string, string * string) Hashtbl.t | ||
| ; github_pat: string | ||
| ; github_install_token: string option | ||
| ; github_name: string | ||
| ; email: string | ||
| ; domain: string | ||
| ; app_id: int } | ||
|
|
||
| (* Returns the GitHub installation token. Requires installation token to be set. *) | ||
| let github_token bot_info = | ||
| match bot_info.github_install_token with | ||
| | Some t -> | ||
| t | ||
| | None -> | ||
| bot_info.github_pat | ||
| (* TODO: use Result.t later *) | ||
| failwith | ||
| "GitHub installation token is required. Please ensure the GitHub App \ | ||
| is installed and an installation token is available." |
There was a problem hiding this comment.
Avoid leaving exceptions in finished code except in very specific cases. Here, my suggestion is that instead of handling the case where github_install_token is None, we just make it a mandatory parameter, just like github_name, etc.
OTOH, github_pat is the one which we want to make optional, just for the few legitimate uses (that are all specific to the Rocq minimization feature). Since the function github_token then becomes trivial, it can just be replaced by direct use of .github_install_token.
Depend on #352
GITHUB_ACCESS_TOKENusage in source codeBot_info.github_tokenrequires installation token and fails if missingREADME.md: removeGITHUB_ACCESS_TOKEN, sectionAs a regular user account (legacy)example-config.toml: removegithub.api_tokentest/test_bot_info: tests installation token usage and failure when missingtest/test_webhook: tests webhook parsing with and withoutinstallation.id