diff --git a/.github/workflows/clippy_rust_engine.yml b/.github/workflows/clippy_rust_engine.yml index 51a5053051..9f2245ac6b 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 --all-features -- -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 705c07b164..61837468be 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()); } }