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
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions