Fix unused method warning and run Clippy on cargo-hax in CI

.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

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) {

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,

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.<name>]` 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<usize> = std::collections::BTreeSet::new();

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<Item = (&String, &BTreeMap<String, ArtifactEntry>)> {
         self.0
             .iter()

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());
             }
         }