This PR substantially modernizes Z3's CMake build, replacing a
significant amount of hand-rolled dependency bookkeeping with CMake's
native target-graph features.
The main benefits are:
* **Less custom build logic.** The existing component system in
`cmake/z3_add_component.cmake` manually walks and records the
component-dependency graph. This PR moves that information onto CMake
targets themselves, eliminating much of the `Z3_COMPONENT_*` /
`Z3_DEPENDENT_*` variable machinery.
* **A more accurate target graph.** Component dependencies, generated
registration headers, and static-component linking are now modeled
directly in CMake rather than reconstructed separately.
* **More natural source-tree organization.** `add_subdirectory()` calls
no longer need to be kept in a global topological order or reach deeply
into the source tree. Forward component dependencies are allowed, so
each directory can add its own children in a natural, alphabetical
order.
* **Better dependency propagation.** External dependencies such as GMP,
Threads, and `atomic` are available to the components that actually need
them. In particular, non-system GMP installations now work correctly
because component targets can see GMP's include path.
* **Cleaner package consumption.** Build-only compiler/linker policy is
separated from the dependencies exported to static-package consumers,
and Z3 behaves more cleanly when included via `add_subdirectory()` or
`FetchContent`.
* **Less code with the same observable package behavior.** The PR
changes 34 files with +566/-902 lines, for a net reduction of roughly
336 lines, while preserving the existing targets, public headers,
install layout, and registration behavior.
The main enabler is raising the minimum CMake version from 3.16 to
**3.30**.
CMake 3.30 introduced **custom transitive properties**, which let
targets propagate the registered module headers, tactic headers, and
memory headers needed for generated registration code. This replaces the
custom graph-walking logic previously used to accumulate those headers.
As a result, the three functions `z3_add_install_tactic_rule`,
`z3_add_memory_initializer_rule`, and
`z3_add_gparams_register_modules_rule` are replaced by a single,
substantially simpler function, `z3_generate_registration`, which
generates the required headers from properties propagated through the
target graph.
Newer CMake also lets us model chains of `OBJECT` libraries correctly.
Historically, only `OBJECT` libraries named directly in
`target_link_libraries()` contributed their object files to the final
link, which made transitive static-component dependencies awkward to
represent. Using `INTERFACE_LINK_LIBRARIES_DIRECT`, those chains can now
be expressed directly in the target graph.
Every Z3 component also links to a new `INTERFACE` target, `z3_common`.
This target owns the external library dependencies that consumers of a
component may need, including GMP, Threads, `atomic`, and similar
dependencies. Previously, these dependencies were attached only to the
final `libz3` target; among other things, that meant individual
components could not see the include path for a non-system GMP
installation.
`z3_common` is exported for static-package consumers, but Z3's own build
policy is not. Internal compiler and linker flags now live on a separate
`z3_internal_options` target used throughout the build. A possible
follow-up is to replace `z3_internal_options` with toolchain files
and/or CMake presets, but that would be a more disruptive change and is
intentionally left out of this PR.
Once CMake itself has an accurate model of the component graph, several
pieces of surrounding machinery become unnecessary. We no longer need a
topologically sorted list of `add_subdirectory()` calls or the previous
requirement that child components be declared before their dependents.
Each directory now adds its own subdirectories, in alphabetical order.
Public headers are likewise installed through CMake file sets instead of
hand-written `install(FILES ...)` rules.
The CMake version bump also enables a few smaller cleanups:
* use `GENERATOR_IS_MULTI_CONFIG` instead of inferring that from whether
`CMAKE_CONFIGURATION_TYPES` is defined;
* use `PROJECT_IS_TOP_LEVEL` guards so Z3 behaves correctly when
consumed as a subdirectory or through `FetchContent`;
* use `block()` instead of manually saving and restoring state around
the Python `find_package()` call.
One unrelated fix is included alongside these changes: the .NET example
now stages its `csproj` and `Program.cs` into the build tree with
`add_custom_command()` rather than `configure_file(..., COPYONLY)`, so
the `dotnet` build target correctly notices source changes.
Overall, the PR moves responsibility for dependency propagation and
graph structure out of Z3's custom CMake code and back into CMake
itself. The result is a smaller build system with fewer ordering
constraints and less duplicated state, while keeping the package's
externally visible behavior unchanged.
These are the last of the changes I have that are compatible with 3.16.
There are a few things here:
1. A small correction to the resolution chain from #10717 plus a test.
The package is now more permissive when only `BUILD_SHARED_LIBS` is set.
2. Use the `SHELL:` argument form to `target_link_options` in emscripten
to avoid dropping `-s` flags.
3. Use CMake's native IPO support rather than hand-rolled detection.
After this, I will open a large PR that bumps the minimum version to
3.30 and reworks the `z3_add_component` function. It will remove 300+
lines of CMake code.
The old pkg-config files didn't support relocation, which makes
packaging difficult. They also didn't support static linking. This PR
fixes both issues by referencing by computing a prefix relative to
`${pcfiledir}` and adding `.private` metadata to `z3.pc`.
In #10717 we enhanced the CMake package to support multiple build
configurations, so that Z3 could be installed and consumed as either a
static or shared package, or both side by side. This PR dog-foods that
work: the Python bindings and the example projects now consume Z3
through the same installed CMake package that external users rely on,
rather than through separate in-tree plumbing.
To make that possible, we introduce a `z3::libz3` ALIAS that mirrors the
installed target in-tree. In-tree consumers (like the examples and the
Python bindings) and out-of-tree consumers of the installed package now
refer to Z3 the same way, so now there's one blessed interface. The
examples and package-consumer test were updated accordingly, both to
exercise this path and to serve as a model for how downstream projects
should consume Z3 going forward.
Finally, we add test coverage for the reworked Python build, including a
CI job that installs a shared build of libz3 and then builds the Python
bindings against that installed package, confirming the Python-only
build path works end to end.
A common pitfall with CMake is that declaring `cmake_minimum_required`
does not guarantee compatibility with the stated version. The reason is
that it's a _backwards-compatibility_ setting, not a
_forwards-compatibility_ one. For instance, you can set
`cmake_minimum_required(VERSION 3.16)` and then use a generator
expression introduced in a newer version, and it will silently break
compatibility with 3.16. Newer versions can run builds authored with
older versions, but not vice versa. Therefore, one must test the build
with the stated version in CI to ensure compatibility.
This PR adds a workflow to test package building at the promised minimum
(currently 3.16) and consuming at the consumer minimum (via
`find_package`, currently 3.5). It also tests the shared and static
package variants to ensure the loading logic is correct.
I had wanted to add this to #10717 but it was merged too quickly 🙂
The "activation" job (and any other job depending on it) failed across
multiple gh-aw generated workflows with:
```
Unable to resolve action `github/gh-aw-actions@v0.83.4`, unable to find version `v0.83.4`
```
## Root cause
- Compiled `.lock.yml` workflows pin `github/gh-aw-actions/setup` to the
same version as the `gh-aw` CLI that generated them (`v0.83.4`).
- The `gh-aw` CLI release `v0.83.4` exists, but the companion
`github/gh-aw-actions` repo never published a matching `v0.83.4` tag (or
`v0.83.3`) — its `0.83.x` series stops at `v0.83.2`. Confirmed via
GitHub API (404 on the tag ref).
- This release-train mismatch broke action resolution at job start for
every workflow compiled at that CLI version.
## Fix
- Repointed the `github/gh-aw-actions/setup` reference from the
non-existent `v0.83.4` to the latest tag that actually exists,
`v0.83.2`, across all 13 affected generated lock files (manifest
comment, header comment, and every `uses:` step):
- `a3-python.lock.yml`, `academic-citation-tracker.lock.yml`,
`api-coherence-checker.lock.yml`, `code-conventions-analyzer.lock.yml`,
`code-simplifier.lock.yml`, `compare-stats-anomaly-reporter.lock.yml`,
`csa-analysis.lock.yml`, `issue-backlog-processor.lock.yml`,
`memory-safety-report.lock.yml`, `release-notes-updater.lock.yml`,
`smtlib-benchmark-finder.lock.yml`, `tactic-to-simplifier.lock.yml`,
`workflow-suggestion-agent.lock.yml`
- Scoped the change to the broken action reference only, avoiding a full
recompile with a newer `gh-aw` CLI, which would have pulled in unrelated
formatting/schema churn.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
The memory-safety report generator was unable to parse ASan/UBSan
findings in some runs because artifact download via MCP was
policy-filtered in the report environment. This change makes artifact
access deterministic for `workflow_run` by downloading artifacts
directly in the workflow and keeping MCP download only as fallback.
- **Workflow artifact access path (lock workflow)**
- Added a `Download triggering workflow artifacts` step to
`memory-safety-report.lock.yml` in the agent job.
- For `workflow_run`, it pulls artifacts from the triggering run into
`/tmp/reports` using `actions/download-artifact` with explicit token
usage.
- Keeps `continue-on-error: true` so the report flow can still proceed
to fallback paths.
- **Report prompt behavior (authoring workflow)**
- Updated `memory-safety-report.md` instructions to:
- Parse `/tmp/reports` first when pre-downloaded artifacts exist.
- Use MCP `download_workflow_run_artifact` only when `/tmp/reports` is
absent (e.g., manual dispatch).
- **Resulting execution model**
- `workflow_run`: local artifact parse path is primary.
- `workflow_dispatch` / missing local artifacts: MCP URL path remains
available.
```yaml
- name: Download triggering workflow artifacts
if: github.event_name == 'workflow_run' && github.event.workflow_run.id != ''
continue-on-error: true
uses: actions/download-artifact@v8
with:
github-token: ${{ github.token }}
repository: ${{ github.repository }}
run-id: ${{ github.event.workflow_run.id }}
path: /tmp/reports
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10640
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
## Summary
- remove the deleted F* `--split_queries on_failure` option
- remove the obsolete `higher_order_smt` extension knob
- retain supported `--log_failing_queries` and `--proof_recovery`
diagnostics
## Root cause
F* commit `5a88fc509` removed `--split_queries` because proof goals are
now split unconditionally. Dependency generation rejected the option, so
`.dependfstarc` was never created; the subsequent missing-file Make
errors were cascading symptoms.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
- add `install()` rules for the CMake-built OCaml bindings so `cmake
--install` stages the OCaml package instead of only building it in
`build/src/api/ml`
- install the OCaml package metadata/modules into `lib/ocaml/z3`,
install `dllz3ml.so` into `lib/ocaml/stublibs`, and install the native
`z3ml.a` archive alongside `libz3ml.a`
- on macOS, update the installed stub library so it keeps its
`@rpath/libz3.<major>.<minor>.dylib` dependency and gains an
`@loader_path/../../` rpath that resolves the installed `libz3` from the
stublibs directory
- extend `.github/workflows/ocaml.yaml` to run `cmake --install`, verify
the staged artifacts, and compile/run the OCaml example against the
installed tree on Ubuntu and macOS
## Root cause
`src/api/ml/CMakeLists.txt` built the OCaml artifacts (`z3ml.cma`,
`z3ml.cmxa`, `z3ml.cmxs`, `dllz3ml.so`, `META`, module interfaces, etc.)
but never installed them. The file also had an abandoned commented-out
macOS fix for the OCaml stub library, so the install path was never
validated in CI.
## Validation
- `ninja -C build test-z3` on Windows with the existing `C:\z3\build`
configuration (`Z3_BUILD_OCAML_BINDINGS=OFF`)
- GitHub Actions `OCaml Binding CI (Ubuntu + macOS)` run:
https://github.com/Z3Prover/z3/actions/runs/31975209612Fixes#7684.
Thanks to @arbipher for the earlier investigation captured in the issue
thread, which helped clarify the packaging/runtime expectations.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Fixes#10375.
## Analysis of [run
30786942559](https://github.com/Z3Prover/z3/actions/runs/30786942559)
The job is green, but `make test` exited 2. Every failing test is an
**expected-output mismatch**, and all 70 of them differ only by the
`--proof_recovery` banner:
```
- The SMT solver could not prove the query.
+ - This query was retried due to the --proof_recovery option, yet it still
+ failed on all attempts.
```
That text comes from `--proof_recovery` in the workflow's own
`fstar_otherflags` default, which F*'s `.expected` files do not carry —
so these are configuration mismatches, not Z3 regressions. There are
also failures that never reach the solver (`hello.__all`, `dune`,
extraction diffs on `RemoveUnusedTypars_B.fs` / `Bug3865.out`).
None of that was reconstructible from the artifact: the run uploaded 526
`.smt2` files, almost all logged failing queries from negative tests
that are *supposed* to fail, and nothing else. No logs, no produced
output, no `.expected` oracle, no diff.
## Changes
* **`Resolve FStar options`** — computes `OTHERFLAGS` once (removing the
duplicated `--z3version` extraction) and enforces
`--log_failing_queries`. Scheduled runs get no `workflow_dispatch`
inputs, so the options that make F* emit `.smt2` files are hard-wired
instead of assumed to come from the inputs. The effective flags are
recorded in the artifact, the job summary and the discussion.
* **`Build FStar`** now tees to a log, as the test step already did.
* **`Collect FStar failure artifacts`** replaces `Collect generated SMT2
files` and produces:
* `logs/` — build log, test log, versions, commit, effective flags, and
a `failing-tests.txt` summary of mismatched outputs plus failed make
targets;
* `smt2/` — the logged failing queries, as before;
* `test-output/` — for every expected-output test whose result differs
from its oracle: `<name>.actual`, `<name>.expected` and a unified
`<name>.diff`.
* **Upload always runs.** Previously, if no `.smt2` file existed the
collect step short-circuited and the upload was skipped, so the hardest
failures produced no artifact at all.
* The failure summary is surfaced in the **job summary** and in the
**discussion**, so a mismatch is visible without downloading anything.
Applied to the run above, `test-output/` would hold the
actual/expected/diff triple for each of the 70 mismatches and
`failing-tests.txt` would list them alongside `hello.__all` and the
other non-SMT failures.
## Validation
The workflow parses as YAML; every `run:` block passes `bash -n` and the
`github-script` body passes `node --check`. The new steps were executed
locally against a fixture reproducing the run's failure shapes:
* mismatched `.output` / `.json_output` / `.ideout` / `.fs` / `.out`
files are collected with correct diffs; the generated diff for
`Basic.fst.output` reproduces the annotation in the run exactly;
* matching outputs, `_output` files with no `.expected`, and files over
4 MB are correctly skipped;
* failed make targets are parsed from both logs;
* with no F* tree at all (build failed before clone) the collector still
exits 0 and the artifact still contains the logs;
* option resolution was checked with the default flags, with
`--log_failing_queries` absent, with empty flags, and with an
unparseable `z3 --version`;
* the rendered discussion body is 53 040 characters in the worst case,
below GitHub's 65 536 limit.
Behaviour deliberately unchanged: the build and test steps keep
`continue-on-error`, so a broken F* master still does not block the
report.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The nightly release failed because the default `GITHUB_TOKEN` is a
GitHub Actions App installation token without permission to create a tag
that includes workflow changes.
- Mint a short-lived installation token for `z3prover-ci-bot`.
- Request only `contents: write` and `workflows: write`.
- Use the App token for checkout credentials, tag deletion/push, and
release deletion/creation.
- Do not use `GH_AW_GITHUB_TOKEN`, a PAT, or another classic token.
Repository setup:
- `Z3_CI_APP_CLIENT_ID` is configured on `Z3Prover/z3`.
- Add `Z3_CI_APP_PRIVATE_KEY` as an Actions repository secret.
- Grant `z3prover-ci-bot` **Workflows: Read and write**, then approve
the updated installation permissions for the Z3Prover organization.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The clang-tidy warning fixer depended on
`download_workflow_run_artifact` to fetch the warning report from the
producer workflow. That path is blocked here, so the fixer could
discover the run but not access the warning contents it needs to
analyze.
- **Fixer input path**
- Update
`/home/runner/work/z3/z3/.github/workflows/build-warning-fixer.md` to
consume the triggering run via `list_workflow_jobs` + `get_job_logs`
- Remove the artifact-download flow from the workflow instructions
- Parse warning and status data from the build job log, with a grep
fallback if the structured summary is missing
- **Producer log contract**
- Update
`/home/runner/work/z3/z3/.github/workflows/clang-tidy-warning-report.yml`
to emit a stable, marker-delimited summary block at the end of the build
job log
- Include both build status and the extracted warning subset in that
block
- Leave artifact upload in place as optional output rather than a
required dependency
- **Workflow behavior**
- Make the fixer operate entirely from Actions logs, avoiding cross-run
artifact retrieval as part of its primary path
- Preserve the existing warning extraction model while shifting the
producer/consumer contract to log output
Example of the emitted log shape:
```text
CLANG_TIDY_WARNING_REPORT_BEGIN
CLANG_TIDY_STATUS_BEGIN
configure_status=0
build_status=0
CLANG_TIDY_STATUS_END
CLANG_TIDY_WARNINGS_BEGIN
123: warning: ...
CLANG_TIDY_WARNINGS_END
CLANG_TIDY_WARNING_REPORT_END
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates the Clang-Tidy Warning Fixer to run after
`clang-tidy-warning-report.yml` completes, consume that run’s warning
artifacts, and produce assignment-ready fix proposals as GitHub issues.
It replaces the previous self-build/PR-creation flow with
artifact-driven analysis and diff-first issue output.
- **Trigger + execution model**
- Switched workflow trigger from scheduled standalone runs to
`workflow_run` on **Clang-Tidy Warning Report** completion (with manual
dispatch retained).
- Keeps fixer analysis scoped to diagnostics from the originating report
run.
- **Artifact-driven diagnostics input**
- Removed in-fixer prebuild/clang-tidy compilation step.
- Updated agent instructions to resolve source run ID, list/download the
warning artifact, extract logs, and analyze
`warnings.txt`/`combined.log` from that artifact.
- **Output contract: PR → Issue**
- Replaced safe output target from `create-pull-request` to
`create-issue`.
- Issue content now requires:
- warning summary,
- skipped-warning rationale,
- proposed fixes as full unified diffs,
- assignment-ready checklist entries.
- **Workflow/runtime alignment**
- Regenerated lockfile to match source workflow changes.
- Added Actions toolset/permissions needed for run/artifact retrieval in
the agent runtime.
```yaml
on:
workflow_run:
workflows: ["Clang-Tidy Warning Report"]
types: [completed]
branches: [master]
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Build Z3 with clang-tidy warnings` job was failing before
compilation due to an invalid `cmake --build` invocation. The workflow
passed a Ninja-only flag directly to CMake, so the job exited with
`Unknown argument -k` instead of producing the intended warning report.
- **Root cause**
- The workflow invoked:
```bash
cmake --build build --target shell test-z3 -k 0
```
- `-k 0` is a native Ninja argument and must be forwarded through CMake
after `--`.
- **Change**
- Update the clang-tidy warning workflow to pass native build-tool
arguments correctly:
```bash
cmake --build build --target shell test-z3 -- -k 0
```
- **Effect**
- The job can now reach the actual Ninja build instead of failing in
CMake argument parsing.
- This restores the intended behavior of collecting clang-tidy/build
diagnostics in the workflow artifact.
- **Files**
- `.github/workflows/clang-tidy-warning-report.yml`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Adds a scheduled workflow to build Z3 with the clang-tidy warning
configuration being tracked in detlefs' PRs, including the latest
`-Wgnu-anonymous-struct` flag from #10345. The workflow persists all
emitted warnings as an artifact so warning regressions can be reviewed
from each run.
- **Workflow**
- Adds `.github/workflows/clang-tidy-warning-report.yml`
- Runs daily and on manual dispatch
- Uses Ubuntu + CMake/Ninja with `clang` and `clang-tidy`
- **Warning coverage**
- Reuses the repository's existing Clang warning setup
- Layers in the current pending detlefs warning flag:
- `-Wgnu-anonymous-struct`
- **Artifacts**
- Captures:
- `configure.log`
- `build.log`
- `combined.log`
- `warnings.txt`
- `status.txt`
- Uploads them as a per-run artifact for inspection
- **Failure behavior**
- Still uploads logs on failure
- Marks the workflow failed if configure or build fails, so broken
clang-tidy runs are visible in Actions
```yaml
CC=clang CXX=clang++ cmake -GNinja -S . -B build \
-DCMAKE_BUILD_TYPE=Debug \
-DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
-DCMAKE_CXX_CLANG_TIDY=clang-tidy \
-DCMAKE_CXX_FLAGS="-Wgnu-anonymous-struct"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `agent` job in the Clang-Tidy Warning Fixer workflow was spending
most of its runtime waiting on a full clang-tidy build, then failing
before it could complete its safe-output path. This change narrows the
prompt so the agent can make a bounded decision from early diagnostics
instead of treating the full build as a prerequisite.
- **Prompt guardrail**
- Add a runtime-budget section to the compiled workflow prompt in
`build-warning-fixer.lock.yml`.
- Instruct the agent to stop after it has enough diagnostics for one
safe fix, or after 15 minutes.
- **Build scope reduction**
- Switch initial diagnostic collection to a `shell`-only build.
- Explicitly avoid waiting for a full `shell + test-z3` clang-tidy build
before deciding whether to act.
- **Fallback behavior**
- Direct the agent to emit `noop` when it cannot reach a safe, validated
fix within the time budget.
- Keep `test-z3` optional unless it is already available or cheap to
build within the remaining budget.
Example of the new prompt guidance:
```yaml
- Use `cmake --build build --target shell -- -k 0 2>&1 | tee /tmp/gh-aw/agent/clang-tidy-build.log` for initial diagnostic collection.
- Do not wait for the full `shell` build to finish before deciding what to do.
- Stop once you have enough diagnostics for one small, high-confidence fix, or after 15 minutes.
- If no safe fix is ready in that budget, call `noop`.
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This updates the existing agentic workflow from generic build-warning
cleanup to a clang-tidy-based loop: compile Z3 with Clang, inspect
clang-tidy/compiler diagnostics, and open a PR only for small,
semantics-preserving fixes.
- **Workflow scope**
- Renames and repurposes `build-warning-fixer` as a clang-tidy warning
fixer.
- Keeps the existing agentic PR flow, but narrows it to clang/clang-tidy
findings from the current run.
- **Build/analyze path**
- Switches the authored workflow prompt to use the repo’s CMake + Ninja
build with `clang`/`clang++`.
- Enables `CMAKE_CXX_CLANG_TIDY=clang-tidy` and exports compile commands
for tool-driven analysis.
- Captures configure/build logs in the agent artifact directory for
post-run diagnosis.
- **Agent behavior**
- Instructs the agent to classify clang-tidy warnings, compiler
warnings, and build errors from the build log.
- Biases toward localized fixes only: e.g. `override`,
`[[maybe_unused]]`, `nullptr`, dead locals.
- Explicitly prefers `noop` over speculative edits when diagnostics are
broad, risky, or design-affecting.
- **Generated workflow**
- Regenerates the compiled lockfile to reflect the new prompt and
current auth/permission model used by other agentic workflows in this
repo.
```yaml
CC=clang CXX=clang++ cmake -GNinja -S . -B build \
-DCMAKE_BUILD_TYPE=Debug \
-DCMAKE_EXPORT_COMPILE_COMMANDS=ON \
-DCMAKE_CXX_CLANG_TIDY=clang-tidy \
2>&1 | tee /tmp/gh-aw/agent/clang-tidy-configure.log
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This addresses stale generated Agentic Workflow artifacts by recompiling
the workflow sources and updating the checked-in lock outputs. The
update brings lockfiles and shared action pin metadata back in sync with
the current compiler/runtime generation.
- **Scope of regeneration**
- Recompiled all Agentic Workflow markdown definitions in
`.github/workflows/*.md` into their corresponding `.lock.yml` outputs.
- Updated generated maintenance workflow output in
`.github/workflows/agentics-maintenance.yml`.
- **Pinned dependency/metadata refresh**
- Refreshed `.github/aw/actions-lock.json` and lockfile manifests
(actions, container digests, compiler metadata) to the latest generated
state.
- Resulting lock headers now reflect the current compiler/toolchain
metadata used for generation.
- **Auth/runtime shape in generated lockfiles**
- Regenerated lock outputs include current AW-generated runtime/env
wiring for Copilot execution paths and token handling where applicable.
```yaml
# Example (lockfile header after regeneration)
# gh-aw-metadata:
# compiler_version: "v0.83.4"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Bumps [actions/cache/save](https://github.com/actions/cache) from 5.0.5
to 6.1.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/releases">actions/cache/save's
releases</a>.</em></p>
<blockquote>
<h2>v6.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1768">actions/cache#1768</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v6...v6.1.0">https://github.com/actions/cache/compare/v6...v6.1.0</a></p>
<h2>v6.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update packages, migrate to ESM by <a
href="https://github.com/Samirat"><code>@Samirat</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1760">actions/cache#1760</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v6.0.0">https://github.com/actions/cache/compare/v5...v6.0.0</a></p>
<h2>v5.1.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Bump <code>@actions/cache</code> to v5.1.0 - handle read-only cache
access by <a
href="https://github.com/jasongin"><code>@jasongin</code></a> in <a
href="https://redirect.github.com/actions/cache/pull/1775">actions/cache#1775</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/cache/compare/v5...v5.1.0">https://github.com/actions/cache/compare/v5...v5.1.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/cache/blob/main/RELEASES.md">actions/cache/save's
changelog</a>.</em></p>
<blockquote>
<h1>Releases</h1>
<h2>How to prepare a release</h2>
<blockquote>
<p>[!NOTE]
Relevant for maintainers with write access only.</p>
</blockquote>
<ol>
<li>Switch to a new branch from <code>main</code>.</li>
<li>Run <code>npm test</code> to ensure all tests are passing.</li>
<li>Update the version in <a
href="https://github.com/actions/cache/blob/main/package.json"><code>https://github.com/actions/cache/blob/main/package.json</code></a>.</li>
<li>Run <code>npm run build</code> to update the compiled files.</li>
<li>Update this <a
href="https://github.com/actions/cache/blob/main/RELEASES.md"><code>https://github.com/actions/cache/blob/main/RELEASES.md</code></a>
with the new version and changes in the <code>## Changelog</code>
section.</li>
<li>Run <code>licensed cache</code> to update the license report.</li>
<li>Run <code>licensed status</code> and resolve any warnings by
updating the <a
href="https://github.com/actions/cache/blob/main/.licensed.yml"><code>https://github.com/actions/cache/blob/main/.licensed.yml</code></a>
file with the exceptions.</li>
<li>Commit your changes and push your branch upstream.</li>
<li>Open a pull request against <code>main</code> and get it reviewed
and merged.</li>
<li>Draft a new release <a
href="https://github.com/actions/cache/releases">https://github.com/actions/cache/releases</a>
use the same version number used in <code>package.json</code>
<ol>
<li>Create a new tag with the version number.</li>
<li>Auto generate release notes and update them to match the changes you
made in <code>RELEASES.md</code>.</li>
<li>Toggle the set as the latest release option.</li>
<li>Publish the release.</li>
</ol>
</li>
<li>Navigate to <a
href="https://github.com/actions/cache/actions/workflows/release-new-action-version.yml">https://github.com/actions/cache/actions/workflows/release-new-action-version.yml</a>
<ol>
<li>There should be a workflow run queued with the same version
number.</li>
<li>Approve the run to publish the new version and update the major tags
for this action.</li>
</ol>
</li>
</ol>
<h2>Changelog</h2>
<h3>6.1.0</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v6.1.0 to pick up <a
href="https://redirect.github.com/actions/toolkit/pull/2435">actions/toolkit#2435
Handle cache write error due to read-only token</a></li>
<li>Switch redundant "Cache save failed" warning to debug log
in save-only</li>
</ul>
<h3>6.0.0</h3>
<ul>
<li>Updated <code>@actions/cache</code> to ^6.0.1,
<code>@actions/core</code> to ^3.0.1, <code>@actions/exec</code> to
^3.0.0, <code>@actions/io</code> to ^3.0.2</li>
<li>Migrated to ESM module system</li>
<li>Upgraded Jest to v30 and test infrastructure to be ESM
compatible</li>
</ul>
<h3>5.0.4</h3>
<ul>
<li>Bump <code>minimatch</code> to v3.1.5 (fixes ReDoS via globstar
patterns)</li>
<li>Bump <code>undici</code> to v6.24.1 (WebSocket decompression bomb
protection, header validation fixes)</li>
<li>Bump <code>fast-xml-parser</code> to v5.5.6</li>
</ul>
<h3>5.0.3</h3>
<ul>
<li>Bump <code>@actions/cache</code> to v5.0.5 (Resolves: <a
href="https://github.com/actions/cache/security/dependabot/33">https://github.com/actions/cache/security/dependabot/33</a>)</li>
<li>Bump <code>@actions/core</code> to v2.0.3</li>
</ul>
<h3>5.0.2</h3>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="55cc834586"><code>55cc834</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1768">#1768</a>
from jasongin/readonly-cache</li>
<li><a
href="d8cd72f230"><code>d8cd72f</code></a>
Bump <code>@actions/cache</code> to v6.1.0 - handle cache write error
due to RO token</li>
<li><a
href="2c8a9bd745"><code>2c8a9bd</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/cache/issues/1760">#1760</a>
from actions/samirat/esm_migration_and_package_update</li>
<li><a
href="e9b91fdc3f"><code>e9b91fd</code></a>
Prettier fixes</li>
<li><a
href="e4884b8ff7"><code>e4884b8</code></a>
Rebuild dist</li>
<li><a
href="10baf0191a"><code>10baf01</code></a>
Fixed licenses</li>
<li><a
href="e39b386c90"><code>e39b386</code></a>
Fix test mock return order</li>
<li><a
href="b692820337"><code>b692820</code></a>
PR feedback</li>
<li><a
href="60749128a4"><code>6074912</code></a>
Rebuild dist bundles as ESM to match type:module</li>
<li><a
href="5a912e8b4a"><code>5a912e8</code></a>
Fix lint and jest issues</li>
<li>Additional commits viewable in <a
href="27d5ce7f10...55cc834586">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
The tptp5 example was removed, so drop its build/run steps from ci.yml,
coverage.yml, and the daily-test-improver coverage action. The z3 -tptp
front-end and the tptp-benchmark workflow are unaffected.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Build FStar only type-checks the compiler and ulib. Running `make test`
afterwards exercises the tests/examples suite, which sends many more SMT
queries to the freshly built Z3 and produces more logged failing queries
for the existing .smt2 collection step.
The new step runs in the FStar clone with the same opam env, PATH to the
Z3 aliases and OTHERFLAGS as the build. It is gated on a new
fstar_run_tests input (default true) and on the build succeeding, and is
continue-on-error so a test failure does not hide the build result or
skip reporting. The discussion summary reports the test outcome and the
tail of the test log; the SMT2 preview budget is reduced accordingly to
stay below the discussion body size limit.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The COPILOT_GITHUB_TOKEN PAT secret expired, causing HTTP 401 auth
failures in all agentic workflows that referenced it. Switch these
workflows to GitHub Actions token-based Copilot inference by adding
'copilot-requests: write' to their permissions (matching the already-
working code-simplifier and release-notes-updater workflows), so the
engine uses the ephemeral github.token instead of the expired PAT.
Recompiled with gh-aw v0.81.6 (repo's pinned version) to keep the diff
minimal. Affected: api-coherence-checker, issue-backlog-processor,
memory-safety-report, academic-citation-tracker, smtlib-benchmark-finder,
workflow-suggestion-agent, specbot-crash-analyzer, tptp-benchmark.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
The eight remaining README-listed agentic workflows (tptp-benchmark, qf-s-benchmark, smtlib-benchmark-finder, memory-safety-report, issue-backlog-processor, workflow-suggestion-agent, academic-citation-tracker, specbot-crash-analyzer) were failing with HTTP 401 because their agent/detection jobs depended on the missing/expired COPILOT_GITHUB_TOKEN repository secret.
Switch the agent and detection 'Execute Copilot CLI' steps from secrets.COPILOT_GITHUB_TOKEN to the S2STOKENS mechanism (github.token) and grant the required copilot-requests: write permission, matching the fix already applied to api-coherence-checker (#10223), code-simplifier (#10222), and release-notes-updater.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 8abbf1d4-fc99-4c10-ac89-3f0276ec8751
On scheduled runs, `github.event.inputs.*` is empty, so the `||
fallback` values in the `env` block are what actually get used — but two
of them diverged from the declared `workflow_dispatch` input defaults.
## Changes
- `Z3_RUNTIME_ARGS`: scheduled fallback was `smt.ho_matching=true`;
corrected to `smt.ho_matching=false` to match the input default
- `FSTAR_OTHERFLAGS`: scheduled fallback was `''`; corrected to
`--split_queries on_failure --log_failing_queries --ext higher_order_smt
--proof_recovery` to match the input default
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `agent` job in the API Coherence Checker workflow was failing every
run with HTTP 401 because it depended on a `COPILOT_GITHUB_TOKEN`
repository secret that was missing/expired.
## Changes
- **`api-coherence-checker.lock.yml`**: Switch `agent` and `detection`
jobs from legacy `secrets.COPILOT_GITHUB_TOKEN` to the S2STOKENS
mechanism (service-to-service token exchange via the standard
`github.token`):
```yaml
# Before (agent and detection Execute Copilot CLI steps)
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
# no S2STOKENS
# After
COPILOT_GITHUB_TOKEN: ${{ github.token }}
S2STOKENS: true
```
- **Permissions**: Replace broad `permissions: read-all` on the `agent`
job (and add to `detection`) with minimal explicit scopes required for
S2STOKENS:
```yaml
permissions:
contents: read
copilot-requests: write # required for S2STOKENS token exchange
```
This brings `api-coherence-checker` in line with the pattern already
used by `code-simplifier` and `release-notes-updater`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Code Simplifier` workflow’s `agent` job was failing before any
analysis ran because Copilot requests were not authorized in the
workflow context. The generated lock workflow therefore executed against
a stale auth model and consistently hit `HTTP 401` during agent startup.
- **Root cause**
- The workflow frontmatter did not grant `copilot-requests: write`,
which is required for Copilot-backed agent execution in Actions.
- **Workflow change**
- Added `copilot-requests: write` to
`.github/workflows/code-simplifier.md`.
- **Generated workflow update**
- Recompiled `code-simplifier.lock.yml` so the executable workflow
matches the new permission model.
- This updates the Copilot invocation path from the old secret-based
flow to the GitHub Actions token-based flow used by current gh-aw
compilation.
- **Effective delta**
```yaml
permissions:
contents: read
issues: read
pull-requests: read
copilot-requests: write
```
- **Lockfile effect**
```yaml
# before
COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }}
# after
COPILOT_GITHUB_TOKEN: ${{ github.token }}
S2STOKENS: true
```
This keeps the change scoped to the failing workflow while aligning the
checked-in lock file with the auth mechanism expected by the current
Agentic Workflows toolchain.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
MinGW silently ignores `#pragma comment(lib, ...)` (MSVC-only), so
linker errors like missing `dbghelp` symbols go undetected until a
downstream user hits them. No CI coverage existed for MinGW on Windows.
## Changes
- **`.github/workflows/Windows.yml`**: New `mingw-build` job using MSYS2
UCRT64 (`mingw-w64-ucrt-x86_64-gcc`) that builds Z3 via `cmake -G Ninja`
and runs `test-z3 /a`, exercising the full link step under MinGW on
every push/PR to master.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
