From 60ae0a81b74d738c9103bee2cdfa9b140167f6d3 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 12:44:11 -0700 Subject: [PATCH] Replace agentic F* build pipeline with standard GitHub Actions workflow (#9745) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- .github/workflows/fstar-master-build.yml | 185 +++++++++++++++++++++++ 1 file changed, 185 insertions(+) create mode 100644 .github/workflows/fstar-master-build.yml diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml new file mode 100644 index 000000000..64a9ee89b --- /dev/null +++ b/.github/workflows/fstar-master-build.yml @@ -0,0 +1,185 @@ +name: Build FStar master with Z3 master + +on: + schedule: + - cron: "9 4 * * *" + workflow_dispatch: + inputs: + z3_ref: + description: Z3 ref to checkout and build + required: false + default: master + z3_cmake_args: + description: Extra CMake arguments for Z3 build + required: false + default: "" + z3_runtime_args: + description: "Extra Z3 runtime args (example: smt.ho_matching=true)" + required: false + default: "smt.ho_matching=true" + fstar_ref: + description: FStar ref to checkout and build + required: false + default: master + fstar_opam_switch: + description: OCaml switch for FStar build + required: false + default: "4.14.2" + fstar_otherflags: + description: "Extra FStar OTHERFLAGS (example: --smt.ho_matching true)" + required: false + default: "--smt.ho_matching true" + discussion_category: + description: Discussion category name + required: false + default: "Agentic Workflows" + +permissions: + contents: read + discussions: write + +concurrency: + group: ${{ github.workflow }} + cancel-in-progress: false + +jobs: + build-and-report: + runs-on: ubuntu-latest + timeout-minutes: 180 + env: + Z3_REF: ${{ github.event.inputs.z3_ref || 'master' }} + Z3_CMAKE_ARGS: ${{ github.event.inputs.z3_cmake_args || '' }} + Z3_RUNTIME_ARGS: ${{ github.event.inputs.z3_runtime_args || 'smt.ho_matching=true' }} + FSTAR_REF: ${{ github.event.inputs.fstar_ref || 'master' }} + FSTAR_OPAM_SWITCH: ${{ github.event.inputs.fstar_opam_switch || '4.14.2' }} + FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '--smt.ho_matching true' }} + DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }} + steps: + - name: Checkout Z3 + uses: actions/checkout@v6.0.3 + with: + ref: ${{ env.Z3_REF }} + fetch-depth: 1 + + - name: Install dependencies + run: | + set -euo pipefail + sudo apt-get update -y + sudo apt-get install -y cmake ninja-build python3 git curl unzip opam m4 pkg-config libgmp-dev + + - name: Build Z3 + run: | + set -euo pipefail + mkdir -p /tmp/gh-aw/agent + cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release $Z3_CMAKE_ARGS + ninja -C build/release z3 + ./build/release/z3 --version | tee /tmp/gh-aw/agent/z3-version.txt + printf '(check-sat)\n' | ./build/release/z3 $Z3_RUNTIME_ARGS -in | tee /tmp/gh-aw/agent/z3-runtime-check.txt + + - name: Prepare Z3 aliases for FStar + run: | + set -euo pipefail + mkdir -p /tmp/gh-aw/agent/z3-bin + ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3 + ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.8.5 + ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.13.3 + /tmp/gh-aw/agent/z3-bin/z3 --version + + - name: Build FStar + run: | + set -euo pipefail + rm -rf /tmp/gh-aw/agent/FStar + git clone --depth=1 --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar + cd /tmp/gh-aw/agent/FStar + echo "FStar commit: $(git rev-parse HEAD)" | tee /tmp/gh-aw/agent/fstar-commit.txt + + opam init --disable-sandboxing --yes + opam switch create "$FSTAR_OPAM_SWITCH" --yes || opam switch "$FSTAR_OPAM_SWITCH" + eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")" + opam install --deps-only . --yes + + Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)" + test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; cat /tmp/gh-aw/agent/z3-version.txt || true; exit 1; } + + PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)" + test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; } + /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt + + - name: Create discussion summary + uses: actions/github-script@v9 + env: + RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }} + with: + script: | + const fs = require('fs'); + + const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim(); + const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim(); + const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown'; + const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim(); + const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, ''); + const date = new Date().toISOString().slice(0, 10); + + const owner = context.repo.owner; + const repo = context.repo.repo; + const categoryName = process.env.DISCUSSION_CATEGORY; + + const categoryQuery = await github.graphql( + `query($owner:String!, $repo:String!) { + repository(owner:$owner, name:$repo) { + id + discussionCategories(first:50) { + nodes { id name } + } + } + }`, + { owner, repo } + ); + + const categories = categoryQuery.repository.discussionCategories.nodes || []; + const normalized = categoryName.trim().toLowerCase(); + const category = categories.find(c => c.name.toLowerCase() === normalized); + if (!category) { + throw new Error(`Discussion category '${categoryName}' not found`); + } + + const body = [ + `### Build status`, + `- ✅ Z3 build completed`, + `- ✅ FStar build completed`, + ``, + `### Inputs used`, + `- z3_ref: \`${process.env.Z3_REF}\``, + `- z3_cmake_args: \`${process.env.Z3_CMAKE_ARGS}\``, + `- z3_runtime_args: \`${process.env.Z3_RUNTIME_ARGS}\``, + `- fstar_ref: \`${process.env.FSTAR_REF}\``, + `- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``, + `- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``, + ``, + `### Produced versions`, + `- Z3: \`${z3VersionText}\``, + `- FStar: \`${fstarVersionText}\``, + `- FStar commit: \`${fstarCommit}\``, + ``, + `### Run`, + `- Workflow run: ${process.env.RUN_URL}` + ].join('\n'); + + await github.graphql( + `mutation($repositoryId:ID!, $categoryId:ID!, $title:String!, $body:String!) { + createDiscussion(input:{ + repositoryId:$repositoryId, + categoryId:$categoryId, + title:$title, + body:$body + }) { + discussion { url } + } + }`, + { + repositoryId: categoryQuery.repository.id, + categoryId: category.id, + title: `FStar build with configurable Z3 inputs — ${date}`, + body + } + );