From 91ac31cff17d70f7fc36023957cd7806a4b277fd Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 4 Oct 2024 14:05:31 -0400 Subject: [PATCH 1/6] Fix link for tool application Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index db5018121be02..a7de40fb768fe 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -4,7 +4,7 @@ - [General Rules](./general-rules.md) - [Challenge Template](./template.md) - - [Tool application](./todo.md) + - [Tool application](./general-rules.md#tool-applications) - [Verification Tools](./tools.md) - [Kani](./tools/kani.md) From b5530f05541f07516c681f165a7d3d1eb5e427af Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 4 Oct 2024 14:09:59 -0400 Subject: [PATCH 2/6] Fix link for tool application template Signed-off-by: Felipe R. Monteiro --- doc/src/general-rules.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index c681e9bb8953d..aac71d80d5fad 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -69,7 +69,7 @@ Follow the following steps to create a new proposal: Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools): -* Any new tool that participants want to enable will require an application using the Issue template [Tool application](todo.md). +* Any new tool that participants want to enable will require an application using the issue template for [tool applications](https://github.com/model-checking/verify-rust-std/blob/main/.github/TOOL_REQUEST_TEMPLATE.md). * The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS * A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed. From 48558fc30ff97cb21b6de4b09ce77ba044b721b4 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 5 Oct 2024 17:33:02 -0400 Subject: [PATCH 3/6] Fix links for tool application in general rules Signed-off-by: Felipe R. Monteiro --- doc/src/general-rules.md | 2 +- library/Cargo.lock | 86 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 87 insertions(+), 1 deletion(-) diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index aac71d80d5fad..04c1e42ce03c0 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -39,7 +39,7 @@ A proposed solution to a verification problem will only **be reviewed** if all t * The contribution must be automated and should be checked and pass as part of the PR checks. * All tools used by the solution must be in [the list of accepted tools](tools.md#approved-tools), and previously integrated in the repository. - If that is not the case, please submit a separate [tool application first](todo.md). + If that is not the case, please submit a separate [tool application first](./general-rules.md#tool-applications). * There is no restriction on the number of contributors for a solution. Make sure you have the rights to submit your solution and that all contributors are properly mentioned. * The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated diff --git a/library/Cargo.lock b/library/Cargo.lock index 54ad052c52322..695e3c4bcb306 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,6 +72,7 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", + "safety", ] [[package]] @@ -219,6 +220,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -236,6 +270,15 @@ dependencies = [ "core", ] +[[package]] +name = "quote" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "4.5.0" @@ -312,6 +355,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.79", +] + [[package]] name = "std" version = "0.0.0" @@ -353,6 +406,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -372,6 +446,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" + [[package]] name = "unicode-width" version = "0.1.13" @@ -405,6 +485,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" From 4ea2850048bfbe13e084293fa4d34e474f95f31b Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 5 Oct 2024 17:34:05 -0400 Subject: [PATCH 4/6] Update gitignore Signed-off-by: Felipe R. Monteiro --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 367d4db4df2f7..41f6d2a5e3c36 100644 --- a/.gitignore +++ b/.gitignore @@ -20,6 +20,7 @@ Session.vim /book/ /build/ /target +library/target *.rlib *.rmeta *.mir From 3ae4df2b90c69fcc8a23397738dc9f37618d704b Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 5 Oct 2024 18:09:54 -0400 Subject: [PATCH 5/6] Move tool application template to our book Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 4 ++-- doc/src/{template.md => challenge_template.md} | 0 doc/src/general-rules.md | 4 ++-- doc/src/todo.md | 3 --- .github/TOOL_REQUEST_TEMPLATE.md => doc/src/tool_template.md | 0 5 files changed, 4 insertions(+), 7 deletions(-) rename doc/src/{template.md => challenge_template.md} (100%) delete mode 100644 doc/src/todo.md rename .github/TOOL_REQUEST_TEMPLATE.md => doc/src/tool_template.md (100%) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index a7de40fb768fe..9d445fc7dc10c 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -3,8 +3,8 @@ [Introduction](intro.md) - [General Rules](./general-rules.md) - - [Challenge Template](./template.md) - - [Tool application](./general-rules.md#tool-applications) + - [Challenge Template](./challenge_template.md) + - [Tool Application Template](./tool_template.md) - [Verification Tools](./tools.md) - [Kani](./tools/kani.md) diff --git a/doc/src/template.md b/doc/src/challenge_template.md similarity index 100% rename from doc/src/template.md rename to doc/src/challenge_template.md diff --git a/doc/src/general-rules.md b/doc/src/general-rules.md index 04c1e42ce03c0..4f419decbdf6b 100644 --- a/doc/src/general-rules.md +++ b/doc/src/general-rules.md @@ -56,7 +56,7 @@ The type of obstacles users face may depend on which part of the standard librar Everyone is welcome to submit new challenge proposals for review by our committee. Follow the following steps to create a new proposal: -1. Create a tracking issue using the Issue template [Challenge Proposal](template.md) for your challenge. +1. Create a tracking issue using the [challenge template](./challenge_template.md) for your challenge. 2. In your fork of this repository do the following: 1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/-.md`. 2. Fill in the details according to the template instructions. @@ -69,7 +69,7 @@ Follow the following steps to create a new proposal: Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools): -* Any new tool that participants want to enable will require an application using the issue template for [tool applications](https://github.com/model-checking/verify-rust-std/blob/main/.github/TOOL_REQUEST_TEMPLATE.md). +* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md). * The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS * A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed. diff --git a/doc/src/todo.md b/doc/src/todo.md deleted file mode 100644 index 50fed3f03274b..0000000000000 --- a/doc/src/todo.md +++ /dev/null @@ -1,3 +0,0 @@ -# 🚧 Under Construction 🚧 - -This section is still under construction. Please check it back again soon and we’ll have more details for you. \ No newline at end of file diff --git a/.github/TOOL_REQUEST_TEMPLATE.md b/doc/src/tool_template.md similarity index 100% rename from .github/TOOL_REQUEST_TEMPLATE.md rename to doc/src/tool_template.md From 743a5d7b169c3068cd02073408008362576ec414 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 5 Oct 2024 18:12:19 -0400 Subject: [PATCH 6/6] Revert changes on Cargo.lock Signed-off-by: Felipe R. Monteiro --- library/Cargo.lock | 86 ---------------------------------------------- 1 file changed, 86 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 695e3c4bcb306..54ad052c52322 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,7 +72,6 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", - "safety", ] [[package]] @@ -220,39 +219,6 @@ dependencies = [ "unwind", ] -[[package]] -name = "proc-macro-error" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" -dependencies = [ - "proc-macro-error-attr", - "proc-macro2", - "quote", - "syn 1.0.109", - "version_check", -] - -[[package]] -name = "proc-macro-error-attr" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" -dependencies = [ - "proc-macro2", - "quote", - "version_check", -] - -[[package]] -name = "proc-macro2" -version = "1.0.86" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" -dependencies = [ - "unicode-ident", -] - [[package]] name = "proc_macro" version = "0.0.0" @@ -270,15 +236,6 @@ dependencies = [ "core", ] -[[package]] -name = "quote" -version = "1.0.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" -dependencies = [ - "proc-macro2", -] - [[package]] name = "r-efi" version = "4.5.0" @@ -355,16 +312,6 @@ dependencies = [ "std", ] -[[package]] -name = "safety" -version = "0.1.0" -dependencies = [ - "proc-macro-error", - "proc-macro2", - "quote", - "syn 2.0.79", -] - [[package]] name = "std" version = "0.0.0" @@ -406,27 +353,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.79" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - [[package]] name = "sysroot" version = "0.0.0" @@ -446,12 +372,6 @@ dependencies = [ "std", ] -[[package]] -name = "unicode-ident" -version = "1.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" - [[package]] name = "unicode-width" version = "0.1.13" @@ -485,12 +405,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1"