From b791416df51f602076aaf5ee493f2e2789089f46 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Aug 2022 14:59:23 -0700 Subject: [PATCH 1/9] Move build docs script to be under scripts/ --- {docs => scripts}/build-docs.sh | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) rename {docs => scripts}/build-docs.sh (86%) diff --git a/docs/build-docs.sh b/scripts/build-docs.sh similarity index 86% rename from docs/build-docs.sh rename to scripts/build-docs.sh index 8a9a0f552b59..8b7952cc2c5a 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/ +# Our RFCs is placed under book/rfcs/ + set -eu SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )" @@ -20,8 +24,11 @@ fi # Publish bookrunner report into our documentation KANI_DIR=$SCRIPT_DIR/.. +DOCS_DIR=$KANI_DIR/docs HTML_DIR=$KANI_DIR/build/output/latest/html/ +pushd $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,9 +45,10 @@ else echo "WARNING: Could not find the latest bookrunner run." fi +echo "Building use documentation..." # Build the book into ./book/ mkdir -p book -./mdbook build +${SCRIPT_DIR}/mdbook build touch book/.nojekyll # Testing of the code in the documentation is done via the usual @@ -48,4 +56,6 @@ touch book/.nojekyll # doc tests is in README.md. We don't run them here because # that would cause CI to run these tests twice. +echo "Building rfcs..." + echo "Finished documentation build successfully." From 3a2e68c0ef7bf1564982971e331c1a6c6c7e9ac9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Aug 2022 16:56:31 -0700 Subject: [PATCH 2/9] Add RFC book and an RFC template This PR itself is our first RFC. :) --- rfcs/book.toml | 17 +++++++++++++ rfcs/src/SUMMARY.md | 8 ++++++ rfcs/src/intro.md | 53 ++++++++++++++++++++++++++++++++++++++++ rfcs/src/template.md | 58 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 136 insertions(+) create mode 100644 rfcs/book.toml create mode 100644 rfcs/src/SUMMARY.md create mode 100644 rfcs/src/intro.md create mode 100644 rfcs/src/template.md diff --git a/rfcs/book.toml b/rfcs/book.toml new file mode 100644 index 000000000000..979d70b6401e --- /dev/null +++ b/rfcs/book.toml @@ -0,0 +1,17 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[book] +title = "Kani RFCs" +description = "Design documents for Kani Rust Verifier" +authors = ["Kani Developers"] +language = "en" +multilingual = false +src = "src" + +[output.html] +site-url = "/kani-rfcs/" +git-repository-url = "https://github.com/model-checking/kani" +edit-url-template = "https://github.com/model-checking/kani/edit/main/rfcs/{path}" + +[output.html.playground] +runnable = false diff --git a/rfcs/src/SUMMARY.md b/rfcs/src/SUMMARY.md new file mode 100644 index 000000000000..5768fe278da9 --- /dev/null +++ b/rfcs/src/SUMMARY.md @@ -0,0 +1,8 @@ +# Kani Rust Verifier - RFCs + +- [Introduction](./intro.md) +- [Template](./template.md) + +# Active RFCs + + diff --git a/rfcs/src/intro.md b/rfcs/src/intro.md new file mode 100644 index 000000000000..44bdb524e587 --- /dev/null +++ b/rfcs/src/intro.md @@ -0,0 +1,53 @@ +# Introduction + +Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. In order to +integate 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 + +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 deprecation, should follow an RFC process. We also ask for substantial architectural +changes to be made via RFC. + +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. + +## The RFC process + +This is the overall workflow for the RFC process: + +```toml + Create RFC ──> Receive Feedback ──> Accepted? + │ Y + ├───> Implement ───> Stabilize? + │ N │ Y + └───> Close PR ├───> RFC Stable + │ N + └───> Remove feature +``` + +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/.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. + 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. +4. Stabilization. + 1. After the feature has been implemented, start the stabilization process. + 2. Gather user feedback and make necessary adjustments. + 3. Create a new PR that removes the `--enable-unstable` guard and that marks the RFC status as "STABLE". Also + make sure the RFC reflects the final implementation and user experience. + 5. In some cases, we might decide not to stabilize a feature. In those cases, please update the RFC status to + "CANCELLED" and remove the code that is no longer relevant. \ No newline at end of file diff --git a/rfcs/src/template.md b/rfcs/src/template.md new file mode 100644 index 000000000000..f736a423c14b --- /dev/null +++ b/rfcs/src/template.md @@ -0,0 +1,58 @@ +- 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]* + +# Summary +[summary]: #summary + +Short description of the feature, i.e.: the elevator pitch. What is this feature about? + +# User Impact +[user-impact]: #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 +[user-experience]: #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 +[detailed-design]: #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 are the corner cases you antecipate? + +# Rationale and alternatives +[rationale-and-alternatives]: #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? + +# Unresolved questions +[unresolved-questions]: #unresolved-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 +[future-possibilities]: #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 From 8959d4901b769f1eb2e4ce55db7b00035a845507 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Aug 2022 17:19:53 -0700 Subject: [PATCH 3/9] Build rfc book as part of build docs --- rfcs/book.toml | 2 +- rfcs/src/SUMMARY.md | 7 ++++--- scripts/build-docs.sh | 12 ++++++++---- 3 files changed, 13 insertions(+), 8 deletions(-) diff --git a/rfcs/book.toml b/rfcs/book.toml index 979d70b6401e..f6c59601311b 100644 --- a/rfcs/book.toml +++ b/rfcs/book.toml @@ -9,7 +9,7 @@ multilingual = false src = "src" [output.html] -site-url = "/kani-rfcs/" +site-url = "/kani/rfcs/" git-repository-url = "https://github.com/model-checking/kani" edit-url-template = "https://github.com/model-checking/kani/edit/main/rfcs/{path}" diff --git a/rfcs/src/SUMMARY.md b/rfcs/src/SUMMARY.md index 5768fe278da9..2a6e6e4757c9 100644 --- a/rfcs/src/SUMMARY.md +++ b/rfcs/src/SUMMARY.md @@ -1,8 +1,9 @@ # Kani Rust Verifier - RFCs -- [Introduction](./intro.md) -- [Template](./template.md) +[Introduction](./intro.md) -# Active RFCs +[RFC Template](./template.md) + +# Kani RFCs diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh index 8b7952cc2c5a..8c26f9ec302f 100755 --- a/scripts/build-docs.sh +++ b/scripts/build-docs.sh @@ -25,9 +25,10 @@ fi # Publish bookrunner report into our documentation KANI_DIR=$SCRIPT_DIR/.. DOCS_DIR=$KANI_DIR/docs +RFCS_DIR=$KANI_DIR/rfcs HTML_DIR=$KANI_DIR/build/output/latest/html/ -pushd $DOCS_DIR +cd $DOCS_DIR if [ -d $HTML_DIR ]; then # Litani run is copied into `src` to avoid deletion by `mdbook` @@ -48,14 +49,17 @@ fi echo "Building use documentation..." # Build the book into ./book/ mkdir -p book -${SCRIPT_DIR}/mdbook build +mkdir -p book/rfcs +$SCRIPT_DIR/mdbook build touch book/.nojekyll +echo "Building RFCs book..." +cd $RFCS_DIR +$SCRIPT_DIR/mdbook build -d $KANI_DIR/docs/book/rfcs + # 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 # that would cause CI to run these tests twice. -echo "Building rfcs..." - echo "Finished documentation build successfully." From ba29b0787444fba07a4698bec8d1ddafbe673858 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Aug 2022 22:00:05 -0700 Subject: [PATCH 4/9] Update kani.yml --- .github/workflows/kani.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 1356813519aa..a72b7a3a8ac5 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -79,7 +79,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 From 57f192a56c5fdeddf89b84a04e5d9c9f85df9af6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Aug 2022 09:56:30 -0700 Subject: [PATCH 5/9] Apply suggestions from code review Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- rfcs/src/intro.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rfcs/src/intro.md b/rfcs/src/intro.md index 44bdb524e587..82664942831b 100644 --- a/rfcs/src/intro.md +++ b/rfcs/src/intro.md @@ -1,13 +1,13 @@ # Introduction Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. In order to -integate feedback from developers and users on future changes to Kani, we decided to follow a light-weight +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 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 deprecation, should follow an RFC process. We also ask for substantial architectural +APIs, new features, as well as depreciation, should follow an RFC process. We also ask for substantial architectural changes to be made via RFC. Bugs and smaller improvements to existing features do not require an RFC. If you are in doubt, feel free to create From fc6473c3787df779427fc5bf3faebbe807418019 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Aug 2022 10:45:43 -0700 Subject: [PATCH 6/9] Apply suggestions from code review Co-authored-by: Daniel Schwartz-Narbonne --- rfcs/src/intro.md | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/rfcs/src/intro.md b/rfcs/src/intro.md index 82664942831b..1e1424d3f3bf 100644 --- a/rfcs/src/intro.md +++ b/rfcs/src/intro.md @@ -6,13 +6,16 @@ integrate feedback from developers and users on future changes to Kani, we decid ## 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 -changes to be made via RFC. +You should create an RFC in one of two cases: -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. +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 From ee02f51453b68e07e193c1f0ec054bedeb25331a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Aug 2022 11:19:25 -0700 Subject: [PATCH 7/9] Apply suggestions from code review Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- rfcs/src/template.md | 2 +- scripts/build-docs.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/rfcs/src/template.md b/rfcs/src/template.md index f736a423c14b..2b27443f5d60 100644 --- a/rfcs/src/template.md +++ b/rfcs/src/template.md @@ -36,7 +36,7 @@ This is the technical portion of the RFC. Please provide high level details of t installation...) - How will they be modified? Any changes to how these components communicate? - Will this require any new dependency? -- What are the corner cases you antecipate? +- What corner cases do you anticipate? # Rationale and alternatives [rationale-and-alternatives]: #rationale-and-alternatives diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh index 8c26f9ec302f..41b440569cd6 100755 --- a/scripts/build-docs.sh +++ b/scripts/build-docs.sh @@ -4,7 +4,7 @@ # Build all our documentation and place them under book/ directory. # The user facing doc is built into book/ -# Our RFCs is placed under book/rfcs/ +# RFCs are placed under book/rfcs/ set -eu From 766fc6d0b122a6e79d3daeb732c9bc80252166f2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Aug 2022 14:43:33 -0700 Subject: [PATCH 8/9] Address feedback --- .github/PULL_REQUEST_TEMPLATE.md | 6 ++++ rfcs/src/intro.md | 52 ++++++++++++++++++-------------- rfcs/src/template.md | 19 +++++------- 3 files changed, 44 insertions(+), 33 deletions(-) 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/rfcs/src/intro.md b/rfcs/src/intro.md index 1e1424d3f3bf..cfe0fbd6a06a 100644 --- a/rfcs/src/intro.md +++ b/rfcs/src/intro.md @@ -1,7 +1,7 @@ # 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 +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 @@ -15,7 +15,7 @@ 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.``` +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 @@ -23,34 +23,42 @@ This is the overall workflow for the RFC process: ```toml Create RFC ──> Receive Feedback ──> Accepted? - │ Y - ├───> Implement ───> Stabilize? - │ N │ Y - └───> Close PR ├───> RFC Stable - │ N - └───> Remove feature + │ ∧ │ Y + ∨ │ ├───> Implement ───> Test + Feedback ───> Stabilize? + Revise │ N │ Y + └───> Close PR ├───> RFC Stable + │ N + └───> Remove feature ``` 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/.md`. - 3. Fill in the details according to the template intructions. - 4. Submit a pull request. + 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 ([`rfcs/src/template.md`](./template.md)) to `rfcs/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 members of the `kani-developers` team. + 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 + 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 + 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. -4. Stabilization. - 1. After the feature has been implemented, start the stabilization process. + 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. Create a new PR that removes the `--enable-unstable` guard and that marks the RFC status as "STABLE". Also - make sure the RFC reflects the final implementation and user experience. - 5. In some cases, we might decide not to stabilize a feature. In those cases, please update the RFC status to - "CANCELLED" and remove the code that is no longer relevant. \ No newline at end of file + 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/rfcs/src/template.md b/rfcs/src/template.md index 2b27443f5d60..9f408c183997 100644 --- a/rfcs/src/template.md +++ b/rfcs/src/template.md @@ -2,51 +2,48 @@ - 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 -[summary]: #summary Short description of the feature, i.e.: the elevator pitch. What is this feature about? # User Impact -[user-impact]: #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 + - 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 -[user-experience]: #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 +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 -[detailed-design]: #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, +- 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 -[rationale-and-alternatives]: #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? -# Unresolved questions -[unresolved-questions]: #unresolved-questions +# 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? @@ -54,5 +51,5 @@ This is the technical portion of the RFC. Please provide high level details of t # Future possibilities [future-possibilities]: #future-possibilities -What are natural extensions and possible improvements that you predict for this feature that is out of the +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 From cb9b5ab33ca769bd113cf9e33464f5c1b4a72183 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Aug 2022 13:10:05 -0700 Subject: [PATCH 9/9] Small adjustments: 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. --- docs/src/getting-started.md | 2 ++ {rfcs => rfc}/book.toml | 6 +++--- {rfcs => rfc}/src/SUMMARY.md | 0 {rfcs => rfc}/src/intro.md | 2 +- {rfcs => rfc}/src/template.md | 29 ++++++++++++++--------------- scripts/build-docs.sh | 14 +++++++------- 6 files changed, 27 insertions(+), 26 deletions(-) rename {rfcs => rfc}/book.toml (85%) rename {rfcs => rfc}/src/SUMMARY.md (100%) rename {rfcs => rfc}/src/intro.md (97%) rename {rfcs => rfc}/src/template.md (72%) 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/rfcs/book.toml b/rfc/book.toml similarity index 85% rename from rfcs/book.toml rename to rfc/book.toml index f6c59601311b..ef6adebf4847 100644 --- a/rfcs/book.toml +++ b/rfc/book.toml @@ -1,7 +1,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT [book] -title = "Kani RFCs" +title = "Kani RFC Book" description = "Design documents for Kani Rust Verifier" authors = ["Kani Developers"] language = "en" @@ -9,9 +9,9 @@ multilingual = false src = "src" [output.html] -site-url = "/kani/rfcs/" +site-url = "/kani/rfc/" git-repository-url = "https://github.com/model-checking/kani" -edit-url-template = "https://github.com/model-checking/kani/edit/main/rfcs/{path}" +edit-url-template = "https://github.com/model-checking/kani/edit/main/rfc/{path}" [output.html.playground] runnable = false diff --git a/rfcs/src/SUMMARY.md b/rfc/src/SUMMARY.md similarity index 100% rename from rfcs/src/SUMMARY.md rename to rfc/src/SUMMARY.md diff --git a/rfcs/src/intro.md b/rfc/src/intro.md similarity index 97% rename from rfcs/src/intro.md rename to rfc/src/intro.md index cfe0fbd6a06a..9187f5b6fc93 100644 --- a/rfcs/src/intro.md +++ b/rfc/src/intro.md @@ -34,7 +34,7 @@ This is the overall workflow for the RFC process: 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 ([`rfcs/src/template.md`](./template.md)) to `rfcs/src/.md`. + 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. diff --git a/rfcs/src/template.md b/rfc/src/template.md similarity index 72% rename from rfcs/src/template.md rename to rfc/src/template.md index 9f408c183997..1ace8208d46e 100644 --- a/rfcs/src/template.md +++ b/rfc/src/template.md @@ -1,16 +1,16 @@ -- 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* +- **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 +## Summary Short description of the feature, i.e.: the elevator pitch. What is this feature about? -# User Impact +## User Impact Why are we doing this? How will this benefit the final user? @@ -19,7 +19,7 @@ Why are we doing this? How will this benefit the final user? - 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 +## 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: @@ -27,7 +27,7 @@ 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 +## Detailed Design This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind: @@ -37,19 +37,18 @@ This is the technical portion of the RFC. Please provide high level details of t - Will this require any new dependency? - What corner cases do you anticipate? -# Rationale and alternatives +## 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 +## 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 -[future-possibilities]: #future-possibilities +## 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/scripts/build-docs.sh b/scripts/build-docs.sh index 41b440569cd6..dea0636a2fa9 100755 --- a/scripts/build-docs.sh +++ b/scripts/build-docs.sh @@ -4,7 +4,7 @@ # Build all our documentation and place them under book/ directory. # The user facing doc is built into book/ -# RFCs are placed under book/rfcs/ +# RFCs are placed under book/rfc/ set -eu @@ -25,7 +25,7 @@ fi # Publish bookrunner report into our documentation KANI_DIR=$SCRIPT_DIR/.. DOCS_DIR=$KANI_DIR/docs -RFCS_DIR=$KANI_DIR/rfcs +RFC_DIR=$KANI_DIR/rfc HTML_DIR=$KANI_DIR/build/output/latest/html/ cd $DOCS_DIR @@ -46,16 +46,16 @@ else echo "WARNING: Could not find the latest bookrunner run." fi -echo "Building use documentation..." +echo "Building user documentation..." # Build the book into ./book/ mkdir -p book -mkdir -p book/rfcs +mkdir -p book/rfc $SCRIPT_DIR/mdbook build touch book/.nojekyll -echo "Building RFCs book..." -cd $RFCS_DIR -$SCRIPT_DIR/mdbook build -d $KANI_DIR/docs/book/rfcs +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