[hermes] Add generate subcommand

gherrit-pr-id: Go47kyyj6ojyz5dbcvuuavbfyxdlpsdyb

Author: joshlf

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

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/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() {}