Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prevent rustfmt from messing with verusfmt #38

Merged
merged 6 commits into from
Feb 28, 2024

Conversation

jaybosamiya
Copy link
Collaborator

@jaybosamiya jaybosamiya commented Feb 27, 2024

Rustfmt messes with verusfmt's formatting, and this has been the cause of idempotency issues such as #33 and #36. With this PR, we close that out (hopefully) entirely.

In short, we add a new (minimal) parser that collapses any verus!{ ... } into verus!{} before passing it to rustfmt; upon getting a result from rustfmt, we expand out those verus!{} to verus!{ ... } again, thereby preventing rustfmt from messing with anything inside the body that we have carefully set up already.

This also allows us to enable the NR snapshot test, which is now stable. Fwiw, we could have fixed NR's non-idempotency if we could pass multiple macros to rustfmt's skip_macro_invocations config; however, that is blocked on an issue in rustfmt: rust-lang/rustfmt#6097; even once that is fixed, we would need to assume/check that the user is on recent-enough rustfmt (also it turns out that skip_macro_invocations is not stable on rustfmt), so the fix that this PR does is a much more manageable fix for us overall.

Additionally, this PR also adds in vstd as a snapshot test (which could not be added before, due to same idempotency issue).

Fixes #36

Copy link
Contributor

@parno parno left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for adding this. It's annoying to have to work around rustfmt this way, but it at least seems like it should definitively solve the problem.

@jaybosamiya jaybosamiya merged commit ccac41b into main Feb 28, 2024
8 checks passed
@jaybosamiya jaybosamiya deleted the rustfmt-without-verus-call branch February 28, 2024 03:15
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.

Non-idempotent verus! inside macro_rules!
2 participants