From 53dc33738eeb8406ca04346ca586ea04e0d41247 Mon Sep 17 00:00:00 2001 From: Shailendra Singh Date: Thu, 23 Jul 2026 12:12:40 -0700 Subject: [PATCH] fix(windows): harden shared Z3 source cache Signed-off-by: Shailendra Singh --- .../build-openshell-mxc-windows/SKILL.md | 11 +++-- architecture/windows-msvc-build.md | 16 ++++--- tasks/scripts/windows-msvc.ps1 | 42 ++++++++++++++++--- 3 files changed, 54 insertions(+), 15 deletions(-) diff --git a/.agents/skills/build-openshell-mxc-windows/SKILL.md b/.agents/skills/build-openshell-mxc-windows/SKILL.md index 0bd2ab447..264d85d92 100644 --- a/.agents/skills/build-openshell-mxc-windows/SKILL.md +++ b/.agents/skills/build-openshell-mxc-windows/SKILL.md @@ -60,7 +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. | +| `$env:Z3_SYS_BUNDLED_DIR_OVERRIDE` | pinned source cached under `CARGO_TARGET_DIR` when explicit, otherwise `%LOCALAPPDATA%\OpenShell\cache\z3` | Reuse an existing Z3 source tree containing `src/api/z3.h`; otherwise the wrapper fetches and caches the pinned revision automatically. | ## Workflow @@ -197,9 +197,12 @@ 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. +Git and sets `Z3_SYS_BUNDLED_DIR_OVERRIDE`. It caches under an explicitly +configured `CARGO_TARGET_DIR`, or under the current user's local application +data directory when Cargo uses its default target tree. Concurrent commands +publish the validated source through an atomic directory rename so x64 and +ARM64 validation can share the cache safely. This bypasses the unauthenticated +GitHub Contents API lookup that can fail with HTTP 403 on shared networks. The repository-wide `mise run pre-commit` task is supported on Windows. `tasks/rust.toml` and `tasks/test.toml` route compiler-bearing checks through diff --git a/architecture/windows-msvc-build.md b/architecture/windows-msvc-build.md index 863198088..19719b3cc 100644 --- a/architecture/windows-msvc-build.md +++ b/architecture/windows-msvc-build.md @@ -76,12 +76,16 @@ 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`. 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`. +revision pinned by `z3-sys` through Git and sets +`Z3_SYS_BUNDLED_DIR_OVERRIDE`. When `CARGO_TARGET_DIR` is explicit, the wrapper +uses it for the source cache. Otherwise, it caches under the current user's +local application data directory, outside the checkout. Publishing uses an +atomic directory rename so concurrent x64 and ARM64 commands can share the +cache safely. This keeps downloaded sources outside the checkout by default and +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 1ef311a98..fc265b684 100644 --- a/tasks/scripts/windows-msvc.ps1 +++ b/tasks/scripts/windows-msvc.ps1 @@ -32,11 +32,24 @@ if (-not (Test-Path $LogDir)) { } $LogDir = (Resolve-Path $LogDir).Path +$TargetDirWasConfigured = -not [string]::IsNullOrWhiteSpace($env:CARGO_TARGET_DIR) $TargetDir = $env:CARGO_TARGET_DIR -if ([string]::IsNullOrWhiteSpace($TargetDir)) { +if (-not $TargetDirWasConfigured) { $TargetDir = Join-Path $RepoRoot "target" } +$BundledZ3CacheRoot = $TargetDir +if (-not $TargetDirWasConfigured) { + $userCacheRoot = [Environment]::GetFolderPath([Environment+SpecialFolder]::LocalApplicationData) + if ([string]::IsNullOrWhiteSpace($userCacheRoot)) { + $userCacheRoot = $env:LOCALAPPDATA + } + if ([string]::IsNullOrWhiteSpace($userCacheRoot)) { + $userCacheRoot = [IO.Path]::GetTempPath() + } + $BundledZ3CacheRoot = Join-Path $userCacheRoot "OpenShell\cache\z3" +} + $BuildJobsValue = $env:OPENSHELL_WINDOWS_BUILD_JOBS if ([string]::IsNullOrWhiteSpace($BuildJobsValue)) { $BuildJobsValue = $env:CARGO_BUILD_JOBS @@ -358,7 +371,7 @@ function Resolve-BundledZ3Source { } $revisionPrefix = $BundledZ3Revision.Substring(0, 12) - $sourcePath = Join-Path $TargetDir "z3-source-$revisionPrefix" + $sourcePath = Join-Path $BundledZ3CacheRoot "z3-source-$revisionPrefix" if (Test-Path $sourcePath) { return Assert-BundledZ3Source $sourcePath $BundledZ3Revision } @@ -366,8 +379,8 @@ function Resolve-BundledZ3Source { 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 + if (-not (Test-Path $BundledZ3CacheRoot -PathType Container)) { + New-Item -ItemType Directory -Force -Path $BundledZ3CacheRoot | Out-Null } $stagingPath = "$sourcePath.partial-$([guid]::NewGuid().ToString('N'))" @@ -394,7 +407,26 @@ function Resolve-BundledZ3Source { } Assert-BundledZ3Source $stagingPath $BundledZ3Revision | Out-Null - Move-Item -Path $stagingPath -Destination $sourcePath + try { + # Directory.Move is an atomic rename on the same volume and, unlike + # Move-Item, fails when the destination already exists. A concurrent + # x64/ARM64 invocation can therefore win publication without the loser + # nesting its staging directory inside the shared cache. + [IO.Directory]::Move($stagingPath, $sourcePath) + } catch { + if (-not (Test-Path $sourcePath -PathType Container)) { + throw + } + Write-Host "==> Reusing bundled Z3 source published by another process" + } finally { + if (Test-Path $stagingPath -PathType Container) { + try { + Remove-Item -LiteralPath $stagingPath -Recurse -Force + } catch { + Write-Warning "Could not remove redundant bundled Z3 staging directory: $stagingPath" + } + } + } return Assert-BundledZ3Source $sourcePath $BundledZ3Revision }