From 537d3f03f23fa47c80883dcc3de7d2e74206e42c Mon Sep 17 00:00:00 2001 From: Zac Scheiwe Date: Tue, 27 Oct 2026 16:49:30 +1100 Subject: [PATCH 1/2] Fix unused method warning and run Clippy on cargo-hax in CI Fixes #2265 - `ToolVersions::iter` (cli/cargo-hax/src/tools/manifest.rs) is only used by tests, so gate it behind `#[cfg(test)]` instead of removing it. - Add a CI step in .github/workflows/clippy_rust_engine.yml running `cargo clippy -p cargo-hax --no-deps --all-targets -- -D warnings`. - Fix the existing Clippy lints in cargo-hax so that step passes (no behaviour change). --- .github/workflows/clippy_rust_engine.yml | 7 +++++-- cli/cargo-hax/src/aeneas.rs | 12 +++++------- cli/cargo-hax/src/aeneas/package.rs | 22 +++++++++++----------- cli/cargo-hax/src/scenario.rs | 7 ++++--- cli/cargo-hax/src/tools/manifest.rs | 1 + cli/cargo-hax/src/tools/project.rs | 7 ++++--- 6 files changed, 30 insertions(+), 26 deletions(-) diff --git a/.github/workflows/clippy_rust_engine.yml b/.github/workflows/clippy_rust_engine.yml index 51a5053051..e37574ca28 100644 --- a/.github/workflows/clippy_rust_engine.yml +++ b/.github/workflows/clippy_rust_engine.yml @@ -1,4 +1,4 @@ -name: Linting for the Rust engine +name: Linting for the Rust engine and cargo-hax on: pull_request: @@ -16,6 +16,9 @@ jobs: - name: Install clippy run: | rustup component add clippy - - name: Run clippy + - name: Run clippy on the Rust engine run: | cargo clippy -p hax-rust-engine -- -D warnings --no-deps + - name: Run clippy on cargo-hax + run: | + cargo clippy -p cargo-hax --no-deps --all-targets -- -D warnings diff --git a/cli/cargo-hax/src/aeneas.rs b/cli/cargo-hax/src/aeneas.rs index 5f89d52d4f..7902388441 100644 --- a/cli/cargo-hax/src/aeneas.rs +++ b/cli/cargo-hax/src/aeneas.rs @@ -407,14 +407,12 @@ pub fn run( // An overridden layout moves the output away from `out_dir`: creating // the default tree would leave an unused directory behind. - if !layout_overridden { - if let Err(e) = fs::create_dir_all(&out_dir) { - HaxMessage::GenericError { - message: format!("failed to create output directory: {}", e), - } - .report(message_format, None); - return true; + if !layout_overridden && let Err(e) = fs::create_dir_all(&out_dir) { + HaxMessage::GenericError { + message: format!("failed to create output directory: {}", e), } + .report(message_format, None); + return true; } if let Err(e) = fs::create_dir_all(&llbc_dir) { diff --git a/cli/cargo-hax/src/aeneas/package.rs b/cli/cargo-hax/src/aeneas/package.rs index 2cb1b221f7..716fcbe091 100644 --- a/cli/cargo-hax/src/aeneas/package.rs +++ b/cli/cargo-hax/src/aeneas/package.rs @@ -745,18 +745,18 @@ pub fn generate( // generation. if !lean_dir.join("lakefile.lean").exists() { let lakefile = lean_dir.join("lakefile.toml"); - if absent_or_empty(&lakefile) { - if let Some(path) = aeneas_local_path { - HaxMessage::GenericWarning { - message: format!( - "aeneas resolves to the local binary {}; pinning the aeneas Lean \ - library to the default {} in the generated lakefile", - path.display(), - pins.aeneas_rev - ), - } - .report(message_format, None); + if absent_or_empty(&lakefile) + && let Some(path) = aeneas_local_path + { + HaxMessage::GenericWarning { + message: format!( + "aeneas resolves to the local binary {}; pinning the aeneas Lean \ + library to the default {} in the generated lakefile", + path.display(), + pins.aeneas_rev + ), } + .report(message_format, None); } error |= write_if_absent( &lakefile, diff --git a/cli/cargo-hax/src/scenario.rs b/cli/cargo-hax/src/scenario.rs index 2bf316d008..791477cad2 100644 --- a/cli/cargo-hax/src/scenario.rs +++ b/cli/cargo-hax/src/scenario.rs @@ -124,12 +124,13 @@ fn extract( } if scope.is_empty() { - return Err(format!( + return Err( "no scenarios in scope. Declare extraction configurations as \ `[scenario.]` tables in a `hax.toml` next to Cargo.toml \ (workspace root or member crate); see the hax manual \ (docs/manual/tools.md)" - )); + .to_string(), + ); } if !packages.is_empty() { @@ -148,7 +149,7 @@ fn extract( // name in scope; an unmatched name is an error and nothing runs. A // repeated name (or two names matching the same scenario) runs it once. let selected: Vec<&ResolvedScenario> = if names.is_empty() { - scope.iter().copied().collect() + scope.to_vec() } else { let mut selected: Vec<&ResolvedScenario> = Vec::new(); let mut taken: std::collections::BTreeSet = std::collections::BTreeSet::new(); diff --git a/cli/cargo-hax/src/tools/manifest.rs b/cli/cargo-hax/src/tools/manifest.rs index 4b57c067f1..cc93119830 100644 --- a/cli/cargo-hax/src/tools/manifest.rs +++ b/cli/cargo-hax/src/tools/manifest.rs @@ -58,6 +58,7 @@ impl ToolVersions { self.0.iter().map(|(version, _)| version.as_str()) } + #[cfg(test)] pub fn iter(&self) -> impl Iterator)> { self.0 .iter() diff --git a/cli/cargo-hax/src/tools/project.rs b/cli/cargo-hax/src/tools/project.rs index f92fe4fe9f..ab58bb9f12 100644 --- a/cli/cargo-hax/src/tools/project.rs +++ b/cli/cargo-hax/src/tools/project.rs @@ -84,9 +84,10 @@ impl CargoArgs { if let Some(value) = flags.next() { args.metadata_args.extend([flag.clone(), value.clone()]); } - } else if name == "--features" || (flag.starts_with("-F") && flag.len() > 2) { - args.metadata_args.push(flag.clone()); - } else if FORWARDED.contains(&name) { + } else if name == "--features" + || (flag.starts_with("-F") && flag.len() > 2) + || FORWARDED.contains(&name) + { args.metadata_args.push(flag.clone()); } } From a6b45e8807d5011cc68bc79c86cbfc485664769d Mon Sep 17 00:00:00 2001 From: Zac Scheiwe Date: Wed, 28 Oct 2026 13:35:57 +1100 Subject: [PATCH 2/2] Update .github/workflows/clippy_rust_engine.yml Co-authored-by: maximebuyse <45398004+maximebuyse@users.noreply.github.com> --- .github/workflows/clippy_rust_engine.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/clippy_rust_engine.yml b/.github/workflows/clippy_rust_engine.yml index e37574ca28..9f2245ac6b 100644 --- a/.github/workflows/clippy_rust_engine.yml +++ b/.github/workflows/clippy_rust_engine.yml @@ -21,4 +21,4 @@ jobs: cargo clippy -p hax-rust-engine -- -D warnings --no-deps - name: Run clippy on cargo-hax run: | - cargo clippy -p cargo-hax --no-deps --all-targets -- -D warnings + cargo clippy -p cargo-hax --no-deps --all-targets --all-features -- -D warnings