Fix architecture detection by using .NET runtime architecture instead of system architecture#544
Merged
MikaelMayer merged 5 commits intomasterfrom Sep 9, 2025
Merged
Conversation
The previous fix detected system architecture but the real issue is that .NET can run under Rosetta translation on ARM64 Macs, requiring x64 Dafny binaries even on ARM64 hardware. Root cause analysis: - User has ARM64 Mac (uname -m returns arm64) - But .NET runtime is x64 (running under Rosetta) - Extension downloaded ARM64 Dafny but .NET needs x64 libraries - Error: 'have arm64, need x86_64' Solution: - Use 'dotnet --info' to detect actual .NET runtime architecture - Parse RID (Runtime Identifier) or Architecture field - Download Dafny binaries matching .NET runtime, not system hardware - Fallback to system detection if .NET detection fails This ensures compatibility when .NET runs under Rosetta translation.
- Remove trailing spaces - Use RegExp.exec() instead of String.match() - Fix keyword spacing for catch
- Remove space after catch - Remove trailing spaces
- Reuse single execAsync instance for both dotnet --info and uname -m - Remove duplicate import statements and setup code - Cleaner, more maintainable implementation
ssomayyajula
approved these changes
Sep 9, 2025
ssomayyajula
left a comment
ssomayyajula
left a comment
There was a problem hiding this comment.
Trusting the process on this one
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
2 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 Analysis
The previous fix (#543) attempted to solve architecture detection issues by using system architecture, but root cause analysis reveals the real problem:
Confirmed user system:
uname -mreturnsarm64lipo -archs /usr/local/bin/dotnetreturnsx86_64RID: osx-x64- running under Rosetta translationhave 'arm64', need 'x86_64'What was happening:
incompatible architectureerrorRoot Cause
The issue isn't system architecture detection - it's that .NET can run under Rosetta translation on ARM64 Macs. When this happens:
Solution
Detect .NET runtime architecture instead of system architecture:
dotnet --infoto get actual .NET runtime informationosx-x64vsosx-arm64x64vsArm64os.arch()Why This Fixes The Issue
This addresses the actual compatibility requirement: Dafny binaries must match .NET runtime architecture, not system hardware architecture.
Confirmed Fix
With the user's confirmed data (
RID: osx-x64), this fix will:osx-x64fromdotnet --infooutputx64architecturedafny-4.11.0-x64-macos-13.zipinstead ofdafny-4.11.0-arm64-macos-13.zipTesting
The fix includes comprehensive logging to help debug architecture detection issues and verify the correct architecture is being selected.
Supersedes #543 with the correct approach based on root cause analysis.