Comments (11)
That appears to work for us, thanks!
from kani.
Actually it seems that, even without any cargo update, suddenly various build actions fail: https://github.com/model-checking/kani/actions/runs/8692459550. No idea what changed here.
from kani.
We ran into this too: https://github.com/google/zerocopy/actions/runs/8695299265/job/23846059719?pr=1071
from kani.
See this thread for the details: https://users.rust-lang.org/t/cannot-compile-simple-tokio-example/109956/3
But basically our nightly version matches the latest released Rust compiler, which has now stabilized proc_macro_byte_character
feature. The proc_macro
build script checks the Rust compiler version to see whether it needs to enable this feature.
I believe there are three different fixes we can apply:
- Update our toolchain version, which will hopefully have that property stabilized.
- Change Kani to enable the feature by default for now.
- Downgrade the
proc_macro
version.
from kani.
But I'm still with https://users.rust-lang.org/t/cannot-compile-simple-tokio-example/109956/6: what has changed? Kani neither changed its toolchain version nor the cargo dependencies. So what proc_macro
version would be downgrading to when we had something that worked until a couple of hours ago?!
from kani.
The proc_macro
crate has a new minor version which includes this change. When building a project with cargo without a Cargo.lock file, cargo will download the latest minor version that matches your dependencies specification.
To go around this issue, an user can either ensure their build are locked via Cargo.lock or specify an exact version in their Cargo.toml. Any version previous to the change I just pasted should do the trick.
from kani.
Note that the toolchain upgrade will fix this issue as expected.
from kani.
@joshlf is this something that is blocking you?
from kani.
@joshlf is this something that is blocking you?
It is, yeah. We run Kani as part of CI, so it's preventing us from merging PRs (without manual override, which we'd like to avoid if possible). We use the Kani GitHub Action in our CI config rather than invoking cargo kani
directly, so I'm not sure whether the Cargo.lock
workaround would work for us, although I haven't tried it.
I assume that once the Kani GitHub Action can cut a new release with a more recent nightly toolchain pinned, upgrading to that new version would resolve our issue.
from kani.
@joshlf is this something that is blocking you?
It is, yeah. We run Kani as part of CI, so it's preventing us from merging PRs (without manual override, which we'd like to avoid if possible). We use the Kani GitHub Action in our CI config rather than invoking
cargo kani
directly, so I'm not sure whether theCargo.lock
workaround would work for us, although I haven't tried it.
Thanks for letting us know @joshlf. I would expect the Cargo.lock
work around to work as long as there is one in the working directory.
I assume that once the Kani GitHub Action can cut a new release with a more recent nightly toolchain pinned, upgrading to that new version would resolve our issue.
That said, we are considering creating a release with the fix to unblock users without forcing them to create a workaround.
from kani.
@joshlf we have now released a new version of Kani which should fix this issue. Please let us know if you are still having trouble.
from kani.
Related Issues (20)
- Benchcomp fails to render scatterplot when some data values are empty
- Disallow side effects in contract expressions HOT 1
- Toolchain upgrade to nightly-2024-05-25 failed HOT 1
- Toolchain upgrade to nightly-2024-05-29 failed HOT 11
- Add an option to Kani to verify a custom version of the standard library.
- Contract unexpectedly fails HOT 6
- Kani fails to detect use of a dangling pointer dereference in println HOT 10
- Issue injecting Kani module to dependency (zerocopy) HOT 6
- Contracts: macro allowing for contraction of specific variables HOT 3
- Property representing `unreachable!()` is marked as SUCCESS instead of UNREACHABLE
- Valid value checks does not check `char` surrogate values
- kani fails to untar on Ubuntu 24.04 HOT 3
- Kani contract cannot be applied to functions with `rustc_diagnostic_item`
- Cannot verify a constant function with contracts
- Cleanup work due to enabling standard library verification
- Cannot verify a constant function if crate has `effect` feature enabled HOT 1
- Toolchain upgrade to nightly-2024-06-12 failed
- Review where we might be incorrectly ignoring projects into ZSTs
- Reachability analysis cannot see through FFI
- Ensure that `Arbitrary` respects `Invariant` somehow
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from kani.