Skip to content

Differentiate types for "Pull Request Simple" and "Pull Request" to support richer data in Github_core.Pull.get #267

@shonfeder

Description

@shonfeder

Currently, both Github_core.Pull.get and Gitub_core.Pull.for_repo both return values of type pull.

My understanding is that, type pull represents what the GitHub API (in the response schema for the repos/OWNER/REPO/pulls endpoint) calls a "Pull Request Simple".

However, the repos/OWNER/REPO/pulls/PULL_NUMBER endpoint (for fetching a single pull request) returns what GitHub calls in the response schema a "Pull Request".

Critically for my purposes, the "Pull Request" object includes many properties that are omitted from the "Pull Request Simple" object, including properties that indicate whether a PR is mergable or whether it has auto_merge enabled.

If we wanted to support inspecting these extended attributes, I think we'd need to introduce a new ATD type that inherited from and extended type pull, and then adapt Github_core.Pull.get to deserialize into the corresponding record.

Perhaps this new type could be something like the following?

type pull_full = {
  mergeable: bool;
  (* etc... *)
  inherit pull
}

If maintaining backwards compatibility where not paramount, you might instead rename the current type pull as type pull_simple to more closely reflect the GitHub API.

On the other hand, to avoid breaking backwards compatibility, we might introduce a new function Github_core.Pull.get_full.

What do you all think of pursuing some such change?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions