Commit ef51aa0
authored
Fix architecture detection by using .NET runtime architecture instead of system architecture (#544)
## 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:**
- Hardware: ARM64 Mac (M1/M2) - `uname -m` returns `arm64`
- .NET Binary: x86_64 - `lipo -archs /usr/local/bin/dotnet` returns
`x86_64`
- .NET Runtime: `RID: osx-x64` - running under Rosetta translation
- Error: `have 'arm64', need 'x86_64'`
**What was happening:**
1. Extension detected ARM64 system → downloaded ARM64 Dafny binaries
2. .NET runtime was x64 (Rosetta) → tried to load ARM64 libraries
3. Architecture mismatch → `incompatible architecture` error
## Root Cause
The issue isn't system architecture detection - it's that **.NET can run
under Rosetta translation** on ARM64 Macs. When this happens:
- System architecture: ARM64
- .NET runtime architecture: x64
- **We need x64 Dafny binaries, not ARM64**
## Solution
**Detect .NET runtime architecture instead of system architecture:**
1. **Use `dotnet --info`** to get actual .NET runtime information
2. **Parse RID (Runtime Identifier):** `osx-x64` vs `osx-arm64`
3. **Parse Architecture field:** `x64` vs `Arm64`
4. **Download matching Dafny binaries** for the .NET runtime
architecture
5. **Fallback chain:** .NET detection → system detection → `os.arch()`
## Why This Fixes The Issue
- **ARM64 Mac + Native .NET:** Downloads ARM64 Dafny ✅
- **ARM64 Mac + Rosetta .NET:** Downloads x64 Dafny ✅
- **x64 Mac:** Downloads x64 Dafny ✅
- **Other platforms:** Unchanged behavior ✅
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:
1. Parse `osx-x64` from `dotnet --info` output
2. Extract `x64` architecture
3. Download `dafny-4.11.0-x64-macos-13.zip` instead of
`dafny-4.11.0-arm64-macos-13.zip`
4. Resolve the architecture mismatch error
## Testing
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.1 parent 7c7e219 commit ef51aa0
1 file changed
+33
-8
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
126 | 126 | | |
127 | 127 | | |
128 | 128 | | |
129 | | - | |
| 129 | + | |
130 | 130 | | |
131 | 131 | | |
132 | 132 | | |
133 | | - | |
| 133 | + | |
134 | 134 | | |
135 | | - | |
136 | | - | |
| 135 | + | |
| 136 | + | |
137 | 137 | | |
138 | 138 | | |
139 | 139 | | |
140 | 140 | | |
141 | | - | |
142 | | - | |
| 141 | + | |
| 142 | + | |
| 143 | + | |
| 144 | + | |
| 145 | + | |
| 146 | + | |
| 147 | + | |
| 148 | + | |
| 149 | + | |
| 150 | + | |
| 151 | + | |
| 152 | + | |
| 153 | + | |
| 154 | + | |
| 155 | + | |
| 156 | + | |
| 157 | + | |
| 158 | + | |
| 159 | + | |
| 160 | + | |
| 161 | + | |
| 162 | + | |
| 163 | + | |
| 164 | + | |
| 165 | + | |
| 166 | + | |
| 167 | + | |
143 | 168 | | |
144 | 169 | | |
145 | | - | |
146 | | - | |
| 170 | + | |
147 | 171 | | |
148 | 172 | | |
149 | 173 | | |
150 | 174 | | |
| 175 | + | |
151 | 176 | | |
152 | 177 | | |
153 | 178 | | |
| |||
0 commit comments