Skip to content

lean_compiler: avoid duplicate compile-and-run output#245

Draft
latifkasuli wants to merge 1 commit into
leanEthereum:mainfrom
latifkasuli:fix/quiet-try-compile-and-run
Draft

lean_compiler: avoid duplicate compile-and-run output#245
latifkasuli wants to merge 1 commit into
leanEthereum:mainfrom
latifkasuli:fix/quiet-try-compile-and-run

Conversation

@latifkasuli
Copy link
Copy Markdown

Summary

  • remove the redundant summary print from try_compile_and_run
  • keep compile_and_run as the single printing wrapper
  • add a regression test proving try_compile_and_run returns the summary without writing it to stdout

Root cause

try_compile_and_run printed result.metadata.display() and returned a freshly computed display string. compile_and_run then printed the returned string again, so callers of compile_and_run saw the same execution summary twice.

Validation

  • cargo fmt --check
  • cargo test -p lean_compiler
  • cargo clippy -p lean_compiler --all-targets -- -D warnings

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant