mirror of
https://github.com/Z3Prover/z3
synced 2026-08-09 23:42:21 +00:00
249778137d
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>
415 lines
18 KiB
YAML
415 lines
18 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
|
||
|
||
# Scheduled runs receive no workflow_dispatch inputs, so the effective F* options
|
||
# come from the hard-wired env defaults above. Resolve them once here, and make sure
|
||
# the options that cause F* to emit .smt2 files are always present: without them the
|
||
# build and the test suite fail without leaving any query behind to analyse.
|
||
- name: Resolve FStar options
|
||
run: |
|
||
set -euo pipefail
|
||
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; }
|
||
|
||
OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS"
|
||
case " $OTHERFLAGS " in
|
||
*" --log_failing_queries "*) ;;
|
||
*) OTHERFLAGS="$OTHERFLAGS --log_failing_queries" ;;
|
||
esac
|
||
|
||
echo "FSTAR_EFFECTIVE_OTHERFLAGS=$OTHERFLAGS" >> "$GITHUB_ENV"
|
||
printf '%s\n' "$OTHERFLAGS" | tee /tmp/gh-aw/agent/fstar-otherflags.txt
|
||
|
||
- 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
|
||
|
||
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="$FSTAR_EFFECTIVE_OTHERFLAGS" make -j"$(nproc)" -k 2>&1 | tee /tmp/gh-aw/agent/fstar-build.log
|
||
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")"
|
||
|
||
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="$FSTAR_EFFECTIVE_OTHERFLAGS" make -j"$(nproc)" -k test 2>&1 | tee /tmp/gh-aw/agent/fstar-test.log
|
||
|
||
# Collect everything needed to triage a failure offline: the logs, the failing SMT2
|
||
# queries, and - for every expected-output test - the produced output, the .expected
|
||
# oracle and a unified diff between them. Test suite failures otherwise leave nothing
|
||
# behind, since only .smt2 files used to be uploaded.
|
||
- name: Collect FStar failure artifacts
|
||
id: collect_artifacts
|
||
if: always()
|
||
run: |
|
||
set -euo pipefail
|
||
FSTAR_DIR=/tmp/gh-aw/agent/FStar
|
||
OUT=/tmp/gh-aw/agent/fstar-artifact
|
||
rm -rf "$OUT"
|
||
mkdir -p "$OUT/logs" "$OUT/smt2" "$OUT/test-output"
|
||
|
||
for name in z3-version.txt z3-runtime-check.txt fstar-version.txt fstar-commit.txt fstar-otherflags.txt fstar-build.log fstar-test.log; do
|
||
if [ -f "/tmp/gh-aw/agent/$name" ]; then
|
||
cp "/tmp/gh-aw/agent/$name" "$OUT/logs/$name"
|
||
fi
|
||
done
|
||
|
||
SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
|
||
SMT2_HEAD_LINES=1000
|
||
: > "$SMT2_PREVIEW"
|
||
|
||
MISMATCH_LIST="$OUT/logs/mismatched-outputs.txt"
|
||
: > "$MISMATCH_LIST"
|
||
SMT2_COUNT=0
|
||
MISMATCH_COUNT=0
|
||
|
||
if [ -d "$FSTAR_DIR" ]; then
|
||
while IFS= read -r file; do
|
||
rel="${file#"$FSTAR_DIR"/}"
|
||
target="$OUT/smt2/${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"
|
||
SMT2_COUNT=$((SMT2_COUNT + 1))
|
||
done < <(find "$FSTAR_DIR" -type f -name '*.smt2' | sort)
|
||
|
||
# An expected-output test compares <dir>/_output/<name> with <dir>/<name>.expected.
|
||
while IFS= read -r file; do
|
||
expected="$(dirname "$(dirname "$file")")/$(basename "$file").expected"
|
||
[ -f "$expected" ] || continue
|
||
if cmp -s "$file" "$expected"; then continue; fi
|
||
|
||
rel="${file#"$FSTAR_DIR"/}"
|
||
target="$OUT/test-output/${rel}"
|
||
mkdir -p "$(dirname "$target")"
|
||
cp "$file" "$target.actual"
|
||
cp "$expected" "$target.expected"
|
||
diff -u "$expected" "$file" > "$target.diff" || true
|
||
printf '%s\n' "$rel" >> "$MISMATCH_LIST"
|
||
MISMATCH_COUNT=$((MISMATCH_COUNT + 1))
|
||
done < <(find "$FSTAR_DIR" -type f -path '*/_output/*' -size -4M \
|
||
\( -name '*.output' -o -name '*.json_output' -o -name '*.ideout' -o -name '*.out' \
|
||
-o -name '*.fs-out' -o -name '*.err' -o -name '*.ml' -o -name '*.fs' -o -name '*.krml' \) | sort)
|
||
fi
|
||
|
||
FAILING="$OUT/logs/failing-tests.txt"
|
||
{
|
||
printf 'Mismatched expected outputs: %s\n' "$MISMATCH_COUNT"
|
||
sed 's/^/ /' "$MISMATCH_LIST"
|
||
printf '\nFailed make targets:\n'
|
||
for log in /tmp/gh-aw/agent/fstar-build.log /tmp/gh-aw/agent/fstar-test.log; do
|
||
[ -f "$log" ] || continue
|
||
grep -oE 'make(\[[0-9]+\])?: \*\*\* \[[^]]*\] Error [0-9]+' "$log" || true
|
||
done | sed -E 's/.*\[([^]]*)\] Error [0-9]+$/ \1/' | sort -u
|
||
} > "$FAILING"
|
||
|
||
{
|
||
echo "smt2_count=$SMT2_COUNT"
|
||
echo "mismatch_count=$MISMATCH_COUNT"
|
||
} >> "$GITHUB_OUTPUT"
|
||
|
||
echo "Collected $SMT2_COUNT .smt2 file(s) and $MISMATCH_COUNT mismatched test output(s)."
|
||
cat "$FAILING"
|
||
|
||
- name: Upload FStar failure artifacts
|
||
id: upload_artifacts
|
||
if: always()
|
||
uses: actions/upload-artifact@v7
|
||
with:
|
||
name: fstar-artifacts-${{ github.run_id }}
|
||
path: /tmp/gh-aw/agent/fstar-artifact
|
||
if-no-files-found: warn
|
||
retention-days: 7
|
||
|
||
- name: Job summary
|
||
if: always()
|
||
env:
|
||
BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
|
||
TEST_OUTCOME: ${{ steps.test_fstar.outcome }}
|
||
SMT2_COUNT: ${{ steps.collect_artifacts.outputs.smt2_count }}
|
||
MISMATCH_COUNT: ${{ steps.collect_artifacts.outputs.mismatch_count }}
|
||
run: |
|
||
set -euo pipefail
|
||
{
|
||
echo "## FStar master build"
|
||
echo
|
||
echo "- FStar build: \`${BUILD_OUTCOME:-unknown}\`"
|
||
echo "- FStar test suite: \`${TEST_OUTCOME:-skipped}\`"
|
||
echo "- Effective OTHERFLAGS: \`$(cat /tmp/gh-aw/agent/fstar-otherflags.txt 2>/dev/null || echo unknown)\`"
|
||
echo "- Logged failing queries: ${SMT2_COUNT:-unknown}"
|
||
echo "- Mismatched expected outputs: ${MISMATCH_COUNT:-unknown}"
|
||
echo
|
||
if [ -f /tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt ]; then
|
||
echo '<details><summary>Failing tests</summary>'
|
||
echo
|
||
echo '```'
|
||
head -c 40000 /tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt
|
||
echo '```'
|
||
echo
|
||
echo '</details>'
|
||
fi
|
||
} >> "$GITHUB_STEP_SUMMARY"
|
||
|
||
- 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_artifacts.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 failingTests = readIfExists('/tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt') ?? '';
|
||
const maxFailingChars = 6000;
|
||
const failingSection = [
|
||
`### Failing tests`,
|
||
``,
|
||
'```',
|
||
failingTests
|
||
? (failingTests.length > maxFailingChars
|
||
? `${failingTests.slice(0, maxFailingChars)}\n... (truncated, see artifact logs/failing-tests.txt)`
|
||
: failingTests)
|
||
: 'No failure summary was produced.',
|
||
'```'
|
||
].join('\n');
|
||
const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md';
|
||
const maxPreviewChars = 38000; // Keep below GitHub's 65536-character discussion body limit, leaving room for the failure summary, 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 (logs, failing \`.smt2\` queries, and mismatched test outputs with diffs): ${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}\``,
|
||
`- effective OTHERFLAGS: \`${readIfExists('/tmp/gh-aw/agent/fstar-otherflags.txt') ?? 'unknown'}\``,
|
||
``,
|
||
`### Produced versions`,
|
||
`- Z3: \`${z3VersionText}\``,
|
||
`- FStar: \`${fstarVersionText}\``,
|
||
`- FStar commit: \`${fstarCommit}\``,
|
||
``,
|
||
failingSection,
|
||
``,
|
||
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
|
||
}
|
||
);
|