The `build-and-report` workflow failed in `build-and-report` because
FStar was invoked with a default `OTHERFLAGS` value containing
`--smt.ho_matching true`, which current FStar no longer recognizes. This
change removes that default while keeping the input configurable for
manual runs.
- **Root cause**
- Workflow default `fstar_otherflags` was set to `--smt.ho_matching
true`.
- During `make`, FStar exited with `error: unrecognized option
'--smt.ho_matching'` (job `79905082893`).
- **Workflow changes**
- Updated `.github/workflows/fstar-master-build.yml`:
- `workflow_dispatch.inputs.fstar_otherflags.default` changed from
`--smt.ho_matching true` to `""`.
- Job env fallback `FSTAR_OTHERFLAGS` changed from `--smt.ho_matching
true` to `""`.
- Removed the outdated option example from the `fstar_otherflags` input
description.
- **Resulting behavior**
- Default scheduled/manual workflow runs no longer pass unsupported
FStar flags.
- Custom flags can still be provided via `fstar_otherflags` when needed.
```yaml
fstar_otherflags:
description: "Extra FStar OTHERFLAGS"
required: false
default: ""
# ...
FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '' }}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Build FStar master with Z3 master` workflow was failing because
FStar's `karamel` submodule was not present after a shallow clone,
causing `make` to abort immediately.
## Change
- Added `--recurse-submodules` to the `git clone` call for FStar in
`.github/workflows/fstar-master-build.yml`
```diff
-git clone --depth=1 --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
+git clone --depth=1 --recurse-submodules --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
```
Failing run:
https://github.com/Z3Prover/z3/actions/runs/27072072789/job/79903014692
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This change replaces the existing agentic workflow with a standard
GitHub Actions workflow that builds Z3 and then builds FStar against
that Z3. The workflow remains parameterized for both toolchains and
supports exercising `smt.ho_matching` via configurable Z3 runtime args
and FStar `OTHERFLAGS`.
- **Workflow migration (agentic → standard)**
- Replaced `.github/workflows/fstar-master-build.md` + `.lock.yml` with
a single native workflow: `.github/workflows/fstar-master-build.yml`.
- Removed dependency on agentic frontmatter, safe-outputs, and
runtime-import flow.
- **Configurable build inputs**
- Added `workflow_dispatch` inputs for:
- `z3_ref`, `z3_cmake_args`, `z3_runtime_args`
- `fstar_ref`, `fstar_opam_switch`, `fstar_otherflags`
- `discussion_category`
- Defaults preserve the requested ho-matching exercise path:
- `z3_runtime_args: smt.ho_matching=true`
- `fstar_otherflags: --smt.ho_matching true`
- **Build and integration flow**
- Builds Z3 from configured ref in `build/release` with CMake+Ninja.
- Clones/builds FStar from configured ref, wiring it to the just-built
Z3 (including version override and PATH aliases expected by FStar).
- **Discussion reporting without agents**
- Adds an `actions/github-script` step that:
- resolves discussion category ID by name,
- posts a summary discussion with inputs, produced versions, commit, and
workflow run URL.
- **Failure diagnostics hardening**
- Added explicit failure messages for missing parsed Z3 version and
missing FStar executable.
- Added defensive handling when parsing generated version text.
```yaml
on:
workflow_dispatch:
inputs:
z3_runtime_args:
default: "smt.ho_matching=true"
fstar_otherflags:
default: "--smt.ho_matching true"
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
