[hermes] Add generate subcommand

hermes/docs/agent/07_workflow.md

@@ -51,4 +51,7 @@ When writing a proof, follow these tips:
 You will use these two commands to interact with Hermes. Both accept `--help`.
 
 1. Run `cargo run verify` to verify a target.
-2. Use `cargo run expand` to see the generated Lean code.
+2. Use `cargo run expand` to see the generated Lean code.
+3. Use `cargo run generate` to generate `.lean` files on the filesystem. You can use these to iterate on specifications and proofs using normal Lean tooling (`lake`, `lean`, etc) and copy results back to `.rs` files when you are done.
+
+You will likely want to start with `cargo run generate`, then iterate on `.lean` files directly, and only use `cargo run verify` for final verification once you have copied your work from temporary `.lean` files back to the source of truth `.rs` files.

hermes/llms-full.txt

@@ -786,6 +786,10 @@ You will use these two commands to interact with Hermes. Both accept `--help`.
 
 1. Run `cargo run verify` to verify a target.
 2. Use `cargo run expand` to see the generated Lean code.
+3. Use `cargo run generate` to generate `.lean` files on the filesystem. You can use these to iterate on specifications and proofs using normal Lean tooling (`lake`, `lean`, etc) and copy results back to `.rs` files when you are done.
+
+You will likely want to start with `cargo run generate`, then iterate on `.lean` files directly, and only use `cargo run verify` for final verification once you have copied your work from temporary `.lean` files back to the source of truth `.rs` files.
+
 
 <!-- File: src/Hermes.lean -->
 

hermes/src/aeneas.rs

@@ -298,10 +298,12 @@ open Lake DSL
 
 package hermes_verification
 
+@[default_target]
 lean_lib «Generated» where
   srcDir := "generated"
   roots := #[{roots_str}]
 
+@[default_target]
 lean_lib «Hermes» where
   srcDir := "hermes"
   roots := #[`Config, `Hermes]
@@ -343,9 +345,8 @@ lean_lib «User» where
     Ok(())
 }
 
-/// Completes Lean verification by generating Hermes `Specs.lean`, writing `Generated.lean`,
-/// and running `lake build` + diagnostics.
-pub fn verify_lean_workspace(roots: &LockedRoots, artifacts: &[HermesArtifact]) -> Result<()> {
+/// Generates Hermes `Specs.lean` and writes `Generated.lean`, but does not run the `lake build`.
+pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[HermesArtifact]) -> Result<()> {
     let lean_generated_root = roots.lean_generated_root();
     let mut generated_imports = String::new();
 
@@ -386,6 +387,13 @@ pub fn verify_lean_workspace(roots: &LockedRoots, artifacts: &[HermesArtifact])
     write_if_changed(&lean_generated_root.join("Generated.lean"), &generated_imports)
         .context("Failed to write Generated.lean")?;
 
+    Ok(())
+}
+
+/// Completes Lean verification by generating Hermes `Specs.lean`, writing `Generated.lean`,
+/// and running `lake build` + diagnostics.
+pub fn verify_lean_workspace(roots: &LockedRoots, artifacts: &[HermesArtifact]) -> Result<()> {
+    generate_lean_workspace(roots, artifacts)?;
     run_lake(roots, artifacts)
 }
 
@@ -627,7 +635,14 @@ fn run_lake(roots: &LockedRoots, artifacts: &[HermesArtifact]) -> Result<()> {
     }
 
     if has_errors {
-        bail!("Lean verification failed");
+        let cmd = if std::env::var("__ZEROCOPY_LOCAL_DEV").is_ok() {
+            "cargo run generate"
+        } else {
+            "cargo hermes generate"
+        };
+        bail!(
+            "Lean verification failed. Consider running `{cmd}`, iterating on generated `.lean` files, and copying results back to `.rs` files."
+        );
     }
 
     Ok(())

hermes/src/main.rs

@@ -29,6 +29,8 @@ enum Commands {
     Setup(resolve::SetupArgs),
     /// Expand a crate's Lean output
     Expand(ExpandArgs),
+    /// Generate Lean workspace and print paths without building
+    Generate(resolve::Args),
     #[command(hide = true)]
     ToolchainPath,
 }
@@ -73,6 +75,18 @@ fn main() -> anyhow::Result<()> {
                 aeneas::verify_lean_workspace(locked_roots, packages)
             })?;
         }
+        Commands::Generate(resolve_args) => {
+            prepare_and_run(&resolve_args, |locked_roots, packages| {
+                aeneas::generate_lean_workspace(locked_roots, packages)?;
+                let lean_root = locked_roots.lean_root();
+                println!("Lean workspace generated at: {}", lean_root.display());
+                println!();
+                println!("To manually build and experiment:");
+                println!("  1. cd {}", lean_root.display());
+                println!("  2. lake build");
+                Ok(())
+            })?;
+        }
         Commands::Setup(resolve::SetupArgs {}) => {
             setup::run_setup()?;
         }

hermes/tests/fixtures/allow_sorry_fallbacks/expected.stderr

@@ -69,4 +69,4 @@
  59 │ /// ```
     ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/const_generics/expected.stderr

@@ -8,4 +8,4 @@
  9 │ /// ```
    ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/diagnostic_mapping/expected.stderr

@@ -36,4 +36,4 @@
  42 │ /// ```
     ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/enums_pattern_matching/expected.stderr

@@ -12,4 +12,4 @@
  10 │ ///   | Enum.B b => b
     ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/generate_output/expected-generate.stdout

@@ -0,0 +1,5 @@
+Lean workspace generated at: [PROJECT_ROOT]/target/hermes/hermes_test_target/lean
+
+To manually build and experiment:
+  1. cd [PROJECT_ROOT]/target/hermes/hermes_test_target/lean
+  2. lake build

hermes/tests/fixtures/generate_output/hermes.toml

@@ -0,0 +1,7 @@
+description = "Test the `generate` subcommand"
+
+[[test.phases]]
+name = "Generate"
+args = ["generate", "--allow-sorry"]
+expected_status = "success"
+stdout_file = "expected-generate.stdout"

hermes/tests/fixtures/generate_output/source/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "expand_output"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]

hermes/tests/fixtures/generate_output/source/src/lib.rs

@@ -0,0 +1,3 @@
+/// ```lean, hermes
+/// ```
+pub fn foo() {}

hermes/tests/fixtures/is_valid_verification/expected.stderr

@@ -92,4 +92,4 @@
  29 │ /// ```
     ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/named_bounds_lean_failures/expected.stderr

@@ -166,4 +166,4 @@
  113 │     x
      ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/sizedness/expected.stderr

@@ -11,4 +11,4 @@
  9 │ /// ```
    ╰────
 
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.

hermes/tests/fixtures/type_features/expected.stderr

@@ -81,4 +81,4 @@
 
 [External Error] generated/TypeFeaturesTypeFeatures<HASH>/TypeFeaturesTypeFeatures<HASH>.lean: type expected, got
   (UsesAssoc Self : Type → Type)
-Error: Lean verification failed
+Error: Lean verification failed. Consider running `cargo run generate`, iterating on generated `.lean` files, and copying results back to `.rs` files.