forked from tokio-rs/prost
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Allow file descriptor be generated without --include_source_info (tokio-rs#786) * Allow file descriptor be generated without --include_source_info The file descriptor sets generated by rules_proto in bazel don't have this by default, so this allows some flexibility for users to reuse results that are already available to them. It's fairly trivial adjustment so it seemed reasonable to me to allow the flexibility. * revert breaking changes and add default * release 0.11.5 (tokio-rs#788) * Add message and enum attributes to prost-build (tokio-rs#784) closes tokio-rs#783 * chore: Prepare 0.11.6 release (tokio-rs#794) * chore: Added Kani to CI. (#1) (tokio-rs#798) * Added Kani documentation. (tokio-rs#799) * Fix issue with negative nanos in Duration::try_from(), and add tests (tokio-rs#803) * Fix issue with negative nanos in Duration::try_from(), and add a unit test * add proptest for negative nanos * PR comment: remove spurious dbg * Prevent spurious overflow in check_duration_roundtrip test (tokio-rs#804) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * Clarify `default_package_filename` documentation. (tokio-rs#809) * Bump msrv to 1.60 (tokio-rs#814) * chore(types): Remove including generated code (tokio-rs#801) * chore: Update github action (tokio-rs#815) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * chore: Add cargo-machete to detect unused dependencies (tokio-rs#817) * chore: Update msrv to 1.60 (tokio-rs#818) * feat: Added try_normalize to Timestamp (tokio-rs#796) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * Update PropProof docs to note the need to submodule init (tokio-rs#805) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * feat(build): Add direct fds compile support (tokio-rs#819) This commit adds two new compile functions that allow passing a `FileDescriptorSet` and it will generate the Rust code. This allows users to use libraries like `protox` directly and in an ergonomic way. * release 0.11.7 (tokio-rs#821) * fix: correct change in visibility of compiler module (tokio-rs#824) Introduced in tokio-rs#801 Closes tokio-rs#823 * release 0.11.8 (tokio-rs#825) * Add existing roundtrip test to Kani CI and avoid recursive submoduling (tokio-rs#828) * Add existing roundtrip test to Kani CI * Bump up Kani version * Remove `v` from GA version * Update to `syn@2` & `prettyplease@0.2` (tokio-rs#833) * Fix corrupted tests and missing CI testing (tokio-rs#832) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * chore: Update to criterion 0.4 (tokio-rs#835) * Fix build in directory not named `prost` (tokio-rs#839) This library will fail to build with the following error when checked out into a directory not named exactly `prost`: error: failed to load manifest for workspace member `/home/alex/src/prost-rs/tests/single-include` Caused by: failed to load manifest for dependency `prost` Caused by: failed to read `/home/alex/src/prost/Cargo.toml` Caused by: No such file or directory (os error 2) This is because the `single-include` test depends on `prost` with the path `../../../prost`. This patch fixes the issue by correcting the path to `../..`. * prost-build: support boxing fields (tokio-rs#802) This allows the user to request boxing of specific fields. This is useful for enum types that might have variants of very different size. * chore: Update to baptiste0928/cargo-install@v2 (tokio-rs#840) Co-authored-by: Lucio Franco <luciofranco14@gmail.com> * Fix typo in bail message (tokio-rs#848) --------- Co-authored-by: David Freese <freese@google.com> Co-authored-by: Lucio Franco <luciofranco14@gmail.com> Co-authored-by: damel_lp <dlambertpowell@gmail.com> Co-authored-by: Yoshiki Takashima <ytakashi@andrew.cmu.edu> Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com> Co-authored-by: Gilad Naaman <gilad@naaman.io> Co-authored-by: tottoto <tottotodev@gmail.com> Co-authored-by: Oliver Browne <109075559+oliverbrowneprima@users.noreply.github.com> Co-authored-by: Marcus Griep <marcus@griep.us> Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Co-authored-by: Donough Liu <liudingming@bytedance.com> Co-authored-by: Alex O'Brien <3541@3541.website> Co-authored-by: Thomas Orozco <thomas@orozco.fr> Co-authored-by: Brendon Daugherty <brendon1097@gmail.com>
- Loading branch information
1 parent
47bf91e
commit b41ff14
Showing
23 changed files
with
800 additions
and
171 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
# Kani | ||
This document describes how to **locally** install and use Kani, along | ||
with its experimental PropProof feature. Because of instability in | ||
Kani internals, the GitHub action is the recommended option if you are | ||
running in CI. | ||
|
||
Kani is a software verification tool that complements testing by | ||
proving the absence of certain classes of bugs like unwrap exceptions, | ||
overflows, and assertion failures. See the [Kani | ||
book](https://model-checking.github.io/kani/) for a full list of | ||
capabilities and limitations. | ||
|
||
## Installing Kani and PropProof | ||
- The install instructions for Kani can be [found | ||
here](https://model-checking.github.io/kani/install-guide.html). Once | ||
Kani is installed, you can run with `cargo kani` for projects or | ||
`kani` for individual Rust files. | ||
- **[UNSTABLE]** To use PropProof, first download the source code | ||
from the Kani repository. | ||
```bash | ||
git clone https://github.com/model-checking/kani.git --branch features/proptest propproof | ||
cd propproof; git submodule update --init | ||
``` | ||
|
||
Then, use `.cargo/config.toml` enable it in the local directory you | ||
want to run Kani in. This will override the `proptest` import in | ||
your repo. | ||
|
||
```bash | ||
cd $YOUR_REPO_LOCAL_PATH | ||
mkdir '.cargo' | ||
echo "paths =[\"$PATH_TO_PROPPROOF\"]" > .cargo/config.toml | ||
``` | ||
|
||
**Please Note**: | ||
- `features/proptest` branch under Kani is likely not the final | ||
location for this code. If these instructions stop working, please | ||
consult the Kani documentation and file an issue on [the Kani | ||
repo](https://github.com/model-checking/kani.git). | ||
- The cargo config file will force cargo to always use PropProof. To | ||
use `proptest`, delete the file. | ||
|
||
## Running Kani | ||
After installing Kani and PropProof, `cargo kani --tests` should | ||
automatically run `proptest!` harnesses inside your crate. Use | ||
`--harness` to run a specific harness, and `-p` for a specific | ||
sub-crate. | ||
|
||
If Kani returns with an error, you can use the concrete playback | ||
feature using `--enable-unstable --concrete-playback print` and paste | ||
in the code to your repository. Running this harness with `cargo test` | ||
will replay the input found by Kani that produced this crash. Please | ||
note that this feature is unstable and using `--concrete-playback | ||
inplace` to automatically inject a replay harness is not supported | ||
when using PropProof. | ||
|
||
## Debugging CI Failure | ||
```yaml | ||
- name: Verify with Kani | ||
uses: model-checking/kani-github-action@v0.xx | ||
with: | ||
enable-propproof: true | ||
args: | | ||
$KANI_ARGUMENTS | ||
``` | ||
The above GitHub CI workflow is equivalent to `cargo kani | ||
$KANI_ARGUMENTS` with PropProof installed. To replicate issues | ||
locally, run `cargo kani` with the same arguments. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.