search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.15k stars 66 forks source link

Fix the rustup toolchain channel regex #1148

Closed xal-0 closed 2 months ago

xal-0 commented 4 months ago

The regex used to extract the channel from the output of rustup show active-toolchain misidentifies aarch64 as part of the channel on Linux:

$ vargo build
error: rustup is using a toolchain with channel 1.76.0-aarch64, we expect 1.76.0
do you have a rustup override set?
$ rustup show active-toolchain
1.76.0-aarch64-unknown-linux-gnu (overridden by '/verus/rust-toolchain.toml')

This is the result of a regex that consumes - as part of the channel name: ^(([A-Za-z0-9.-]+)-[A-Za-z0-9_]+-[A-Za-z0-9]+-[A-Za-z0-9-]+)

The first capture group can't contain _, so it works on x86_64. According to the toolchain spec grammar, we'll need to use a less liberal regex to avoid capturing too much as the channel/date.

<channel>[-<date>][-<host>]

<channel>       = stable|beta|nightly|<major.minor>|<major.minor.patch>
<date>          = YYYY-MM-DD
<host>          = <target-triple>

The regex also causes problems on platforms that use a target "triple" that isn't a triple, like 1.76.0-aarch64-apple-darwin, so we make no assumptions about the number of --separated words in the target triple.

parno commented 4 months ago

I ran into this issue too. With help from @jaybosamiya, we came up with this alternate approach https://github.com/verus-lang/verus/pull/1103/commits/592ad9b554cf1240f7f516df6c0771b3999bcd47 (ignore the accidental removal of the raw string annotation).

utaal commented 2 months ago

Sorry for the delay on this, and thanks @parno for the alternate approach.

I think the combination of https://github.com/verus-lang/verus/commit/592ad9b554cf1240f7f516df6c0771b3999bcd47 and https://github.com/verus-lang/verus/commit/560a53857e3ffb5b46f2e6a3b029f5f1862c4828 should address the same issue. Both are now in main, so I'll close this. If a similar problem comes up again, please reopen, or open an issue.