Idris2 [RFC] Update Pull Request requirements

While thinking on this RFC, please keep in mind that this project is relatively small and maintained by a small number of people without consistent amounts of time available to put towards Idris2 at any given point in time. It's good to have processes but my goal is not to add a ton of overhead that isn't realistic for this project. I just admit there could be a bit more clarity and consistency.

[x] I have read CONTRIBUTING.md.
[x] I have checked that there is no existing PR/issue about my proposal.

Summary

This proposal is to modify the CONTRIBUTING document to more accurately and clearly reflect PR requirements at the same time as updating any supporting materials (like the PR template) and even get suggestions for potential CI automations that could help enforce guidelines if any come to mind.

Motivation

It has become apparent that the requirements in the CONTRIBUTING document are either (a) not all relevant or not all relevant all the time or (b) not followed all the time for lack of thinking of them or lack of motivation or lack of perceived importance.

While one response to this could be to just renew the sense of importance of such guidelines, it also seems clear that the guidelines could say more and be louder about some things while also being clear about what exceptions are made and when.

The proposal

I'd like to open this up to community input for the most part but there are a few suggestions from comments on https://github.com/idris-lang/Idris2/pull/3565 that I will mention here for starters.

We should re-emphasize the following sections of the contribution guidelines. [My take: Perhaps a more explicit section on Pull Request reviewing for some but not all of these; That would serve both to let submitters know how their PRs are reviewed and also reviewers know what they are expected to take into consideration].

Many contributions will require accompanying tests and documentation updates. Bugfixes in particular should be accompanied by tests, to avoid future regressions.

In all cases, a pull request must have a short description (one sentence is usually enough) that explains its purpose. However obvious you think it might be, it really helps when reviewing the changes.

Changes to prelude and base libraries 'prelude' and 'base' are, in some sense, part of the language. There are a lot of trade offs to be made in the design of the prelude especially - such as interface hierarchies - and while you may not agree with the way it looks, by and large these decisions have already been made so there must be a compelling reason for them to be changed.

We should merge CI changes similar to these that make it easier for us to be cognizent of the impact of breaking changes to libraries for which we have already stated we would like to have relative stability.
We should adopt a self-merge and merge-without-comment policy and follow it. I suggest the policy say that PRs will not be merged without any review comments or approval prior to a specified review window. Perhaps a few days or a work week. PRs that receive approval need not wait out that full window before merging. There would likely need to be other exemptions: hot fixes to bugs and fixes to CI issues may deserve mention as exempt from the review period limitation. This limitation isn't intended to artificially slow down progress, just give community and other maintainers adequate time to chime in even during an otherwise busy week. Self merging should be explicitly allowed given the size of our maintainer team but the aforementioned limitations on it seem reasonable to me.
We should consider adding a check box to our PR template for adding code documentation to any new library contributions (base, contrib, test, linear, etc) as a friendly reminder.

Now I cede the floor to you. Have I missed good suggestions? Do you object to any of the suggestions above? I don't think we need to wait for some sort of formal approval of this RFC as a whole to act. At some point in the future, someone will take points from this issue that were not objected to and act on them with changes to the CONTRIBUTING.md file or the PR template or the README as feels most appropriate.

Jun 03 '25 18:06 mattpolzin

All of this sounds good. Something I've been trying to unsuccessfully encourage in the past is to have PRs explain exactly what they are, why they exist, why they fix the problem, by requiring them to be paired with a comprehensively written issue. This way:

Reviewers know why the PR exist and can close them if they don't have a good reason to exist (fix a problem already being fixed by another PR/issue for example, fix a symptom rather than a cause, address a non-goal like changes additions to contrib or prelude)
Reviewers know what to look for. If the PR has a stated goal, the reviewer can use their knowledge of the codebase to be mindful about changes related to that specific goal
The community can easily give feedback in the issue comments. When a PR is submitted, the community loses their ability to evaluate the change, since the text is often written with other maintainers in mind and the code is essentially illegible for non-maintainers.

Maybe there is a way to reach the same goals without requiring an issue number upfront. But part of the reason why PRs remain unreviewed (and why maintainers end up merging their own stuff) is also because they are not easy to review, and therefore every step we take to ease that process will result in more PRs being reviewed more quickly, reducing the incentive for self-merge.

Jun 04 '25 11:06 andrevidela

Thanks for taking the time to start this process. The suggested changes sound reasonable to me. I'd also like to second Andre's suggestion that ideally, PRs are each paired with an issue.

I'd also like to stress that we should not blow up the standard libs with custom functionality, unless it has been agreed on that these are general enough to be included in base or even the prelude. Already now, we have some not so well documented (and, probably, not so well designed) modules in base, about which I'm quite sure they are hardly ever used in the wild. They make it hard for newcomers to find their way around and figure out which parts are actually important and which parts should probably be just ignored.

Jun 04 '25 13:06 stefan-hoeck

The danger of having issue first, implementation second is that it demands that reviewers invest a lot of time giving feedback on pie-in-the-sky proposals that never actually get implemented.

Jun 10 '25 10:06 gallais

Something I would like to submit here as a new concept in the current process is the notion of an "accepted" issue/proposal vs one that is "in discussion" or "rejected".

An example of this is issue #3355 which has a proposal, some discussion, and even a prototype implemented. But no conclusion: Should it be implemented? Should it not be implemented? What is the cutoff for making that decision and what timeline should we expect from them?

To solve the problem of proposals stuck in limbo I suggest the following:

4 new meta-tags for issues "in Discussion", "stale", "accepted", "rejected"
Every bug report is automatically "accepted"
Every proposal starts with "in discussion"
A maintainer can give their support with a message along the lines of "I believe this is a positive change and I vouch for it to be accepted ✅ "
A maintainer can reject the proposal if it is fundamentally incompatible with Idris2's design goals, citing the CONTRIBUTING document, FAQ, or documentation. A proposal can also be rejected if it is not comprehensive enough to be evaluated.
If no maintainers reject the proposal, and at least 2 other maintainers vouch for it, the proposal is accepted.
Support for a proposal does not mean committing for maintenance or reviewing.
Once an issue is "accepted" any PR fixing it can be merged knowing that it is indeed solving a problem that was recognised as requiring a solution.
A PR should not be merged for an proposal that is not "accepted"
After 6 months of inactivity, an issue "in discussion" is "stale".
Because changes in the compiler can invalidate older knowledge, a "stale" proposal needs to be revised to modern standards if it is to be revived. In that case it can move back to "in discussion"

This seems like a lot of text but the only thing that changes is that if we see something that's obviously inadequate, we can mark it as rejected, give a good reason and close it. If we see something nice that should be done, we mark it as "accepted". If something is marked "stale" we know that we can't rely on its current state because the discussion and knowledge might be outdated. This also remove the uncertaintly about a PR linked to an issue where there is no real way to know why the PR exists in the first place for example #3531 links to a comment on discord (which should never be done) but no real thought has been given to how this impacts downstream libraries or how/when to update them. This issue would still be tagged "in discussion" and the PR shouldn't be merged

Jun 22 '25 16:06 andrevidela