mirror of
https://github.com/Z3Prover/z3
synced 2026-08-02 04:03:26 +00:00
d49c389a69
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>
312 lines
13 KiB
YAML
312 lines
13 KiB
YAML
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=false"
|
||
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"
|
||
required: false
|
||
default: "--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery"
|
||
fstar_run_tests:
|
||
description: "Run the FStar test suite (make test) after the build"
|
||
required: false
|
||
default: "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=false' }}
|
||
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 || '--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery' }}
|
||
FSTAR_RUN_TESTS: ${{ github.event.inputs.fstar_run_tests || 'true' }}
|
||
DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
|
||
steps:
|
||
- name: Checkout Z3
|
||
uses: actions/checkout@v7.0.1
|
||
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
|
||
id: build_fstar
|
||
continue-on-error: true
|
||
run: |
|
||
set -euo pipefail
|
||
rm -rf /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
|
||
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)" -k
|
||
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: Run FStar test suite
|
||
id: test_fstar
|
||
if: env.FSTAR_RUN_TESTS == 'true' && steps.build_fstar.outcome == 'success'
|
||
continue-on-error: true
|
||
run: |
|
||
set -euo pipefail
|
||
cd /tmp/gh-aw/agent/FStar
|
||
eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")"
|
||
|
||
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')"; exit 1; }
|
||
|
||
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)" -k test 2>&1 | tee /tmp/gh-aw/agent/fstar-test.log
|
||
|
||
- name: Collect generated SMT2 files
|
||
id: collect_smt2
|
||
if: always()
|
||
run: |
|
||
set -euo pipefail
|
||
rm -rf /tmp/gh-aw/agent/smt2-artifact
|
||
mkdir -p /tmp/gh-aw/agent/smt2-artifact
|
||
SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
|
||
SMT2_HEAD_LINES=1000
|
||
> "$SMT2_PREVIEW"
|
||
|
||
if [ -d /tmp/gh-aw/agent/FStar ]; then
|
||
mapfile -t SMT2_FILES < <(find /tmp/gh-aw/agent/FStar -type f -name '*.smt2' | sort)
|
||
else
|
||
SMT2_FILES=()
|
||
fi
|
||
|
||
if [ "${#SMT2_FILES[@]}" -eq 0 ]; then
|
||
echo "has_files=false" >> "$GITHUB_OUTPUT"
|
||
exit 0
|
||
fi
|
||
|
||
for file in "${SMT2_FILES[@]}"; do
|
||
rel="${file#/tmp/gh-aw/agent/FStar/}"
|
||
target="/tmp/gh-aw/agent/smt2-artifact/${rel}"
|
||
mkdir -p "$(dirname "$target")"
|
||
cp "$file" "$target"
|
||
{
|
||
printf '#### `%s`\n\n' "$rel"
|
||
printf '```smt2\n'
|
||
head -n "$SMT2_HEAD_LINES" "$file"
|
||
printf '\n```\n\n'
|
||
} >> "$SMT2_PREVIEW"
|
||
done
|
||
|
||
echo "has_files=true" >> "$GITHUB_OUTPUT"
|
||
|
||
- name: Upload generated SMT2 artifact
|
||
id: upload_smt2
|
||
if: always() && steps.collect_smt2.outputs.has_files == 'true'
|
||
uses: actions/upload-artifact@v7
|
||
with:
|
||
name: fstar-generated-smt2-${{ github.run_id }}
|
||
path: /tmp/gh-aw/agent/smt2-artifact
|
||
if-no-files-found: error
|
||
retention-days: 7
|
||
|
||
- name: Create discussion summary
|
||
if: always()
|
||
uses: actions/github-script@v9
|
||
env:
|
||
RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
|
||
FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
|
||
FSTAR_TEST_OUTCOME: ${{ steps.test_fstar.outcome }}
|
||
SMT2_ARTIFACT_ID: ${{ steps.upload_smt2.outputs.artifact-id }}
|
||
with:
|
||
script: |
|
||
const fs = require('fs');
|
||
|
||
const readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null;
|
||
const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown';
|
||
const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? '';
|
||
const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
|
||
const fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? '';
|
||
const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown';
|
||
const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown';
|
||
const fstarBuildSucceeded = fstarBuildOutcome === 'success';
|
||
const fstarStatus = fstarBuildSucceeded
|
||
? '✅ FStar build completed'
|
||
: `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`;
|
||
const fstarTestOutcome = process.env.FSTAR_TEST_OUTCOME || 'skipped';
|
||
const fstarTestStatus = fstarTestOutcome === 'success'
|
||
? '✅ FStar test suite (`make test`) passed'
|
||
: fstarTestOutcome === 'skipped'
|
||
? 'ℹ️ FStar test suite (`make test`) skipped'
|
||
: `⚠️ FStar test suite (\`make test\`) ${fstarTestOutcome} (pipeline continued)`;
|
||
const testLog = readIfExists('/tmp/gh-aw/agent/fstar-test.log') ?? '';
|
||
const maxTestLogChars = 8000;
|
||
let testLogTail = testLog ? testLog.split('\n').slice(-200).join('\n') : '';
|
||
if (testLogTail.length > maxTestLogChars) {
|
||
testLogTail = `... (truncated)\n${testLogTail.slice(-maxTestLogChars)}`;
|
||
}
|
||
const testSection = testLog
|
||
? [
|
||
`### FStar test suite (last 200 log lines)`,
|
||
``,
|
||
'```',
|
||
testLogTail,
|
||
'```'
|
||
].join('\n')
|
||
: '';
|
||
const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim();
|
||
const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : '';
|
||
const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md';
|
||
const maxPreviewChars = 45000; // Keep below GitHub's 65536-character discussion body limit, leaving room for the test log tail and other sections.
|
||
let smt2Preview = readIfExists(smt2PreviewFile) ?? '';
|
||
const smt2PreviewChars = Array.from(smt2Preview);
|
||
if (smt2PreviewChars.length > maxPreviewChars) {
|
||
smt2Preview = `${smt2PreviewChars.slice(0, maxPreviewChars).join('')}\n\n... (truncated due to discussion size limits)`;
|
||
}
|
||
const smt2Section = smt2ArtifactId
|
||
? [
|
||
`### Generated SMT2 files`,
|
||
`- Artifact: ${smt2ArtifactUrl}`,
|
||
``,
|
||
`First 1000 lines per generated \`.smt2\` file:`,
|
||
``,
|
||
smt2Preview || '_No preview content available._'
|
||
].join('\n')
|
||
: [
|
||
`### Generated SMT2 files`,
|
||
`- No generated \`.smt2\` files were found.`
|
||
].join('\n');
|
||
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`,
|
||
`- ${fstarStatus}`,
|
||
`- ${fstarTestStatus}`,
|
||
``,
|
||
`### 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}\``,
|
||
`- fstar_run_tests: \`${process.env.FSTAR_RUN_TESTS}\``,
|
||
``,
|
||
`### Produced versions`,
|
||
`- Z3: \`${z3VersionText}\``,
|
||
`- FStar: \`${fstarVersionText}\``,
|
||
`- FStar commit: \`${fstarCommit}\``,
|
||
``,
|
||
smt2Section,
|
||
``,
|
||
testSection,
|
||
``,
|
||
`### 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
|
||
}
|
||
);
|