Skip to content

Allow considering part of the serialized code as a library #6294

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 5 commits into from
Jul 4, 2025
Merged

Allow considering part of the serialized code as a library #6294

merged 5 commits into from
Jul 4, 2025

Conversation

@keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Jul 2, 2025 •
edited
Loading

What was changed?

  • Allow considering part of the serialized code as a library

How has this been tested?

  • Added a test inputFormatLibrary.dfy
  • Manually tested using a serializing customer

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

olivier-aws
olivier-aws previously approved these changes Jul 2, 2025
View reviewed changes
Copy link
Contributor

@olivier-aws olivier-aws left a comment

Choose a reason for hiding this comment

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

LGTM. Any chance we can add an integration test that validates the behavior (e.g. by extending/modifying inputFormatAnything.dfy)?

@keyboardDrummer
Copy link
Member Author

LGTM. Any chance we can add an integration test that validates the behavior (e.g. by extending/modifying inputFormatAnything.dfy)?

Added the inputFormatLibrary.dfy test

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) July 3, 2025 15:13
@keyboardDrummer keyboardDrummer merged commit 14c4857 into dafny-lang:master Jul 4, 2025
46 of 48 checks passed
@keyboardDrummer keyboardDrummer deleted the librarySerialization branch July 5, 2025 12:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-aws robin-aws robin-aws approved these changes

@olivier-aws olivier-aws Awaiting requested review from olivier-aws

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@keyboardDrummer @robin-aws @olivier-aws