From 55af204a2f1c713e27e0caf0f3a3bb01a2f198c2 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Mon, 6 Apr 2026 21:14:29 +0000 Subject: [PATCH] [hermes] Track output for more integration tests gherrit-pr-id: G5hqizeipgnmwhocpqscopsoqtirndpdi --- .../tests/fixtures/dst_layout/expected.stderr | 1 + hermes/tests/fixtures/dst_layout/hermes.toml | 1 + .../test_7_1_phantom_fn/expected.stderr | 13 + .../test_7_1_phantom_fn/hermes.toml | 1 + .../test_7_3_ghost_spec/expected.stderr | 17 ++ .../test_7_3_ghost_spec/hermes.toml | 1 + .../test_8_2_unions/expected.stderr | 22 ++ .../test_8_2_unions/hermes.toml | 1 + .../test_4_6_assoc_types/expected.stderr | 1 + .../test_4_6_assoc_types/hermes.toml | 1 + .../test_5_4_std_types/expected.stderr | 24 ++ .../test_5_4_std_types/hermes.toml | 1 + .../test_6_1_external_crate/expected.stderr | 1 + .../test_6_1_external_crate/hermes.toml | 1 + .../test_6_3_renaming/expected.stderr | 1 + .../test_6_3_renaming/hermes.toml | 1 + .../test_3_3_ret_mut/expected.stderr | 31 +++ .../test_3_3_ret_mut/hermes.toml | 1 + .../expected.stderr | 1 + .../test_1_1_lean_keywords_fns/hermes.toml | 1 + .../expected.stderr | 242 ++++++++++++++++++ .../test_1_2_lean_keywords_args/hermes.toml | 1 + .../expected.stderr | 1 + .../test_1_3_rust_keywords_idents/hermes.toml | 1 + .../test_11_2_monolith/expected.stderr | 20 ++ .../test_11_2_monolith/hermes.toml | 1 + .../test_2_3_zst/expected.stderr | 1 + .../edge_cases_types/test_2_3_zst/hermes.toml | 1 + .../test_2_6_nested_refs/expected.stderr | 1 + .../test_2_6_nested_refs/hermes.toml | 1 + .../fixtures/lean_generation/hermes.toml | 1 + .../tests/fixtures/multi_artifact/hermes.toml | 1 + .../raw_ptr_dst_layout/expected.stderr | 30 +++ .../fixtures/raw_ptr_dst_layout/hermes.toml | 1 + .../success_allow_sorry/source/src/lib.rs | 2 +- hermes/tests/integration.rs | 22 +- 36 files changed, 440 insertions(+), 9 deletions(-) create mode 100644 hermes/tests/fixtures/dst_layout/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_naming/test_1_2_lean_keywords_args/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_stress/test_11_2_monolith/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_types/test_2_3_zst/expected.stderr create mode 100644 hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/expected.stderr create mode 100644 hermes/tests/fixtures/raw_ptr_dst_layout/expected.stderr diff --git a/hermes/tests/fixtures/dst_layout/expected.stderr b/hermes/tests/fixtures/dst_layout/expected.stderr new file mode 100644 index 0000000000..5424ade65f --- /dev/null +++ b/hermes/tests/fixtures/dst_layout/expected.stderr @@ -0,0 +1 @@ +\n \ No newline at end of file diff --git a/hermes/tests/fixtures/dst_layout/hermes.toml b/hermes/tests/fixtures/dst_layout/hermes.toml index e1d0e8434c..1c9fba910a 100644 --- a/hermes/tests/fixtures/dst_layout/hermes.toml +++ b/hermes/tests/fixtures/dst_layout/hermes.toml @@ -5,4 +5,5 @@ Minimal reproduction of KnownLayout bounding DstLayout's attributes. [test] # Temporarily allowing this to fail while we debug other things. expected_status = "known_bug" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"] diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr new file mode 100644 index 0000000000..463ccba9e8 --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/expected.stderr @@ -0,0 +1,13 @@ + Compiling test_7_1_phantom_fn v0.1.0 ([PROJECT_ROOT]) +warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item + + +thread 'rustc' () panicked at src/errors.rs:278:13: +when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +ERROR Compilation panicked +error: could not compile `test_7_1_phantom_fn` (lib) + +Caused by: + process didn't exit successfully: `[CACHE_ROOT]/charon-driver [RUSTUP_TOOLCHAIN]/bin/rustc --crate-name test_7_1_phantom_fn --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn=/dummy` (exit status: 101) +Error: Charon failed with status: exit status: 101 diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml index bbf46073d2..d4a8d46869 100644 --- a/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_cfg/test_7_1_phantom_fn/hermes.toml @@ -5,4 +5,5 @@ Behavior: Uses conditionally compiled functions (`#[cfg(target_os = ...)]`). Ver [test] expected_status = "failure" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr new file mode 100644 index 0000000000..a08f91d0d6 --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/expected.stderr @@ -0,0 +1,17 @@ + Compiling test_7_3_ghost_spec v0.1.0 ([PROJECT_ROOT]) +warning: when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item + --> src/lib.rs:18:36 + | +18 | pub fn linux_only() -> u32 { 100 } + | ^ + + +thread 'rustc' () panicked at src/errors.rs:278:13: +when processing starting pattern `crate::windows_only`: path `crate::windows_only` does not correspond to any item +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +ERROR Compilation panicked +error: could not compile `test_7_3_ghost_spec` (lib) + +Caused by: + process didn't exit successfully: `[CACHE_ROOT]/charon-driver [RUSTUP_TOOLCHAIN]/bin/rustc --crate-name test_7_3_ghost_spec --edition=2021 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata= -C extra-filename=- --out-dir [PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/incremental -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/x86_64-unknown-linux-gnu/debug/deps -L dependency=[PROJECT_ROOT]/target/hermes/cargo_target/debug/deps --remap-path-prefix=tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec=/dummy` (exit status: 101) +Error: Charon failed with status: exit status: 101 diff --git a/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml index fc21b21879..7c7a14c9db 100644 --- a/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_cfg/test_7_3_ghost_spec/hermes.toml @@ -5,4 +5,5 @@ Behavior: Provides annotated functions under `#[cfg]`. Verifies only the specifi [test] expected_status = "failure" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr new file mode 100644 index 0000000000..00610257bb --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/expected.stderr @@ -0,0 +1,22 @@ +Error: Aeneas failed for package 'test_8_2_unions' with status: exit status: 2 +stderr: +Applied prepasses: [----------------------------------------------------] 0/2 ⠋Applied prepasses: [##########################--------------------------] 1/2 ⠋Applied prepasses: [####################################################] 2/2 ✔️ +Uncaught exception: + + (Failure + "unions are not supported\ + \nSource: 'src/lib.rs', lines 2:0-5:1\ + \nCompiler source: llbc/TypesAnalysis.ml, line 503") + +Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23 +Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43 +Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74 +Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23 +Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62 +Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66 +Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71 +Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37 + diff --git a/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml index 51504c700b..39050ab597 100644 --- a/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_charon/test_8_2_unions/hermes.toml @@ -5,4 +5,5 @@ Behavior: Delcares a `pub union U { ... }` and accesses it in an `unsafe` block. [test] expected_status = "failure" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr new file mode 100644 index 0000000000..5424ade65f --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/expected.stderr @@ -0,0 +1 @@ +\n \ No newline at end of file diff --git a/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml index 6ab9e06772..54c4623ff5 100644 --- a/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml @@ -7,4 +7,5 @@ Behavior: In an `isValid` boundary condition, queries the default instantiation # FIXME(#3089): Update the syntax in `lib.rs` to be valid Lean, and get this # passing. expected_status = "known_bug" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"] diff --git a/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr new file mode 100644 index 0000000000..2e0b426a61 --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/expected.stderr @@ -0,0 +1,24 @@ +[External Error] generated/Test54StdTypesTest54StdTypes/Test54StdTypesTest54StdTypes.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 +[External Error] generated/Test54StdTypesTest54StdTypes/Test54StdTypesTest54StdTypes.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 +[External Error] generated/Test54StdTypesTest54StdTypes/Test54StdTypesTest54StdTypes.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 + +Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement. +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/edge_cases_logic/test_5_4_std_types/hermes.toml b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/hermes.toml index 2846817849..9eebb0840f 100644 --- a/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_logic/test_5_4_std_types/hermes.toml @@ -5,4 +5,5 @@ Behavior: Uses `Vec` and `String` directly in function signatures. Confirms the [test] expected_status = "failure" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr new file mode 100644 index 0000000000..5424ade65f --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/expected.stderr @@ -0,0 +1 @@ +\n \ No newline at end of file diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml index d37e00afb8..8f248d392a 100644 --- a/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_modules/test_6_1_external_crate/hermes.toml @@ -5,4 +5,5 @@ Behavior: Imports and uses `std::collections::HashMap` in a signature. Validates [test] expected_status = "known_bug" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr new file mode 100644 index 0000000000..5424ade65f --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/expected.stderr @@ -0,0 +1 @@ +\n \ No newline at end of file diff --git a/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml index 8d46b4da52..08f4d9fd92 100644 --- a/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_modules/test_6_3_renaming/hermes.toml @@ -5,4 +5,5 @@ Behavior: Re-aliases `Vec` using `use ... as MyVec;`. Ensures Charon de-aliases [test] expected_status = "known_bug" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr new file mode 100644 index 0000000000..064515138f --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/expected.stderr @@ -0,0 +1,31 @@ +[External Error] generated/Test33RetMutTest33RetMut/Test33RetMutTest33RetMut.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 +[External Error] generated/Test33RetMutTest33RetMut/Test33RetMutTest33RetMut.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 +[External Error] generated/Test33RetMutTest33RetMut/Test33RetMutTest33RetMut.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 +[External Error] generated/Test33RetMutTest33RetMut/Test33RetMutTest33RetMut.lean: Function expected at + Vec +but this term has type + ?m.1 + +Note: Expected a function because this term is being applied to the argument + Std.U32 + +Hint: The identifier `Vec` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement. +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/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml index a214eebb09..1f0c678d54 100644 --- a/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_mut_refs/test_3_3_ret_mut/hermes.toml @@ -5,4 +5,5 @@ Behavior: Mutates a vector to return an inner value (`v.pop()`). Validates Aenea [test] expected_status = "failure" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr new file mode 100644 index 0000000000..5424ade65f --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/expected.stderr @@ -0,0 +1 @@ +\n \ No newline at end of file diff --git a/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml index e7cd6e5f5d..7c61221e1d 100644 --- a/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml +++ b/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml @@ -6,4 +6,5 @@ Behavior: Asserts that `fn theorem()`, `fn match()`, etc. are strictly escaped i [test] # FIXME(#3089): This should succeed expected_status = "known_bug" +stderr_file = "expected.stderr" args = ["verify", "--allow-sorry"] diff --git a/hermes/tests/fixtures/edge_cases_naming/test_1_2_lean_keywords_args/expected.stderr b/hermes/tests/fixtures/edge_cases_naming/test_1_2_lean_keywords_args/expected.stderr new file mode 100644 index 0000000000..b48f80eeaf --- /dev/null +++ b/hermes/tests/fixtures/edge_cases_naming/test_1_2_lean_keywords_args/expected.stderr @@ -0,0 +1,242 @@ + ⚠ unused variable: `theorem` + ╭─[[PROJECT_ROOT]/src/lib.rs:10:5] + 9 │ pub fn test_args( + 10 │ theorem: u32, + · ───┬─── + · ╰── + 11 │ axiom: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `axiom` + ╭─[[PROJECT_ROOT]/src/lib.rs:11:5] + 10 │ theorem: u32, + 11 │ axiom: u32, + · ──┬── + · ╰── + 12 │ variable: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `variable` + ╭─[[PROJECT_ROOT]/src/lib.rs:12:5] + 11 │ axiom: u32, + 12 │ variable: u32, + · ────┬─── + · ╰── + 13 │ lemma: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `lemma` + ╭─[[PROJECT_ROOT]/src/lib.rs:13:5] + 12 │ variable: u32, + 13 │ lemma: u32, + · ──┬── + · ╰── + 14 │ def: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `def` + ╭─[[PROJECT_ROOT]/src/lib.rs:14:5] + 13 │ lemma: u32, + 14 │ def: u32, + · ─┬─ + · ╰── + 15 │ class: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `class` + ╭─[[PROJECT_ROOT]/src/lib.rs:15:5] + 14 │ def: u32, + 15 │ class: u32, + · ──┬── + · ╰── + 16 │ instance: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `instance` + ╭─[[PROJECT_ROOT]/src/lib.rs:16:5] + 15 │ class: u32, + 16 │ instance: u32, + · ────┬─── + · ╰── + 17 │ structure: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `structure` + ╭─[[PROJECT_ROOT]/src/lib.rs:17:5] + 16 │ instance: u32, + 17 │ structure: u32, + · ────┬──── + · ╰── + 18 │ inductive: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `inductive` + ╭─[[PROJECT_ROOT]/src/lib.rs:18:5] + 17 │ structure: u32, + 18 │ inductive: u32, + · ────┬──── + · ╰── + 19 │ from: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `from` + ╭─[[PROJECT_ROOT]/src/lib.rs:19:5] + 18 │ inductive: u32, + 19 │ from: u32, + · ──┬─ + · ╰── + 20 │ have: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `have` + ╭─[[PROJECT_ROOT]/src/lib.rs:20:5] + 19 │ from: u32, + 20 │ have: u32, + · ──┬─ + · ╰── + 21 │ show: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `show` + ╭─[[PROJECT_ROOT]/src/lib.rs:21:5] + 20 │ have: u32, + 21 │ show: u32, + · ──┬─ + · ╰── + 22 │ calc: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `calc` + ╭─[[PROJECT_ROOT]/src/lib.rs:22:5] + 21 │ show: u32, + 22 │ calc: u32, + · ──┬─ + · ╰── + 23 │ then: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `then` + ╭─[[PROJECT_ROOT]/src/lib.rs:23:5] + 22 │ calc: u32, + 23 │ then: u32, + · ──┬─ + · ╰── + 24 │ with: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `with` + ╭─[[PROJECT_ROOT]/src/lib.rs:24:5] + 23 │ then: u32, + 24 │ with: u32, + · ──┬─ + · ╰── + 25 │ section: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `section` + ╭─[[PROJECT_ROOT]/src/lib.rs:25:5] + 24 │ with: u32, + 25 │ section: u32, + · ───┬─── + · ╰── + 26 │ namespace: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `namespace` + ╭─[[PROJECT_ROOT]/src/lib.rs:26:5] + 25 │ section: u32, + 26 │ namespace: u32, + · ────┬──── + · ╰── + 27 │ end: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `end` + ╭─[[PROJECT_ROOT]/src/lib.rs:27:5] + 26 │ namespace: u32, + 27 │ end: u32, + · ─┬─ + · ╰── + 28 │ import: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `import` + ╭─[[PROJECT_ROOT]/src/lib.rs:28:5] + 27 │ end: u32, + 28 │ import: u32, + · ───┬── + · ╰── + 29 │ open: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `open` + ╭─[[PROJECT_ROOT]/src/lib.rs:29:5] + 28 │ import: u32, + 29 │ open: u32, + · ──┬─ + · ╰── + 30 │ attribute: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `attribute` + ╭─[[PROJECT_ROOT]/src/lib.rs:30:5] + 29 │ open: u32, + 30 │ attribute: u32, + · ────┬──── + · ╰── + 31 │ universe: u32, + ╰──── + help: if this is intentional, prefix it with an underscore + + ⚠ unused variable: `universe` + ╭─[[PROJECT_ROOT]/src/lib.rs:31:5] + 30 │ attribute: u32, + 31 │ universe: u32, + · ────┬─── + · ╰── + 32 │ ) {} + ╰──── + help: if this is intentional, prefix it with an underscore + +Error: Lean build failed +STDOUT: +⚠ [1516/1629] Replayed Aeneas.Std.Slice +warning: Aeneas/Std/Slice.lean:297:4: declaration uses `sorry` +warning: Aeneas/Std/Slice.lean:520:8: declaration uses `sorry` +⚠ [1552/1629] Replayed Aeneas.Std.String +warning: Aeneas/Std/String.lean:9:4: declaration uses `sorry` +⚠ [1565/1629] Replayed Aeneas.Std.SliceIter +warning: Aeneas/Std/SliceIter.lean:142:4: declaration uses `sorry` +⚠ [1568/1629] Replayed Aeneas.Std.StringIter +warning: Aeneas/Std/StringIter.lean:13:4: declaration uses `sorry` +✔ [1626/1629] Built Test12LeanKeywordsArgsTest12LeanKeywordsArgs.Types (