Skip to content

test: check Sym invariants in the vcgen tests - #16308

Closed
sgraf812 wants to merge 1 commit into
leanprover:masterfrom
sgraf812:sg/vcgen-tests-sym-debug
Closed

sgraf812 wants to merge 1 commit into
leanprover:masterfrom
sgraf812:sg/vcgen-tests-sym-debug

Conversation

@sgraf812

@sgraf812 sgraf812 commented Nov 6, 2026

Copy link
Copy Markdown
Member

The vcgen and mvcgen tests now run with sym.debug set, so the test suite catches a change that breaks the maximal sharing or another SymM invariant.

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF51DQwLT5S6Qt4iXvb
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 6, 2026
@sgraf812 sgraf812 closed this Nov 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant