search

verus-lang / verus

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

Provide print_u64 only for feature = std #1121

Closed ouuan closed 4 months ago

ouuan commented 4 months ago

It's useless to provide a function that does nothing for no_std. Now it introduces a warning that the parameter i is not used when building with no_std.

utaal commented 4 months ago

Hi @ouuan, thanks for the PR. Can you explain your rationale further?

As far as I can tell, this will make print_u64 unavailable to non-std builds, which is technically a breaking change. I'm not sure this is worth the potential breakage (I think we'd need to deprecate the function first).

ouuan commented 4 months ago

My main consideration is to avoid the unused variable warning. We may use an #[allow] for it instead if you want to avoid the breakage.

However, I don't think anyone would actually use this function in no_std, as it's a no-op. One may argue that this no-op is a semantic bug of this function. We can deprecate it first, but given the active development status of Verus, I don't think it's necessary.

utaal commented 4 months ago

My main consideration is to avoid the unused variable warning. We may use an #[allow] for it instead if you want to avoid the breakage.

Let's do that!

ouuan commented 4 months ago

Close this in favor of #1133