An RFC for creating an RFC process. :) #1543

celinval · 2022-08-18T00:37:57Z

Description of changes:

I am creating this PR to gather feedback on the following:

Should we start an RFC process? If we do:
How would that process look like?
What do we expect to be included in an RFC?

I would like to suggest that we do start a light-weight RFC process. In this PR, I included a suggestion of a process and a suggestion of a template. Finally, this PR also creates a book of RFCs under kani/rfcs.

My reasoning here is that the RFC process will:

Improve collaboration by requesting comments at an earlier stage of development.
Provide better user experience by writing the RFCs starting from the user impact.
improve the quality of our software by thinking in terms of architecture.
improve our documentation

The main drawback is the time overhead to write the RFC and iterating over the feedback. So we should aim to make this a lightweight process. The RFC doesn't have to answer all questions and it can be updated as we go.

Resolved issues:

N/A

Call-outs:

I am suggesting that RFCs require at least 2 approvals, but I haven't looked into how we could enforce it yet.

Testing:

How is this change tested? N/A
Is this a refactor change? N/A

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

This PR itself is our first RFC. :)

rfcs/src/intro.md

jaisnan · 2022-08-18T16:18:07Z

Thank you! I have a few questions as someone unfamiliar with the RFC process -

Is the RFC process supposed to formalize and replace the internal document writing process? If not, when do we decide to make it an RFC and when do we make it a design document?
Do all RFC's need to be public facing or can the person proposing the RFC choose to make it not available to the public?
What is the reasoning behind closing the PR for an RFC once it's not approved? Is the person expected to come up with a new RFC with the feedback given?

Co-authored-by: Jaisurya Nanduri <[email protected]>

rfcs/src/intro.md

rfcs/src/template.md

danielsn · 2022-08-18T18:34:40Z

Thank you! I have a few questions as someone unfamiliar with the RFC process -

Is the RFC process supposed to formalize and replace the internal document writing process? If not, when do we decide to make it an RFC and when do we make it a design document?

Yes, the RFC mechanism will be the Kani process going forward.

Do all RFC's need to be public facing or can the person proposing the RFC choose to make it not available to the public?

Yes. We expect every RFC to be public since the changes would be made public too. For changes that are still under development, it might make sense to open a "Draft" RFC

What is the reason behind closing the PR for an RFC once it's not approved? Is the person expected to come up with a new RFC with the feedback given?

If an RFC is not accepted, the next steps are up to the author (much like when a paper is not accepted by a peer review process). Depending on their judgement, they can abandon the RFC, start a new RFC with a different approach, or revise their current approach to address the reviewer feedback.

danielsn

We should add the RFC to the PR template

rfcs/src/intro.md

danielsn · 2022-08-18T18:42:25Z

rfcs/src/intro.md

