From c32f0bc680cf9cfc1c190498d052c39c29ad23c4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 1 Sep 2022 08:44:22 -0700 Subject: [PATCH] An RFC for creating an RFC process. :) (#1543) * Move build docs script to be under scripts/ * Add RFC book and an RFC template * Build rfc book as part of build docs . Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Co-authored-by: Daniel Schwartz-Narbonne Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .github/PULL_REQUEST_TEMPLATE.md | 6 +++ .github/workflows/kani.yml | 2 +- docs/src/getting-started.md | 2 + rfc/book.toml | 17 +++++++++ rfc/src/SUMMARY.md | 9 +++++ rfc/src/intro.md | 64 ++++++++++++++++++++++++++++++++ rfc/src/template.md | 54 +++++++++++++++++++++++++++ {docs => scripts}/build-docs.sh | 16 +++++++- 8 files changed, 168 insertions(+), 2 deletions(-) create mode 100644 rfc/book.toml create mode 100644 rfc/src/SUMMARY.md create mode 100644 rfc/src/intro.md create mode 100644 rfc/src/template.md rename {docs => scripts}/build-docs.sh (81%) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 279a044146ac..7635b0adccf5 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -7,6 +7,12 @@ Describe Kani's current behavior and how your code changes that behavior. If the Resolves #ISSUE-NUMBER +### Related RFC: + + +Optional #ISSUE-NUMBER. ### Call-outs: diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 8a8208369452..9c8b7ec043e6 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -82,7 +82,7 @@ jobs: # On one OS only, build the documentation, too. - name: Build Documentation - run: ./docs/build-docs.sh + run: ./scripts/build-docs.sh # When we're pushed to main branch, only then actually publish the docs. - name: Publish Documentation diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 35bbf483209d..3f43d31f29d9 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -12,6 +12,8 @@ Proof harnesses are similar to test harnesses, especially property-based test ha Kani is currently under active development. Releases are published [here](/~https://github.com/model-checking/kani/releases). +Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc). + There is support for a fair amount of Rust language features, but not all (e.g., concurrency). Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features. diff --git a/rfc/book.toml b/rfc/book.toml new file mode 100644 index 000000000000..ef6adebf4847 --- /dev/null +++ b/rfc/book.toml @@ -0,0 +1,17 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[book] +title = "Kani RFC Book" +description = "Design documents for Kani Rust Verifier" +authors = ["Kani Developers"] +language = "en" +multilingual = false +src = "src" + +[output.html] +site-url = "/kani/rfc/" +git-repository-url = "/~https://github.com/model-checking/kani" +edit-url-template = "/~https://github.com/model-checking/kani/edit/main/rfc/{path}" + +[output.html.playground] +runnable = false diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md new file mode 100644 index 000000000000..2a6e6e4757c9 --- /dev/null +++ b/rfc/src/SUMMARY.md @@ -0,0 +1,9 @@ +# Kani Rust Verifier - RFCs + +[Introduction](./intro.md) + +[RFC Template](./template.md) + +# Kani RFCs + + diff --git a/rfc/src/intro.md b/rfc/src/intro.md new file mode 100644 index 000000000000..9187f5b6fc93 --- /dev/null +++ b/rfc/src/intro.md @@ -0,0 +1,64 @@ +# Introduction + +Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. In order to +integrate feedback from developers and users on future changes to Kani, we decided to follow a light-weight +"RFC" (request for comments) process. + +## When to create an RFC + +You should create an RFC in one of two cases: + +1. The change you are proposing would be a "one way door": e.g. a change to the public API, a new feature that would be difficult to modify once released, deprecating a feature, etc. +2. The change you are making has a significant design component, and would benefit from a design review. + +Bugs and smaller improvements to existing features do not require an RFC. +If you are in doubt, feel free to create a [feature request](/~https://github.com/model-checking/kani/issues/new?assignees=&labels=&template=feature_request.md) and discuss the next steps in the new issue. +Your PR reviewer may also request an RFC if your change appears to fall into category 1 or 2. + +You do not necessarily need to create an RFC immediately. It is our experience that it is often best to write some "proof of concept" code to test out possible ideas before writing the formal RFC. + +## The RFC process + +This is the overall workflow for the RFC process: + +```toml + Create RFC ──> Receive Feedback ──> Accepted? + │ ∧ │ Y + ∨ │ ├───> Implement ───> Test + Feedback ───> Stabilize? + Revise │ N │ Y + └───> Close PR ├───> RFC Stable + │ N + └───> Remove feature +``` + +1. Create an RFC + 1. Create a tracking issue for your RFC (e.g.: [Issue-1588](/~https://github.com/model-checking/kani/issues/1588)). + 2. Start from a fork of the Kani repository. + 3. Copy the template file ([`rfc/src/template.md`](./template.md)) to `rfc/src/.md`. + 4. Fill in the details according to the template instructions. + 5. Submit a pull request. +2. Build consensus and integrate feedback. + 1. RFCs should get approved by at least 2 Kani developers. + 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. +3. Feature implementation. + 1. Start implementing the new feature in your fork. + 2. It is OK to implement it incrementally over multiple PRs. Just ensure that every pull request has a testable + end-to-end flow and that it is properly tested. + 3. In the implementation stage, the feature should only be accessible if the user explicitly passes + `--enable-unstable` as an argument to Kani. + 4. Document how to use the feature. + 5. Keep the RFC up-to-date with the decisions you make during implementation. +4. Test and Gather Feedback. + 1. Fix major issues related to the new feature. + 2. Gather user feedback and make necessary adjustments. + 3. Add lots of tests. +5. Stabilization. + 1. Propose to stabilize the feature when feature is well tested and UX has received positive feedback. + 2. Create a new PR that removes the `--enable-unstable` guard and that marks the RFC status as "STABLE". + 1. Make sure the RFC reflects the final implementation and user experience. + 3. In some cases, we might decide not to incorporate a feature + (E.g.: performance degradation, bad user experience, better alternative). + In those cases, please update the RFC status to "CANCELLED as per " and remove the code + that is no longer relevant. + 4. Close the tracking issue. \ No newline at end of file diff --git a/rfc/src/template.md b/rfc/src/template.md new file mode 100644 index 000000000000..1ace8208d46e --- /dev/null +++ b/rfc/src/template.md @@ -0,0 +1,54 @@ +- **Feature Name:** *Fill me with pretty name and a unique ident. E.g: New Feature (`new_feature`)* +- **Feature Request Issue:** *Link to issue* +- **RFC PR:** *Link to original PR* +- **Status:** *One of the following: [Under Review | Unstable | Stable | Cancelled]* +- **Version:** [0-9]\* *Increment this version whenever you open a new PR to update the RFC (not at every revision). + Start with 0.* +- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here* + +## Summary + +Short description of the feature, i.e.: the elevator pitch. What is this feature about? + +## User Impact + +Why are we doing this? How will this benefit the final user? + + - If this is an API change, how will that impact current users? + - For deprecation or breaking changes, how will the transition look like? + - If this RFC is related to change in the architecture without major user impact, think about the long term +impact for user. I.e.: what future work will this enable. + +## User Experience + +What is the scope of this RFC? Which use cases do you have in mind? Explain how users will interact with it. Also +please include: + +- How would you teach this feature to users? What changes will be required to the user documentation? +- If the RFC is related to architectural changes and there are no visible changes to UX, please state so. + +## Detailed Design + +This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind: + +- What are the main components that will be modified? (E.g.: changes to `kani-compiler`, `kani-driver`, metadata, + installation...) +- How will they be modified? Any changes to how these components communicate? +- Will this require any new dependency? +- What corner cases do you anticipate? + +## Rationale and alternatives + +- What are the pros and cons of this design? +- What is the impact of not doing this? +- What other designs have you considered? Why didn't you choose them? + +## Open questions + +- Is there any part of the design that you expect to resolve through the RFC process? +- What kind of user feedback do you expect to gather before stabilization? How will this impact your design? + +## Future possibilities + +What are natural extensions and possible improvements that you predict for this feature that is out of the +scope of this RFC? Feel free to brainstorm here. \ No newline at end of file diff --git a/docs/build-docs.sh b/scripts/build-docs.sh similarity index 81% rename from docs/build-docs.sh rename to scripts/build-docs.sh index 8a9a0f552b59..dea0636a2fa9 100755 --- a/docs/build-docs.sh +++ b/scripts/build-docs.sh @@ -2,6 +2,10 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT +# Build all our documentation and place them under book/ directory. +# The user facing doc is built into book/ +# RFCs are placed under book/rfc/ + set -eu SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" @@ -20,8 +24,12 @@ fi # Publish bookrunner report into our documentation KANI_DIR=$SCRIPT_DIR/.. +DOCS_DIR=$KANI_DIR/docs +RFC_DIR=$KANI_DIR/rfc HTML_DIR=$KANI_DIR/build/output/latest/html/ +cd $DOCS_DIR + if [ -d $HTML_DIR ]; then # Litani run is copied into `src` to avoid deletion by `mdbook` cp -r $HTML_DIR src/bookrunner/ @@ -38,11 +46,17 @@ else echo "WARNING: Could not find the latest bookrunner run." fi +echo "Building user documentation..." # Build the book into ./book/ mkdir -p book -./mdbook build +mkdir -p book/rfc +$SCRIPT_DIR/mdbook build touch book/.nojekyll +echo "Building RFC book..." +cd $RFC_DIR +$SCRIPT_DIR/mdbook build -d $KANI_DIR/docs/book/rfc + # Testing of the code in the documentation is done via the usual # ./scripts/kani-regression.sh script. A note on running just the # doc tests is in README.md. We don't run them here because