From b93c782b32ec63cba09b4ccd978037f75d583e8a Mon Sep 17 00:00:00 2001 From: Shailendra Singh Date: Wed, 22 Jul 2026 09:28:33 -0700 Subject: [PATCH] fix(windows): avoid rate-limited Z3 source lookup Signed-off-by: Shailendra Singh Signed-off-by: Akber Raza --- .../build-openshell-mxc-windows/SKILL.md | 6 ++ .../build-openshell-mxc-windows/reference.md | 11 +++ architecture/windows-msvc-build.md | 8 +- tasks/scripts/windows-msvc.ps1 | 82 +++++++++++++++++++ 4 files changed, 106 insertions(+), 1 deletion(-) diff --git a/.agents/skills/build-openshell-mxc-windows/SKILL.md b/.agents/skills/build-openshell-mxc-windows/SKILL.md index 0defc1fbf..f1965c50f 100644 --- a/.agents/skills/build-openshell-mxc-windows/SKILL.md +++ b/.agents/skills/build-openshell-mxc-windows/SKILL.md @@ -60,6 +60,7 @@ The skill reads these environment variables (PowerShell syntax): | `$env:OPENSHELL_WXC_EXEC_PATH` | unset | Optional path to `wxc-exec.exe`. Validated for existence and architecture match only. Not used in this build-only skill. | | `$env:OPENSHELL_MXC_SKIP_ARM64` | `0` | Set to `1` to skip aarch64 build (e.g., for fast x64-only iterations). | | `$env:OPENSHELL_MXC_FORK_BRANCH` | `windows-mxc-build` | Branch name created in the fork. | +| `$env:Z3_SYS_BUNDLED_DIR_OVERRIDE` | pinned source cached under `CARGO_TARGET_DIR` | Reuse an existing Z3 source tree containing `src/api/z3.h`; otherwise the wrapper fetches and caches the pinned revision automatically. | ## Workflow @@ -195,6 +196,11 @@ The PowerShell wrapper must: Use `mise run --skip-tools windows:*` in GitHub Actions and local Windows automation. `--skip-tools` is intentional: this repo should not ask mise to install Rust on Windows because the MSVC flow relies on rustup plus Visual Studio Build Tools. +For bundled Z3, the wrapper fetches the revision pinned by `z3-sys` through +Git, caches it under `CARGO_TARGET_DIR`, and sets +`Z3_SYS_BUNDLED_DIR_OVERRIDE`. This bypasses the unauthenticated GitHub +Contents API lookup that can fail with HTTP 403 on shared networks. + ### Step 6: mise check on x86_64-pc-windows-msvc ```powershell diff --git a/.agents/skills/build-openshell-mxc-windows/reference.md b/.agents/skills/build-openshell-mxc-windows/reference.md index 433162dc3..8768f8970 100644 --- a/.agents/skills/build-openshell-mxc-windows/reference.md +++ b/.agents/skills/build-openshell-mxc-windows/reference.md @@ -78,6 +78,12 @@ Same pattern — gate with `#[cfg(unix)]`. `libsecret` only works on Linux. If `openshell-providers` pulls it in, gate it. The build-only skill does not need credential storage on Windows; that is a follow-on skill. +### Bundled Z3 fails with HTTP 403 + +The wrapper should fetch the pinned Z3 revision through Git before Cargo starts. +If that prefetch fails, inspect the reported partial checkout and verify that +Git can reach `https://github.com/Z3Prover/z3.git`. + ## Cfg gating patterns ### Module-level @@ -181,6 +187,11 @@ native MSVC `cl.exe` with Ninja. Use a short `CARGO_TARGET_DIR` if Windows path-length limits are reached. Test tasks reject a target that does not match the Windows host architecture. +Bundled Z3 source is pinned by revision, fetched through Git, and cached under +`CARGO_TARGET_DIR`. The wrapper sets `Z3_SYS_BUNDLED_DIR_OVERRIDE` so `z3-sys` +does not make an unauthenticated GitHub Contents API call. An explicit override +must point to a source tree containing `src/api/z3.h`. + ## What NOT to do in this skill - Do not implement named-pipe IPC. Stubs only. (Belongs to the follow-on MXC driver skill.) diff --git a/architecture/windows-msvc-build.md b/architecture/windows-msvc-build.md index fa0e2a54e..3049555da 100644 --- a/architecture/windows-msvc-build.md +++ b/architecture/windows-msvc-build.md @@ -64,7 +64,13 @@ an ARM64 test result is native coverage rather than x64 emulation coverage. By default it enables bundled Z3 for reproducible Windows builds. When `Z3_LIBRARY_PATH_OVERRIDE` points at a directory containing `libz3.lib`, the wrapper uses that system Z3 instead and requires `Z3_SYS_Z3_HEADER` to point at -the full path to `z3.h`. +the full path to `z3.h`. For bundled builds, the wrapper fetches the Z3 source +revision pinned by `z3-sys` through Git, caches it under `CARGO_TARGET_DIR`, and +sets `Z3_SYS_BUNDLED_DIR_OVERRIDE`. This avoids the unauthenticated GitHub API +lookup in the `z3-sys` build script, which can fail with HTTP 403 when a shared +runner or developer network exhausts its API rate limit. An explicitly set +`Z3_SYS_BUNDLED_DIR_OVERRIDE` remains supported and must contain +`src/api/z3.h`. The lane uses `mise run --skip-tools windows:*` because Windows Rust comes from rustup and linking comes from Visual Studio Build Tools. Mise orchestrates the diff --git a/tasks/scripts/windows-msvc.ps1 b/tasks/scripts/windows-msvc.ps1 index e0cb0ecbe..c27e4f4bd 100644 --- a/tasks/scripts/windows-msvc.ps1 +++ b/tasks/scripts/windows-msvc.ps1 @@ -40,6 +40,10 @@ if ([string]::IsNullOrWhiteSpace($TargetDir)) { $UnsupportedDriverPackageExcludes = "--exclude openshell-driver-docker --exclude openshell-driver-kubernetes --exclude openshell-driver-podman --exclude openshell-driver-vm" $BundledZ3WorkspaceFeatures = "--features openshell-prover/bundled-z3" $BundledZ3ServerFeatures = "--features openshell-server/bundled-z3,openshell-prover/bundled-z3" +$BundledZ3Repository = "https://github.com/Z3Prover/z3.git" +$BundledZ3SysVersion = "0.10.9" +# This is the matching z3-sys submodule revision. Update both pins together. +$BundledZ3Revision = "ddb49568d3520e99799e364fb22f35fc67d887b1" $Z3WorkspaceFeatures = $BundledZ3WorkspaceFeatures $Z3ServerFeatures = $BundledZ3ServerFeatures @@ -330,9 +334,87 @@ function Resolve-Z3HeaderPath([string] $HeaderPath) { return (Resolve-Path $HeaderPath).Path } +function Assert-BundledZ3Source([string] $SourcePath, [string] $ExpectedRevision) { + if (-not (Test-Path $SourcePath -PathType Container)) { + throw "Bundled Z3 source directory does not exist: $SourcePath" + } + + $header = Join-Path $SourcePath "src\api\z3.h" + if (-not (Test-Path $header -PathType Leaf)) { + throw "Bundled Z3 source directory does not contain src\api\z3.h: $SourcePath" + } + + if (-not [string]::IsNullOrWhiteSpace($ExpectedRevision)) { + $actualRevision = (& git -C $SourcePath rev-parse HEAD 2>$null) + if ($LASTEXITCODE -ne 0 -or [string]::IsNullOrWhiteSpace($actualRevision)) { + throw "Could not verify the bundled Z3 source revision at: $SourcePath" + } + if ($actualRevision.Trim() -ne $ExpectedRevision) { + throw "Bundled Z3 source revision mismatch at ${SourcePath}: expected $ExpectedRevision, found $($actualRevision.Trim())" + } + } + + return (Resolve-Path $SourcePath).Path +} + +function Resolve-BundledZ3Source { + if (-not [string]::IsNullOrWhiteSpace($env:Z3_SYS_BUNDLED_DIR_OVERRIDE)) { + return Assert-BundledZ3Source $env:Z3_SYS_BUNDLED_DIR_OVERRIDE "" + } + + $cargoLock = Get-Content (Join-Path $RepoRoot "Cargo.lock") -Raw + $packagePattern = '(?ms)^\[\[package\]\]\s+name = "z3-sys"\s+version = "([^"]+)"' + $packageMatches = [regex]::Matches($cargoLock, $packagePattern) + if ($packageMatches.Count -ne 1 -or $packageMatches[0].Groups[1].Value -ne $BundledZ3SysVersion) { + throw "Bundled Z3 source pin expects z3-sys $BundledZ3SysVersion. Update the version and revision pins for the z3-sys version in Cargo.lock." + } + + $revisionPrefix = $BundledZ3Revision.Substring(0, 12) + $sourcePath = Join-Path $TargetDir "z3-source-$revisionPrefix" + if (Test-Path $sourcePath) { + return Assert-BundledZ3Source $sourcePath $BundledZ3Revision + } + + if (-not (Get-Command git.exe -ErrorAction SilentlyContinue)) { + throw "Bundled Z3 source preparation requires git.exe on PATH." + } + if (-not (Test-Path $TargetDir -PathType Container)) { + New-Item -ItemType Directory -Force -Path $TargetDir | Out-Null + } + + $stagingPath = "$sourcePath.partial-$([guid]::NewGuid().ToString('N'))" + Write-Host "==> Fetching bundled Z3 source" + Write-Host " repository: $BundledZ3Repository" + Write-Host " revision: $BundledZ3Revision" + Write-Host " cache: $sourcePath" + + & git init --quiet $stagingPath + if ($LASTEXITCODE -ne 0) { + throw "git init failed while preparing bundled Z3 source at: $stagingPath" + } + & git -C $stagingPath remote add origin $BundledZ3Repository + if ($LASTEXITCODE -ne 0) { + throw "git remote add failed while preparing bundled Z3 source at: $stagingPath" + } + & git -C $stagingPath fetch --quiet --depth 1 origin $BundledZ3Revision + if ($LASTEXITCODE -ne 0) { + throw "git fetch failed for bundled Z3 revision $BundledZ3Revision. Partial source remains at: $stagingPath" + } + & git -C $stagingPath checkout --quiet --detach FETCH_HEAD + if ($LASTEXITCODE -ne 0) { + throw "git checkout failed for bundled Z3 revision $BundledZ3Revision. Partial source remains at: $stagingPath" + } + + Assert-BundledZ3Source $stagingPath $BundledZ3Revision | Out-Null + Move-Item -Path $stagingPath -Destination $sourcePath + return Assert-BundledZ3Source $sourcePath $BundledZ3Revision +} + function Configure-Z3 { if ([string]::IsNullOrWhiteSpace($env:Z3_LIBRARY_PATH_OVERRIDE)) { Write-Host "==> Z3: bundled" + $env:Z3_SYS_BUNDLED_DIR_OVERRIDE = Resolve-BundledZ3Source + Write-Host " Z3_SYS_BUNDLED_DIR_OVERRIDE=$env:Z3_SYS_BUNDLED_DIR_OVERRIDE" return [pscustomobject]@{ WorkspaceFeatures = $BundledZ3WorkspaceFeatures ServerFeatures = $BundledZ3ServerFeatures