+This is the overall workflow for the RFC process:
+
+```toml
+    Create RFC ──> Receive Feedback  ──> Accepted?


You might want to note the recieve feedback/revise loop.

Also, the Implement -> Revise RFC feedback edge

I added the first. The second I added a note to the item below (I'm worried that the diagram is getting too complicated). Is that OK?

danielsn · 2022-08-18T18:43:16Z

rfcs/src/intro.md

+
+1. Create an RFC
+   1. Start from a fork of the Kani repository.
+   2. Copy the template file ([`rfcs/src/template.md`](./template.md)) to `rfcs/src/<my-feature>.md`.


I like having numbered RFCs. Perhaps say copy to rfcs/src/<ID_NUMBER><my-feature>.md

I added the ID_NUMBER. Any suggestion on how this will be assigned? We can either try to increment based on existing RFCs and open RFCs or we can use the tracking issue number.

danielsn · 2022-08-18T18:44:24Z

rfcs/src/intro.md

+2. Build consensus and integrate feedback.
+   1. RFCs should get approved by at least 2 members of the `kani-developers` team.
+   2. Once the RFC has been approved, update the RFC status and merge the PR.
+   3. If the RFC is not approved, close the PR without merging.


If the RFC is not approved, replace status of the RFC with a template saying "Closed as per PR blah"

Actually, I think that's ok.

rfcs/src/intro.md

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

tedinski · 2022-08-22T17:50:39Z

rfcs/src/intro.md

+## When to create an RFC
+
+As a rule of thumb you should create an RFC if you are making changes that impact the user experience. New 
+APIs, new features, as well as depreciation, should follow an RFC process. We also ask for substantial architectural 


IMO, we should be explicit about a lighter-weight process option here. Changes are usually going to be:

Simple enough to not need an RFC

Complex enough to merit discussion and get consensus on design choices, but perhaps as a github issue rather than an RFC proper.

Important enough to merit an RFC-like process, especially when it comes to soliciting customer feedback.

I would prefer start with 2 modes only. For the case where it merit discussion and get consensus, I would prefer using an RFC PR instead of an issue. It's OK if the RFC document is fairly small.

We can adjust as we go.

rfcs/src/intro.md

adpaco-aws · 2022-08-25T16:08:11Z

rfcs/src/intro.md

+   3. Fill in the details according to the template intructions.
+   4. Submit a pull request.
+2. Build consensus and integrate feedback.
+   1. RFCs should get approved by at least 2 members of the `kani-developers` team.


I think it's kani-devs.

I actually removed the group name here. I still need to figure out a way to enforce this without changing all our PRs.

rfcs/src/template.md

adpaco-aws · 2022-08-25T16:13:53Z

rfcs/src/template.md

+- Will this require any new dependency?
+- What are the corner cases you antecipate?
+
+# Rationale and alternatives


This could just be part of "Detailed design".

Hummm... That's an interesting point. I can see that in some cases that would make sense.

The reason I believe this is not inside "Detailed Design" because the "Rationale and alternatives" may go beyond the implementation details. In some cases, the alternative could be providing a completely different user experience to achieve the same purpose. Like this rust RFC.

Does it make sense?

Yes, it does.

For the record, I was looking to reduce the number of sections here as I don't think Kani is more complex than the Rust compiler, and in my opinion Kani's RFCs shouldn't be more complex than Rust's RFCs neither. That said, we don't have any RFC experience at the moment so it's hard to tell if this is too much. Let's revisit this in the future, when we've had some RFCs (in particular, at least one coming from external contributors) so we can get some feedback based on their experience.

rfcs/src/template.md

scripts/build-docs.sh

adpaco-aws · 2022-08-25T16:30:58Z

rfcs/src/intro.md

+   4. Document how to use the feature.
+4. Stabilization.
+   1. After the feature has been implemented, start the stabilization process.
+   2. Gather user feedback and make necessary adjustments.


We should define some criteria to stabilize a feature. This reads like "Stabilize right away after implementing it", when in practice we will wait for a feature to be stabilized after a period. Recent bug reports or short periods after implementation should all delay the stabilization of a feature.

Yeah, I totally agree. Any suggestions?

I would prefer keeping it lightweight for now. Something like creating a PR that marks the RFC as stable and remove the --enable-unstable requirement. In the description of the PR, the developer states why they believe the feature can be marked as stable and we go from there. I guess we could add a minimum "bake" time like 2 releases.

I think for the rust project, they have two different process which is more heavy weight. This includes writing a report and starting an FCP (final comment period).

I added a stage between "Implementation" and "Stabilization". Let me know what you think.

Thanks for adding another stage. I think that makes clear there is not an immediate path to stabilization, while at the same time keeping the process lightweight as we want.

Co-authored-by: Adrian Palacios <[email protected]>

celinval · 2022-08-25T22:10:11Z

@danielsn I added the "proof-of-concept" field, but I'm having second thoughts on this one. Developers will likely link this against some branch in their fork and this branch will likely be deleted. I think it would make more sense to add that link to the PR description itself. What do you think?

adpaco-aws

Thanks for doing this!

adpaco-aws · 2022-08-30T18:53:49Z

rfcs/src/template.md

+- Will this require any new dependency?
+- What are the corner cases you antecipate?
+
+# Rationale and alternatives


Yes, it does.

For the record, I was looking to reduce the number of sections here as I don't think Kani is more complex than the Rust compiler, and in my opinion Kani's RFCs shouldn't be more complex than Rust's RFCs neither. That said, we don't have any RFC experience at the moment so it's hard to tell if this is too much. Let's revisit this in the future, when we've had some RFCs (in particular, at least one coming from external contributors) so we can get some feedback based on their experience.

adpaco-aws · 2022-08-30T21:09:09Z

rfcs/src/intro.md

+   4. Document how to use the feature.
+4. Stabilization.
+   1. After the feature has been implemented, start the stabilization process.
+   2. Gather user feedback and make necessary adjustments.


Thanks for adding another stage. I think that makes clear there is not an immediate path to stabilization, while at the same time keeping the process lightweight as we want.

rfcs/src/template.md

tedinski

Ship it, let's try it and see how it goes.

One last question: this creates the /rfcs/ directory (should it be just /rfc/ perhaps?) but nothing links to it. Should we add a link from our regular docs to the "rfc book" ?

celinval · 2022-08-31T19:09:44Z

Ship it, let's try it and see how it goes.

One last question: this creates the /rfcs/ directory (should it be just /rfc/ perhaps?) but nothing links to it. Should we add a link from our regular docs to the "rfc book" ?

Great question! I am happy to rename it to /rfc/ or /rfc-book/. Any preference?

I like the idea of adding a link to it from our regular docs. Initially I wanted to make sure they would play nice to each other, but I was able to test that in my fork, and I don't see why not. Should I just add a link in the Summary table?

tedinski · 2022-08-31T19:13:59Z

I like /rfc/.

A link from the summary works for me.

celinval · 2022-08-31T20:00:06Z

Unfortunately, a link from the summary won't work. mdbook doesn't support external links inside SUMMARY.md (rust-lang/mdBook#919). There is a very hacky way to do it as described in rust-lang/mdBook#1354, but I don't think it's worth it.

I'll add a link under Project Status for now. Let me know if you have any other suggestion.

1- Renamed rfcs/ to rfc/ 2- Small tweaks with the template format to make it cleaner. 3- Added a list to the RFC Book from the user document.

celinval added 3 commits August 17, 2022 14:59

Move build docs script to be under scripts/

b791416

Add RFC book and an RFC template

3a2e68c

This PR itself is our first RFC. :)

Build rfc book as part of build docs

8959d49

celinval requested a review from a team as a code owner August 18, 2022 00:37

Update kani.yml

ba29b07

jaisnan reviewed Aug 18, 2022

View reviewed changes

rfcs/src/intro.md Outdated Show resolved Hide resolved

jaisnan reviewed Aug 18, 2022

View reviewed changes

rfcs/src/intro.md Outdated Show resolved Hide resolved

Apply suggestions from code review

57f192a

Co-authored-by: Jaisurya Nanduri <[email protected]>

celinval commented Aug 18, 2022

View reviewed changes

rfcs/src/intro.md Outdated Show resolved Hide resolved

celinval commented Aug 18, 2022

View reviewed changes

rfcs/src/template.md Outdated Show resolved Hide resolved

danielsn reviewed Aug 18, 2022

View reviewed changes

Apply suggestions from code review

fc6473c

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

tedinski reviewed Aug 22, 2022

View reviewed changes

adpaco-aws reviewed Aug 25, 2022

View reviewed changes

celinval and others added 2 commits August 25, 2022 11:19

Apply suggestions from code review

ee02f51

Co-authored-by: Adrian Palacios <[email protected]>

Address feedback

766fc6d

celinval force-pushed the rfcs branch from eb72577 to 766fc6d Compare August 25, 2022 21:49

adpaco-aws approved these changes Aug 30, 2022

View reviewed changes

Merge branch 'main' into rfcs

6ef3954

tedinski approved these changes Aug 31, 2022

View reviewed changes

Small adjustments:

cb9b5ab

1- Renamed rfcs/ to rfc/ 2- Small tweaks with the template format to make it cleaner. 3- Added a list to the RFC Book from the user document.

celinval merged commit c32f0bc into model-checking:main Sep 1, 2022

celinval added a commit to celinval/kani-dev that referenced this pull request Sep 2, 2022

Move folder rfcs -> rfc per model-checking#1543

ceacdfb

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

An RFC for creating an RFC process. :) #1543

An RFC for creating an RFC process. :) #1543

celinval commented Aug 18, 2022 •

edited

Loading

jaisnan commented Aug 18, 2022 •

edited

Loading

danielsn commented Aug 18, 2022

danielsn left a comment

danielsn Aug 18, 2022

celinval Aug 25, 2022

danielsn Aug 18, 2022

celinval Aug 25, 2022

danielsn Aug 18, 2022

celinval Aug 25, 2022 •

edited

Loading

tedinski Aug 22, 2022

celinval Aug 22, 2022

adpaco-aws Aug 25, 2022

celinval Aug 25, 2022

adpaco-aws Aug 25, 2022

celinval Aug 25, 2022

adpaco-aws Aug 30, 2022

adpaco-aws Aug 25, 2022

celinval Aug 25, 2022

celinval Aug 25, 2022

adpaco-aws Aug 30, 2022

celinval commented Aug 25, 2022

adpaco-aws left a comment

adpaco-aws Aug 30, 2022

adpaco-aws Aug 30, 2022

tedinski left a comment

celinval commented Aug 31, 2022

tedinski commented Aug 31, 2022

celinval commented Aug 31, 2022

An RFC for creating an RFC process. :) #1543

An RFC for creating an RFC process. :) #1543

Conversation

celinval commented Aug 18, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

jaisnan commented Aug 18, 2022 • edited Loading

danielsn commented Aug 18, 2022

danielsn left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval Aug 25, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval commented Aug 25, 2022

adpaco-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tedinski left a comment

Choose a reason for hiding this comment

celinval commented Aug 31, 2022

tedinski commented Aug 31, 2022

celinval commented Aug 31, 2022

celinval commented Aug 18, 2022 •

edited

Loading

jaisnan commented Aug 18, 2022 •

edited

Loading

celinval Aug 25, 2022 •

edited

Loading