Flatten prove::prove::prove module nesting (#418) - #431
Merged
Conversation
Collaborator
|
Thanks for contributing to formality! :) |
Mslady-jojo
force-pushed
the
flatten-prove-module
branch
from
July 10, 2026 19:01
245acd8 to
e099a56
Compare
This comment has been minimized.
This comment has been minimized.
nikomatsakis
requested changes
Jul 15, 2026
tiif
approved these changes
Jul 17, 2026
Collapses the triple-nested prove module structure into a single flat prove module. No logic changes - this is a pure structural refactor. Updated all import paths accordingly. Test snapshots updated to reflect new file paths in error messages.
nikomatsakis
force-pushed
the
flatten-prove-module
branch
from
July 21, 2026 16:55
e099a56 to
4d5c4d4
Compare
Collaborator
|
This PR was rebased onto a different main commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
nikomatsakis
approved these changes
Jul 21, 2026
This was referenced Jul 21, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
The
provemodule informality-rustwas nested three levels deep (prove::prove::prove::*), withprove.rsdeclaring a submoduleprove(prove/prove.rs), which itself declared another submoduleprove(prove/prove/prove.rs) containing the actual proving logic (env,prove_eq,prove_wf,combinators, etc). This meant every import path across the codebase had to spell outcrate::prove::prove::prove::Xorcrate::prove::prove::Xjust to reach ordinary sibling items, with no corresponding conceptual separation to justify the extra layers.What changed:
prove/prove/prove/*andprove/prove/*up intoprove/*directly (git mv, so history is preserved).prove/prove.rsandprove/prove/prove.rs) directly into the top-levelprove.rs, combining theirmoddeclarations andpub usere-exports (de-duplicating overlapping re-exports likeConstrained/Constraintsand the negation functions, which were previously re-exported from two places).check/,codegen/,to_rust/,grammar/, and withinprove/itself) fromcrate::prove::prove::X/crate::prove::prove::prove::Xto the flatcrate::prove::X.expect_testsnapshots intests/basic_tests.rswhere the expected output embedded the old (now-changed) source file paths in panic/error messages. No logic or assertion values changed only the file path strings.cargo clippy --all-targets: same pre-existing warning count asmain; no new warnings introduced, and none touch files modified in this PR. Left untouched to keep this PR scoped to the module restructuring only.This is a pure structural refactor no behavior changes.