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

Add more files in examples/ to CI #34

Merged
merged 10 commits into from
Feb 27, 2024
Merged

Add more files in examples/ to CI #34

merged 10 commits into from
Feb 27, 2024

Conversation

jaybosamiya
Copy link
Collaborator

@jaybosamiya jaybosamiya commented Feb 26, 2024

This PR sets up more files from examples/ to be run on CI.

Since we didn't have these on CI, there was a regression in the parser that is also fixed in this PR.

Also, if the snapshot test for syntax.rs fails, we now get a nicer output (using a unified diff), rather than just dumping everything.

The mimalloc and nr examples suffer from issues when snapshot testing, so I've added them as ignored tests with reminders of why. However, we should not block this PR on fixing that, so that at least we start getting the CI checks on the rest.

Due to newly added `spec_fn`, `FnSpec` itself is deprecated. Nonetheless, we should support parsing it for older instances of Verus.

We used to support parsing it, but in a21b251, a copy-paste-typo got introduced which broke support for it.
Multiple files are blocked currently on #33
@jaybosamiya jaybosamiya requested a review from parno February 26, 2024 21:50
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 fixing the macro idempotentcy issue; that's an elegant way to address it.

@parno parno merged commit ad8fbf7 into main Feb 27, 2024
8 checks passed
@parno parno deleted the snapshot-examples branch February 27, 2024 02:45
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.

2 participants