Newest proc_macro2 version does not work with kani-0.49.0

[tautschnig]

See https://github.com/model-checking/kani/actions/runs/8683193890/job/23808816781:

1. It seems that, on this occasion, a manual PR with cargo updates will be required.
2. We need to fix the CI job to make sure that compilation failures do not trigger an early abort, but instead automatically cut an issue.

[tautschnig]

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.

[joshlf]

We ran into this too: https://github.com/google/zerocopy/actions/runs/8695299265/job/23846059719?pr=1071

[celinval]

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:

1. Update our toolchain version, which will hopefully have that property stabilized.
2. Change Kani to enable the feature by default for now.
3. Downgrade the proc_macro version.

[tautschnig]

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?!

[celinval]

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.

[celinval]

Note that the toolchain upgrade will fix this issue as expected.

[celinval]

@joshlf is this something that is blocking you?

[joshlf]

@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.

[celinval]

@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.

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.

[celinval]

@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.

[joshlf]

That appears to work for us, thanks!