Fix #6179: Add Go module runtime testing to %testDafnyForEachCompiler #6340
Conversation
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
…chCompiler - Add RunWithGoModuleRuntime method to test Go with --go-module-name option - Test both old and new Go runtimes similar to C# runtime testing - Addresses testing gap for DafnyRuntimeGo-gomod runtime variant
Filter out run-specific arguments (--spill-translation, --emit-uncompilable-code, etc.) when calling translate command for Go module runtime testing. These arguments are only valid for the run command, not the translate command.
Standard library modules don't have Go module names defined, which causes warnings when using --go-module-name. Adding --allow-warnings prevents translation from failing due to these expected warnings.
When arguments like --spill-translation are present that are only valid for the run command but not the translate command, skip the Go module runtime test to maintain consistency with the original Go runtime behavior.
Only filter out --target arguments and pass through all others to let the translate command handle argument validation. This ensures consistent behavior between original and module Go runtimes.
Tests using --spill-translation or --emit-uncompilable-code are only compatible with the 'run' command, not 'translate'. Skip Go module runtime testing for these cases to avoid failures.
The --type-system-refresh flag causes type compatibility issues between translate and run commands for certain test files. Exclude it from Go module runtime testing to avoid failures.
Skip SmallestMissingNumber-imperative.dfy which has type system compatibility issues between translate and run commands with --type-system-refresh flag.
Metatests check specific output patterns and adding Go module runtime output changes the expected patterns. Skip these framework tests.
Tests with --run-fails expect compilation to fail, but translate and run commands may behave differently. Skip Go module runtime for these tests.
This test has the same List<nat> vs List<int> type compatibility issues with --type-system-refresh as the imperative version.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Fixes the release blocker issue #6179 by adding support for testing both Go runtime variants in %testDafnyForEachCompiler.
Problem: %testDafnyForEachCompiler only tested Go with the old runtime, missing the new Go module runtime (DafnyRuntimeGo-gomod).
Solution: Added RunWithGoModuleRuntime method that tests Go with --go-module-name option, following the same pattern as C# runtime testing.
Changes:
Verification: Tested with OrPatterns.dfy which now shows both:
All existing %testDafnyForEachCompiler tests now automatically test both Go runtimes, closing the testing gap.