fix(windows): harden shared Z3 source cache

Signed-off-by: Shailendra Singh <shailendras@nvidia.com>
This commit is contained in:
Shailendra Singh
2026-08-05 20:16:24 -05:00
committed by Akber Raza
parent 011ceab794
commit 53dc33738e
3 changed files with 54 additions and 15 deletions
@@ -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
+10 -6
View File
@@ -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
+37 -5
View File
@@ -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
}