diff --git a/hermes/docs/agent/07_workflow.md b/hermes/docs/agent/07_workflow.md index 42e95d9ad7..3c29a4a88f 100644 --- a/hermes/docs/agent/07_workflow.md +++ b/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. \ No newline at end of file +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. diff --git a/hermes/llms-full.txt b/hermes/llms-full.txt index 073fbd1120..e2421fb054 100644 --- a/hermes/llms-full.txt +++ b/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. + diff --git a/hermes/src/aeneas.rs b/hermes/src/aeneas.rs index 6e03759569..cb54ecb823 100644 --- a/hermes/src/aeneas.rs +++ b/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(()) diff --git a/hermes/src/main.rs b/hermes/src/main.rs index 0bedba4fcb..d1476b69cb 100644 --- a/hermes/src/main.rs +++ b/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()?; } diff --git a/hermes/tests/fixtures/allow_sorry_fallbacks/expected.stderr b/hermes/tests/fixtures/allow_sorry_fallbacks/expected.stderr index b470ce2ae4..13c68a744d 100644 --- a/hermes/tests/fixtures/allow_sorry_fallbacks/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/const_generics/expected.stderr b/hermes/tests/fixtures/const_generics/expected.stderr index fc7e07526d..b38a1c2e66 100644 --- a/hermes/tests/fixtures/const_generics/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/diagnostic_mapping/expected.stderr b/hermes/tests/fixtures/diagnostic_mapping/expected.stderr index 07c8771dd7..92145d49da 100644 --- a/hermes/tests/fixtures/diagnostic_mapping/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/enums_pattern_matching/expected.stderr b/hermes/tests/fixtures/enums_pattern_matching/expected.stderr index 70afafb140..ad1eaae5ed 100644 --- a/hermes/tests/fixtures/enums_pattern_matching/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/generate_output/expected-generate.stdout b/hermes/tests/fixtures/generate_output/expected-generate.stdout new file mode 100644 index 0000000000..ed98485c8e --- /dev/null +++ b/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 diff --git a/hermes/tests/fixtures/generate_output/hermes.toml b/hermes/tests/fixtures/generate_output/hermes.toml new file mode 100644 index 0000000000..c789aceeb2 --- /dev/null +++ b/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" diff --git a/hermes/tests/fixtures/generate_output/source/Cargo.toml b/hermes/tests/fixtures/generate_output/source/Cargo.toml new file mode 100644 index 0000000000..b348b5a916 --- /dev/null +++ b/hermes/tests/fixtures/generate_output/source/Cargo.toml @@ -0,0 +1,6 @@ +[package] +name = "expand_output" +version = "0.1.0" +edition = "2021" + +[workspace] diff --git a/hermes/tests/fixtures/generate_output/source/src/lib.rs b/hermes/tests/fixtures/generate_output/source/src/lib.rs new file mode 100644 index 0000000000..8afbc86ed9 --- /dev/null +++ b/hermes/tests/fixtures/generate_output/source/src/lib.rs @@ -0,0 +1,3 @@ +/// ```lean, hermes +/// ``` +pub fn foo() {} diff --git a/hermes/tests/fixtures/is_valid_verification/expected.stderr b/hermes/tests/fixtures/is_valid_verification/expected.stderr index 99fcbf1d4e..32a536c027 100644 --- a/hermes/tests/fixtures/is_valid_verification/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/named_bounds_lean_failures/expected.stderr b/hermes/tests/fixtures/named_bounds_lean_failures/expected.stderr index 2dff33b626..6dd3c21776 100644 --- a/hermes/tests/fixtures/named_bounds_lean_failures/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/sizedness/expected.stderr b/hermes/tests/fixtures/sizedness/expected.stderr index 96e7f6450f..e7dade0577 100644 --- a/hermes/tests/fixtures/sizedness/expected.stderr +++ b/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. diff --git a/hermes/tests/fixtures/type_features/expected.stderr b/hermes/tests/fixtures/type_features/expected.stderr index e3700cad00..be7be5cbe7 100644 --- a/hermes/tests/fixtures/type_features/expected.stderr +++ b/hermes/tests/fixtures/type_features/expected.stderr @@ -81,4 +81,4 @@ [External Error] generated/TypeFeaturesTypeFeatures/TypeFeaturesTypeFeatures.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.