Skip to content

fix: limit .mbtp inputs to check and prove - #2000

Merged
peter-jerry-ye merged 1 commit into
moonbitlang:mainfrom
peter-jerry-ye:codex/limit-mbtp-to-check-and-prove
Aug 6, 2026
Merged

fix: limit .mbtp inputs to check and prove#2000
peter-jerry-ye merged 1 commit into
moonbitlang:mainfrom
peter-jerry-ye:codex/limit-mbtp-to-check-and-prove

Conversation

@peter-jerry-ye

Copy link
Copy Markdown
Contributor

Summary

Proof helper files were unconditionally copied into every build target projection, so commands such as moon test passed them to moonc even though only moon check and moon prove should consume them.

This change gates .mbtp projection on the Check and Prove run modes while leaving package discovery and metadata unchanged. The existing verification fixture now asserts that check and prove include the helper, while build, test, bench, and bundle do not.

The change is limited to target file selection and its regression coverage.

@semanticdiff-com

semanticdiff-com Bot commented Aug 6, 2026

Copy link
Copy Markdown

Review changes with  SemanticDiff

Changed Files
File Status
  crates/moon/tests/test_cases/moon_prove/mod.rs  0% smaller
  crates/moonbuild-rupes-recta/src/build_plan/builders.rs  0% smaller

@peter-jerry-ye
peter-jerry-ye marked this pull request as ready for review August 6, 2026 07:32
@peter-jerry-ye
peter-jerry-ye merged commit 85ff01a into moonbitlang:main Aug 6, 2026
13 checks passed
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