mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-28 21:08:43 +00:00
Code Activity

SpecBot: Output to Discussions instead of Pull Requests (#8399)

Browse source 
* Initial plan

* Replace create-pull-request with create-discussion for SpecBot

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-27 13:21:09 -08:00 • committed by GitHub
parent cd5cea9e9c
commit 9ea16e966d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 45 additions and 95 deletions
Download patch file Download diff file Expand all files Collapse all files

25
.github/agentics/specbot.md vendored
View file

@ -202,18 +202,19 @@ int* allocate_buffer(size_t size) {
- Run quick smoke tests if possible
- Note any compilation errors or warnings
### 6. Create Pull Request
### 6. Create Discussion
**PR Structure:**
- Title: `[SpecBot] Add specifications to [ClassName]`
- Use `create-pull-request` safe output
- Set `skip-if-match: 'is:pr is:open in:title "[SpecBot]"'` to avoid duplicates
**Discussion Structure:**
- Title: `Add specifications to [ClassName]`
- Use `create-discussion` safe output
- Category: "Agentic Workflows"
- Previous discussions with same prefix will be automatically closed
**PR Body Template:**
**Discussion Body Template:**
```markdown
## ✨ Automatic Specification Mining
This PR adds formal specifications (class invariants, pre/post-conditions) to improve code correctness and maintainability.
This discussion proposes formal specifications (class invariants, pre/post-conditions) to improve code correctness and maintainability.
### 📋 Classes Annotated
- `ClassName` in `src/path/to/file.cpp`
@ -247,7 +248,7 @@ This PR adds formal specifications (class invariants, pre/post-conditions) to im
- All assertions are guarded by debug macros where appropriate
- Assertions have been validated for correctness
- No behavior changes - only adding checks
- Human review recommended for complex invariants
- Human review and manual implementation recommended for complex invariants
### 📚 Methodology
Specifications synthesized using LLM-based invariant mining inspired by [arXiv:2502.18917](https://arxiv.org/abs/2502.18917).
@ -293,7 +294,7 @@ Specifications synthesized using LLM-based invariant mining inspired by [arXiv:2
## Output Format
### Success Case (specifications added):
Create a PR with annotated code.
Create a discussion documenting the proposed specifications.
### No Changes Case (already well-annotated):
Exit gracefully with a comment explaining why no changes were made:
@ -309,7 +310,7 @@ No additional specifications needed at this time.
```
### Partial Success Case:
Create a PR with whatever specifications could be confidently added, and note any limitations:
Create a discussion documenting whatever specifications could be confidently identified, and note any limitations:
```markdown
### ⚠️ Limitations
Some potential invariants were identified but not added due to:
@ -330,7 +331,7 @@ These can be addressed in future iterations or manual review.
### Incremental Refinement:
- Use cache-memory to track which classes have been analyzed
- Build on previous runs to improve specifications over time
- Learn from PR feedback to refine future annotations
- Learn from discussion feedback to refine future annotations
### Pattern Recognition:
- Common patterns: container invariants, ownership invariants, state machine invariants
@ -349,5 +350,5 @@ These can be addressed in future iterations or manual review.
- If you can't understand a class well enough, skip it and try another
- If compilation fails, investigate and fix assertion syntax
- If you're unsure about an invariant's correctness, document it as a question in PR
- If you're unsure about an invariant's correctness, document it as a question in the discussion
- Always be transparent about confidence levels and limitations

88
.github/workflows/specbot.lock.yml generated vendored
View file

@ -156,32 +156,25 @@ jobs:
mkdir -p /tmp/gh-aw/safeoutputs
mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs
cat > /opt/gh-aw/safeoutputs/config.json << 'EOF'
{"create_missing_tool_issue":{"max":1,"title_prefix":"[missing tool]"},"create_pull_request":{},"missing_data":{},"missing_tool":{},"noop":{"max":1}}
{"create_discussion":{"max":1},"create_missing_tool_issue":{"max":1,"title_prefix":"[missing tool]"},"missing_data":{},"missing_tool":{},"noop":{"max":1}}
EOF
cat > /opt/gh-aw/safeoutputs/tools.json << 'EOF'
[
{
"description": "Create a new GitHub pull request to propose code changes. Use this after making file edits to submit them for review and merging. The PR will be created from the current branch with your committed changes. For code review comments on an existing PR, use create_pull_request_review_comment instead. CONSTRAINTS: Maximum 1 pull request(s) can be created.",
"description": "Create a GitHub discussion for announcements, Q\u0026A, reports, status updates, or community conversations. Use this for content that benefits from threaded replies, doesn't require task tracking, or serves as documentation. For actionable work items that need assignment and status tracking, use create_issue instead. CONSTRAINTS: Maximum 1 discussion(s) can be created. Title will be prefixed with \"[SpecBot] \". Discussions will be created in category \"Agentic Workflows\".",
"inputSchema": {
"additionalProperties": false,
"properties": {
"body": {
"description": "Detailed PR description in Markdown. Include what changes were made, why, testing notes, and any breaking changes. Do NOT repeat the title as a heading.",
"description": "Discussion content in Markdown. Do NOT repeat the title as a heading since it already appears as the discussion's h1. Include all relevant context, findings, or questions.",
"type": "string"
},
"branch": {
"description": "Source branch name containing the changes. If omitted, uses the current working branch.",
"category": {
"description": "Discussion category by name (e.g., 'General'), slug (e.g., 'general'), or ID. If omitted, uses the first available category. Category must exist in the repository.",
"type": "string"
},
"labels": {
"description": "Labels to categorize the PR (e.g., 'enhancement', 'bugfix'). Labels must exist in the repository.",
"items": {
"type": "string"
},
"type": "array"
},
"title": {
"description": "Concise PR title describing the changes. Follow repository conventions (e.g., conventional commits). The title appears as the main heading.",
"description": "Concise discussion title summarizing the topic. The title appears as the main heading, so keep it brief and descriptive.",
"type": "string"
}
},
@ -191,7 +184,7 @@ jobs:
],
"type": "object"
},
"name": "create_pull_request"
"name": "create_discussion"
},
{
"description": "Report that a tool or capability needed to complete the task is not available, or share any information you deem important about missing functionality or limitations. Use this when you cannot accomplish what was requested because the required functionality is missing or access is restricted.",
@ -266,7 +259,7 @@ jobs:
EOF
cat > /opt/gh-aw/safeoutputs/validation.json << 'EOF'
{
"create_pull_request": {
"create_discussion": {
"defaultMax": 1,
"fields": {
"body": {
@ -275,17 +268,14 @@ jobs:
"sanitize": true,
"maxLength": 65000
},
"branch": {
"required": true,
"category": {
"type": "string",
"sanitize": true,
"maxLength": 256
"maxLength": 128
},
"labels": {
"type": "array",
"itemType": "string",
"itemSanitize": true,
"itemMaxLength": 128
"repo": {
"type": "string",
"maxLength": 256
},
"title": {
"required": true,
@ -499,7 +489,7 @@ jobs:
<instructions>
To create or modify GitHub resources (issues, discussions, pull requests, etc.), you MUST call the appropriate safe output tool. Simply writing content will NOT work - the workflow requires actual tool calls.
**Available tools**: create_pull_request, missing_tool, noop
**Available tools**: create_discussion, missing_tool, noop
**Critical**: Tool calls write structured data that downstream jobs process. Without tool calls, follow-up actions will be skipped.
</instructions>
@ -729,7 +719,6 @@ jobs:
/tmp/gh-aw/mcp-logs/
/tmp/gh-aw/sandbox/firewall/logs/
/tmp/gh-aw/agent-stdio.log
/tmp/gh-aw/aw.patch
if-no-files-found: ignore
conclusion:
@ -821,21 +810,6 @@ jobs:
setupGlobals(core, github, context, exec, io);
const { main } = require('/opt/gh-aw/actions/handle_agent_failure.cjs');
await main();
- name: Handle Create Pull Request Error
id: handle_create_pr_error
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
env:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
CREATE_PR_ERROR_MESSAGE: ${{ needs.create_pull_request.outputs.error_message }}
GH_AW_WORKFLOW_NAME: "Specbot"
GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
script: |
const { setupGlobals } = require('/opt/gh-aw/actions/setup_globals.cjs');
setupGlobals(core, github, context, exec, io);
const { main } = require('/opt/gh-aw/actions/handle_create_pr_error.cjs');
await main();
- name: Update reaction comment with completion status
id: conclusion
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
@ -1000,15 +974,13 @@ jobs:
safe_outputs:
needs:
- activation
- agent
- detection
if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (needs.detection.outputs.success == 'true')
runs-on: ubuntu-slim
permissions:
contents: write
issues: write
pull-requests: write
contents: read
discussions: write
timeout-minutes: 15
env:
GH_AW_ENGINE_ID: "copilot"
@ -1033,38 +1005,12 @@ jobs:
mkdir -p /tmp/gh-aw/safeoutputs/
find "/tmp/gh-aw/safeoutputs/" -type f -print
echo "GH_AW_AGENT_OUTPUT=/tmp/gh-aw/safeoutputs/agent_output.json" >> "$GITHUB_ENV"
- name: Download patch artifact
continue-on-error: true
uses: actions/download-artifact@018cc2cf5baa6db3ef3c5f8a56943fffe632ef53 # v6.0.0
with:
name: agent-artifacts
path: /tmp/gh-aw/
- name: Checkout repository
if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (contains(needs.agent.outputs.output_types, 'create_pull_request'))
uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6
with:
token: ${{ github.token }}
persist-credentials: false
fetch-depth: 1
- name: Configure Git credentials
if: ((!cancelled()) && (needs.agent.result != 'skipped')) && (contains(needs.agent.outputs.output_types, 'create_pull_request'))
env:
REPO_NAME: ${{ github.repository }}
SERVER_URL: ${{ github.server_url }}
GIT_TOKEN: ${{ github.token }}
run: |
git config --global user.email "github-actions[bot]@users.noreply.github.com"
git config --global user.name "github-actions[bot]"
# Re-authenticate git with GitHub token
SERVER_URL_STRIPPED="${SERVER_URL#https://}"
git remote set-url origin "https://x-access-token:${GIT_TOKEN}@${SERVER_URL_STRIPPED}/${REPO_NAME}.git"
echo "Git configured with standard GitHub Actions identity"
- name: Process Safe Outputs
id: process_safe_outputs
uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
env:
GH_AW_AGENT_OUTPUT: ${{ env.GH_AW_AGENT_OUTPUT }}
GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_pull_request\":{\"base_branch\":\"${{ github.ref_name }}\",\"if_no_changes\":\"ignore\",\"max\":1,\"max_patch_size\":1024},\"missing_data\":{},\"missing_tool\":{}}"
GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_discussion\":{\"category\":\"Agentic Workflows\",\"close_older_discussions\":true,\"expires\":168,\"max\":1,\"title_prefix\":\"[SpecBot] \"},\"missing_data\":{},\"missing_tool\":{}}"
with:
github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
script: |

6
.github/workflows/specbot.md vendored
View file

@ -35,8 +35,10 @@ tools:
- ":*"
safe-outputs:
create-pull-request:
if-no-changes: ignore
create-discussion:
title-prefix: "[SpecBot] "
category: "Agentic Workflows"
close-older-discussions: true
missing-tool:
create-issue: true

21
SPECBOT.md
View file

@ -20,7 +20,7 @@ SpecBot uses LLM reasoning to:
2. **Analyze code structure** including members, methods, and dependencies
3. **Mine specifications** using multi-step reasoning about code semantics
4. **Generate annotations** using Z3's existing assertion macros (`SASSERT`, `ENSURE`, `VERIFY`)
5. **Create pull requests** with the annotated code for human review
5. **Create discussions** documenting the proposed specifications for human review and implementation
### Example Annotations
@ -124,11 +124,11 @@ Uses LLM reasoning to infer:
- Follows Z3's coding conventions
- Guards expensive checks with `DEBUG` macros
### 5. Pull Request Creation
Creates a PR with:
- Detailed description of specifications added
### 5. Discussion Creation
Creates a discussion in the "Agentic Workflows" category with:
- Detailed description of specifications identified
- Rationale for each assertion
- Human review recommendations
- Human review and implementation recommendations
## Best Practices
@ -149,17 +149,18 @@ Creates a PR with:
## Human Review Required
SpecBot is a **specification synthesis assistant**, not a replacement for human expertise:
- **Review all assertions** for correctness
- **Review all proposed assertions** for correctness
- **Validate complex invariants** against code semantics
- **Check performance impact** of assertion checks
- **Refine specifications** based on domain knowledge
- **Test changes** before merging
- **Implement changes manually** after review
- **Test changes** before applying to the codebase
LLMs can occasionally hallucinate or miss nuances, so human oversight is essential.
## Output Format
### Pull Request Structure
### Discussion Structure
```markdown
## ✨ Automatic Specification Mining
@ -197,7 +198,7 @@ LLMs can occasionally hallucinate or miss nuances, so human oversight is essenti
Edit `.github/agentics/specbot.md` to modify:
- Agent instructions and guidelines
- Specification synthesis strategies
- Output formatting
- Discussion output formatting
- Error handling behavior
Changes take effect immediately on the next run.
@ -211,7 +212,7 @@ gh aw compile specbot
Recompilation is needed for:
- Changing triggers (schedule, workflow_dispatch)
- Modifying permissions or tools
- Adjusting timeout or safe outputs
- Adjusting timeout or safe outputs (e.g., switching from PR to Discussion)
## Troubleshooting