From e561387900b10744bb650258b8f9d9a4937e4f17 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 11:37:56 -0700 Subject: [PATCH 01/13] Handle `choice_k` in SMT pretty-printer switch to remove macOS `-Wswitch` warning (#9734) `src/ast/ast_smt_pp.cpp` emitted a compiler warning on macOS because `quantifier_kind::choice_k` was not handled in `smt_printer::visit_quantifier`. This change makes the switch exhaustive and preserves printer behavior for existing quantifier kinds. - **Problem** - `visit_quantifier` handled `forall_k`, `exists_k`, and `lambda_k`, but omitted `choice_k`, triggering `-Wswitch`. - **Change** - Added an explicit `choice_k` branch in the quantifier-kind switch in `/tmp/workspace/Z3Prover/z3/src/ast/ast_smt_pp.cpp`. - The branch prints `choice` in SMT output, consistent with how other quantifier headers are emitted. - **Code snippet** ```cpp switch (q->get_kind()) { case forall_k: m_out << "forall "; break; case exists_k: m_out << "exists "; break; case lambda_k: m_out << "lambda "; break; case choice_k: m_out << "choice "; break; } ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/ast_smt_pp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index db52a583f..852e81cf1 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -507,6 +507,7 @@ class smt_printer { case forall_k: m_out << "forall "; break; case exists_k: m_out << "exists "; break; case lambda_k: m_out << "lambda "; break; + case choice_k: m_out << "choice "; break; } m_out << "("; for (unsigned i = 0; i < q->get_num_decls(); ++i) { From 488c9b1b3715fc535f9397aec899ba0160ad6099 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2026 11:43:13 -0700 Subject: [PATCH 02/13] remove AW for F* Signed-off-by: Nikolaj Bjorner --- .github/workflows/fstar-master-build.lock.yml | 1042 ----------------- .github/workflows/fstar-master-build.md | 117 -- 2 files changed, 1159 deletions(-) delete mode 100644 .github/workflows/fstar-master-build.lock.yml delete mode 100644 .github/workflows/fstar-master-build.md diff --git a/.github/workflows/fstar-master-build.lock.yml b/.github/workflows/fstar-master-build.lock.yml deleted file mode 100644 index fde80fbf3..000000000 --- a/.github/workflows/fstar-master-build.lock.yml +++ /dev/null @@ -1,1042 +0,0 @@ -# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"794f78de820db067bdea875107ef6dcb2872fdcf7d90166cfe495f54acd766ad","body_hash":"ac407cfd3ca9748b16f2654fe081a6bab151ff5c338e1775dda9e7c137cf31ed","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"} -# gh-aw-manifest: {"version":1,"secrets":["COPILOT_GITHUB_TOKEN","GH_AW_GITHUB_MCP_SERVER_TOKEN","GH_AW_GITHUB_TOKEN","GITHUB_TOKEN"],"actions":[{"repo":"actions/checkout","sha":"de0fac2e4500dabe0009e67214ff5f5447ce83dd","version":"v6.0.2"},{"repo":"actions/download-artifact","sha":"3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c","version":"v8.0.1"},{"repo":"actions/github-script","sha":"3a2844b7e9c422d3c10d287c895573f7108da1b3","version":"v9.0.0"},{"repo":"actions/github-script","sha":"v9","version":"v9"},{"repo":"actions/upload-artifact","sha":"043fb46d1a93c77aae656e7c1c64a875d1fc6a0a","version":"v7.0.1"},{"repo":"github/gh-aw-actions/setup","sha":"v0.77.5","version":"v0.77.5"}],"resolution_failures":[{"repo":"actions/github-script","ref":"v9","error_type":"dynamic_resolution_failed"}],"containers":[{"image":"ghcr.io/github/gh-aw-firewall/agent:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/squid:0.25.58"},{"image":"ghcr.io/github/gh-aw-mcpg:v0.3.22"},{"image":"ghcr.io/github/github-mcp-server:v1.1.0"},{"image":"node:lts-alpine","digest":"sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f","pinned_image":"node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f"}]} -# ___ _ _ -# / _ \ | | (_) -# | |_| | __ _ ___ _ __ | |_ _ ___ -# | _ |/ _` |/ _ \ '_ \| __| |/ __| -# | | | | (_| | __/ | | | |_| | (__ -# \_| |_/\__, |\___|_| |_|\__|_|\___| -# __/ | -# _ _ |___/ -# | | | | / _| | -# | | | | ___ _ __ _ __| |_| | _____ ____ -# | |/\| |/ _ \ '__| |/ /| _| |/ _ \ \ /\ / / ___| -# \ /\ / (_) | | | | ( | | | | (_) \ V V /\__ \ -# \/ \/ \___/|_| |_|\_\|_| |_|\___/ \_/\_/ |___/ -# -# This file was automatically generated by gh-aw (v0.77.5). DO NOT EDIT. -# -# To update this file, edit the corresponding .md file and run: -# gh aw compile -# Not all edits will cause changes to this file. -# -# For more information: https://github.github.com/gh-aw/introduction/overview/ -# -# Build Z3 master and then build FStar master using that Z3 build -# -# Secrets used: -# - COPILOT_GITHUB_TOKEN -# - GH_AW_GITHUB_MCP_SERVER_TOKEN -# - GH_AW_GITHUB_TOKEN -# - GITHUB_TOKEN -# -# Custom actions used: -# - actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 -# - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 -# - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 -# - actions/github-script@v9 -# - actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 -# - github/gh-aw-actions/setup@v0.77.5 -# -# Container images used: -# - ghcr.io/github/gh-aw-firewall/agent:0.25.58 -# - ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58 -# - ghcr.io/github/gh-aw-firewall/squid:0.25.58 -# - ghcr.io/github/gh-aw-mcpg:v0.3.22 -# - ghcr.io/github/github-mcp-server:v1.1.0 -# - node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f - -name: "Build FStar master with Z3 master" -on: - schedule: - - cron: "9 4 * * *" - # Friendly format: daily (scattered) - workflow_dispatch: - inputs: - aw_context: - default: "" - description: "Agent caller context (used internally by Agentic Workflows)." - required: false - type: string - -permissions: {} - -concurrency: - group: "gh-aw-${{ github.workflow }}" - -run-name: "Build FStar master with Z3 master" - -jobs: - activation: - runs-on: ubuntu-slim - permissions: - actions: read - contents: read - outputs: - comment_id: "" - comment_repo: "" - engine_id: ${{ steps.generate_aw_info.outputs.engine_id }} - lockdown_check_failed: ${{ steps.generate_aw_info.outputs.lockdown_check_failed == 'true' }} - model: ${{ steps.generate_aw_info.outputs.model }} - secret_verification_result: ${{ steps.validate-secret.outputs.verification_result }} - setup-parent-span-id: ${{ steps.setup.outputs.parent-span-id || steps.setup.outputs.span-id }} - setup-span-id: ${{ steps.setup.outputs.span-id }} - setup-trace-id: ${{ steps.setup.outputs.trace-id }} - stale_lock_file_failed: ${{ steps.check-lock-file.outputs.stale_lock_file_failed == 'true' }} - steps: - - name: Setup Scripts - id: setup - uses: github/gh-aw-actions/setup@v0.77.5 - with: - destination: ${{ runner.temp }}/gh-aw/actions - job-name: ${{ github.job }} - env: - GH_AW_SETUP_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/fstar-master-build.lock.yml@${{ github.ref }} - GH_AW_INFO_VERSION: "1.0.55" - GH_AW_INFO_AWF_VERSION: "v0.25.58" - GH_AW_INFO_ENGINE_ID: "copilot" - - name: Generate agentic run info - id: generate_aw_info - env: - GH_AW_INFO_ENGINE_ID: "copilot" - GH_AW_INFO_ENGINE_NAME: "GitHub Copilot CLI" - GH_AW_INFO_MODEL: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || vars.GH_AW_DEFAULT_MODEL_COPILOT || 'claude-sonnet-4.6' }} - GH_AW_INFO_VERSION: "1.0.55" - GH_AW_INFO_AGENT_VERSION: "1.0.55" - GH_AW_INFO_CLI_VERSION: "v0.77.5" - GH_AW_INFO_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_INFO_EXPERIMENTAL: "false" - GH_AW_INFO_SUPPORTS_TOOLS_ALLOWLIST: "true" - GH_AW_INFO_STAGED: "false" - GH_AW_INFO_ALLOWED_DOMAINS: '["defaults"]' - GH_AW_INFO_FIREWALL_ENABLED: "true" - GH_AW_INFO_AWF_VERSION: "v0.25.58" - GH_AW_INFO_AWMG_VERSION: "" - GH_AW_INFO_FIREWALL_TYPE: "squid" - GH_AW_COMPILED_STRICT: "true" - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/generate_aw_info.cjs'); - await main(core, context); - - name: Validate COPILOT_GITHUB_TOKEN secret - id: validate-secret - run: bash "${RUNNER_TEMP}/gh-aw/actions/validate_multi_secret.sh" COPILOT_GITHUB_TOKEN 'GitHub Copilot CLI' https://github.github.com/gh-aw/reference/engines/#github-copilot-default - env: - COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }} - - name: Checkout .github and .agents folders - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - persist-credentials: false - sparse-checkout: | - .github - .agents - .antigravity - .claude - .codex - .crush - .gemini - .opencode - .pi - sparse-checkout-cone-mode: true - fetch-depth: 1 - - name: Save agent config folders for base branch restoration - env: - GH_AW_AGENT_FOLDERS: ".agents .antigravity .claude .codex .crush .gemini .github .opencode .pi" - GH_AW_AGENT_FILES: ".crush.json AGENTS.md ANTIGRAVITY.md CLAUDE.md GEMINI.md PI.md opencode.jsonc" - # poutine:ignore untrusted_checkout_exec - run: bash "${RUNNER_TEMP}/gh-aw/actions/save_base_github_folders.sh" - - name: Check workflow lock file - id: check-lock-file - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_WORKFLOW_FILE: "fstar-master-build.lock.yml" - GH_AW_CONTEXT_WORKFLOW_REF: "${{ github.workflow_ref }}" - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/check_workflow_timestamp_api.cjs'); - await main(); - - name: Check compile-agentic version - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_COMPILED_VERSION: "v0.77.5" - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/check_version_updates.cjs'); - await main(); - - name: Create prompt with built-in context - env: - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - GH_AW_SAFE_OUTPUTS: ${{ runner.temp }}/gh-aw/safeoutputs/outputs.jsonl - GH_AW_EXPR_1A3A194A: ${{ github.event.discussion.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'discussion' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_463A214A: ${{ github.event.pull_request.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'pull_request' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_802A9F6A: ${{ github.event.issue.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'issue' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_FF1D34CE: ${{ github.event.comment.id || fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').comment_id }} - GH_AW_GITHUB_ACTOR: ${{ github.actor }} - GH_AW_GITHUB_REPOSITORY: ${{ github.repository }} - GH_AW_GITHUB_RUN_ID: ${{ github.run_id }} - GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }} - # poutine:ignore untrusted_checkout_exec - run: | - bash "${RUNNER_TEMP}/gh-aw/actions/create_prompt_first.sh" - { - cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - - GH_AW_PROMPT_4e12b9cf31810404_EOF - cat "${RUNNER_TEMP}/gh-aw/prompts/xpia.md" - cat "${RUNNER_TEMP}/gh-aw/prompts/temp_folder_prompt.md" - cat "${RUNNER_TEMP}/gh-aw/prompts/markdown.md" - cat "${RUNNER_TEMP}/gh-aw/prompts/safe_outputs_prompt.md" - cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - - Tools: create_issue - GH_AW_PROMPT_4e12b9cf31810404_EOF - cat "${RUNNER_TEMP}/gh-aw/prompts/safe_outputs_auto_create_issue.md" - cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - - GH_AW_PROMPT_4e12b9cf31810404_EOF - cat "${RUNNER_TEMP}/gh-aw/prompts/mcp_cli_tools_prompt.md" - cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - - The following GitHub context information is available for this workflow: - {{#if github.actor}} - - **actor**: __GH_AW_GITHUB_ACTOR__ - {{/if}} - {{#if github.repository}} - - **repository**: __GH_AW_GITHUB_REPOSITORY__ - {{/if}} - {{#if github.workspace}} - - **workspace**: __GH_AW_GITHUB_WORKSPACE__ - {{/if}} - {{#if github.event.issue.number || (github.aw.context.item_type == 'issue' && github.aw.context.item_number)}} - - **issue-number**: #__GH_AW_EXPR_802A9F6A__ - {{/if}} - {{#if github.event.discussion.number || (github.aw.context.item_type == 'discussion' && github.aw.context.item_number)}} - - **discussion-number**: #__GH_AW_EXPR_1A3A194A__ - {{/if}} - {{#if github.event.pull_request.number || (github.aw.context.item_type == 'pull_request' && github.aw.context.item_number)}} - - **pull-request-number**: #__GH_AW_EXPR_463A214A__ - {{/if}} - {{#if github.event.comment.id || github.aw.context.comment_id}} - - **comment-id**: __GH_AW_EXPR_FF1D34CE__ - {{/if}} - {{#if github.run_id}} - - **workflow-run-id**: __GH_AW_GITHUB_RUN_ID__ - {{/if}} - - - GH_AW_PROMPT_4e12b9cf31810404_EOF - cat "${RUNNER_TEMP}/gh-aw/prompts/github_mcp_tools_with_safeoutputs_prompt.md" - cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - - {{#runtime-import .github/workflows/fstar-master-build.md}} - GH_AW_PROMPT_4e12b9cf31810404_EOF - } > "$GH_AW_PROMPT" - - name: Interpolate variables and render templates - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - GH_AW_ENGINE_ID: "copilot" - GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }} - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/interpolate_prompt.cjs'); - await main(); - - name: Substitute placeholders - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - GH_AW_EXPR_1A3A194A: ${{ github.event.discussion.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'discussion' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_463A214A: ${{ github.event.pull_request.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'pull_request' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_802A9F6A: ${{ github.event.issue.number || (fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_type == 'issue' && fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').item_number) }} - GH_AW_EXPR_FF1D34CE: ${{ github.event.comment.id || fromJSON(github.event.inputs.aw_context || github.event.client_payload.aw_context || '{}').comment_id }} - GH_AW_GITHUB_ACTOR: ${{ github.actor }} - GH_AW_GITHUB_REPOSITORY: ${{ github.repository }} - GH_AW_GITHUB_RUN_ID: ${{ github.run_id }} - GH_AW_GITHUB_WORKSPACE: ${{ github.workspace }} - GH_AW_MCP_CLI_SERVERS_LIST: '- `safeoutputs` — run `safeoutputs --help` to see available tools' - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - - const substitutePlaceholders = require('${{ runner.temp }}/gh-aw/actions/substitute_placeholders.cjs'); - - // Call the substitution function - return await substitutePlaceholders({ - file: process.env.GH_AW_PROMPT, - substitutions: { - GH_AW_EXPR_1A3A194A: process.env.GH_AW_EXPR_1A3A194A, - GH_AW_EXPR_463A214A: process.env.GH_AW_EXPR_463A214A, - GH_AW_EXPR_802A9F6A: process.env.GH_AW_EXPR_802A9F6A, - GH_AW_EXPR_FF1D34CE: process.env.GH_AW_EXPR_FF1D34CE, - GH_AW_GITHUB_ACTOR: process.env.GH_AW_GITHUB_ACTOR, - GH_AW_GITHUB_REPOSITORY: process.env.GH_AW_GITHUB_REPOSITORY, - GH_AW_GITHUB_RUN_ID: process.env.GH_AW_GITHUB_RUN_ID, - GH_AW_GITHUB_WORKSPACE: process.env.GH_AW_GITHUB_WORKSPACE, - GH_AW_MCP_CLI_SERVERS_LIST: process.env.GH_AW_MCP_CLI_SERVERS_LIST - } - }); - - name: Validate prompt placeholders - env: - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - # poutine:ignore untrusted_checkout_exec - run: bash "${RUNNER_TEMP}/gh-aw/actions/validate_prompt_placeholders.sh" - - name: Print prompt - env: - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - # poutine:ignore untrusted_checkout_exec - run: bash "${RUNNER_TEMP}/gh-aw/actions/print_prompt_summary.sh" - - name: Upload activation artifact - if: success() - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 - with: - name: activation - include-hidden-files: true - path: | - /tmp/gh-aw/aw_info.json - /tmp/gh-aw/model_multipliers.json - /tmp/gh-aw/aw-prompts/prompt.txt - /tmp/gh-aw/aw-prompts/prompt-template.txt - /tmp/gh-aw/aw-prompts/prompt-import-tree.json - /tmp/gh-aw/github_rate_limits.jsonl - /tmp/gh-aw/base - /tmp/gh-aw/.github/agents - /tmp/gh-aw/.github/skills - if-no-files-found: ignore - retention-days: 1 - - agent: - needs: activation - runs-on: ubuntu-latest - permissions: read-all - concurrency: - group: "gh-aw-copilot-${{ github.workflow }}" - queue: max - env: - DEFAULT_BRANCH: ${{ github.event.repository.default_branch }} - GH_AW_ASSETS_ALLOWED_EXTS: "" - GH_AW_ASSETS_BRANCH: "" - GH_AW_ASSETS_MAX_SIZE_KB: 0 - GH_AW_MCP_LOG_DIR: /tmp/gh-aw/mcp-logs/safeoutputs - GH_AW_WORKFLOW_ID_SANITIZED: fstarmasterbuild - outputs: - agentic_engine_timeout: ${{ steps.detect-agent-errors.outputs.agentic_engine_timeout || 'false' }} - checkout_pr_success: ${{ steps.checkout-pr.outputs.checkout_pr_success || 'true' }} - effective_tokens: ${{ steps.parse-mcp-gateway.outputs.effective_tokens }} - effective_tokens_rate_limit_error: ${{ steps.parse-mcp-gateway.outputs.effective_tokens_rate_limit_error || 'false' }} - has_patch: ${{ steps.collect_output.outputs.has_patch }} - inference_access_error: ${{ steps.detect-agent-errors.outputs.inference_access_error || 'false' }} - mcp_policy_error: ${{ steps.detect-agent-errors.outputs.mcp_policy_error || 'false' }} - model: ${{ needs.activation.outputs.model }} - model_not_supported_error: ${{ steps.detect-agent-errors.outputs.model_not_supported_error || 'false' }} - output: ${{ steps.collect_output.outputs.output }} - output_types: ${{ steps.collect_output.outputs.output_types }} - setup-parent-span-id: ${{ steps.setup.outputs.parent-span-id || steps.setup.outputs.span-id }} - setup-span-id: ${{ steps.setup.outputs.span-id }} - setup-trace-id: ${{ steps.setup.outputs.trace-id }} - steps: - - name: Setup Scripts - id: setup - uses: github/gh-aw-actions/setup@v0.77.5 - with: - destination: ${{ runner.temp }}/gh-aw/actions - job-name: ${{ github.job }} - trace-id: ${{ needs.activation.outputs.setup-trace-id }} - parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }} - env: - GH_AW_SETUP_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/fstar-master-build.lock.yml@${{ github.ref }} - GH_AW_INFO_VERSION: "1.0.55" - GH_AW_INFO_AWF_VERSION: "v0.25.58" - GH_AW_INFO_ENGINE_ID: "copilot" - - name: Set runtime paths - id: set-runtime-paths - run: | - { - echo "GH_AW_SAFE_OUTPUTS=${RUNNER_TEMP}/gh-aw/safeoutputs/outputs.jsonl" - echo "GH_AW_SAFE_OUTPUTS_CONFIG_PATH=${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" - echo "GH_AW_SAFE_OUTPUTS_TOOLS_PATH=${RUNNER_TEMP}/gh-aw/safeoutputs/tools.json" - } >> "$GITHUB_OUTPUT" - - name: Create gh-aw temp directory - run: bash "${RUNNER_TEMP}/gh-aw/actions/create_gh_aw_tmp_dir.sh" - - name: Configure gh CLI for GitHub Enterprise - run: bash "${RUNNER_TEMP}/gh-aw/actions/configure_gh_for_ghe.sh" - env: - GH_TOKEN: ${{ github.token }} - - name: Checkout Z3 master - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - fetch-depth: 1 - persist-credentials: false - ref: master - - - name: Configure Git credentials - env: - REPO_NAME: ${{ github.repository }} - SERVER_URL: ${{ github.server_url }} - GITHUB_TOKEN: ${{ github.token }} - run: | - git config --global user.email "github-actions[bot]@users.noreply.github.com" - git config --global user.name "github-actions[bot]" - git config --global am.keepcr true - # Re-authenticate git with GitHub token - SERVER_URL_STRIPPED="${SERVER_URL#https://}" - git remote set-url origin "https://x-access-token:${GITHUB_TOKEN}@${SERVER_URL_STRIPPED}/${REPO_NAME}.git" - echo "Git configured with standard GitHub Actions identity" - - name: Checkout PR branch - id: checkout-pr - if: | - github.event.pull_request || github.event.issue.pull_request - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - with: - github-token: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/checkout_pr_branch.cjs'); - await main(); - - name: Install GitHub Copilot CLI - run: bash "${RUNNER_TEMP}/gh-aw/actions/install_copilot_cli.sh" 1.0.55 - env: - GH_HOST: github.com - - name: Install AWF binary - run: bash "${RUNNER_TEMP}/gh-aw/actions/install_awf_binary.sh" v0.25.58 - - name: Determine automatic lockdown mode for GitHub MCP Server - id: determine-automatic-lockdown - uses: actions/github-script@v9 - env: - GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }} - GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }} - with: - script: | - const determineAutomaticLockdown = require('${{ runner.temp }}/gh-aw/actions/determine_automatic_lockdown.cjs'); - await determineAutomaticLockdown(github, context, core); - - name: Download activation artifact - uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 - with: - name: activation - path: /tmp/gh-aw - - name: Restore agent config folders from base branch - if: steps.checkout-pr.outcome == 'success' - env: - GH_AW_AGENT_FOLDERS: ".agents .antigravity .claude .codex .crush .gemini .github .opencode .pi" - GH_AW_AGENT_FILES: ".crush.json AGENTS.md ANTIGRAVITY.md CLAUDE.md GEMINI.md PI.md opencode.jsonc" - run: bash "${RUNNER_TEMP}/gh-aw/actions/restore_base_github_folders.sh" - - name: Restore inline sub-agents from activation artifact - env: - GH_AW_SUB_AGENT_DIR: ".github/agents" - GH_AW_SUB_AGENT_EXT: ".agent.md" - run: bash "${RUNNER_TEMP}/gh-aw/actions/restore_inline_sub_agents.sh" - - name: Restore inline skills from activation artifact - env: - GH_AW_SKILL_DIR: ".github/skills" - run: bash "${RUNNER_TEMP}/gh-aw/actions/restore_inline_skills.sh" - - name: Download container images - run: bash "${RUNNER_TEMP}/gh-aw/actions/download_docker_images.sh" ghcr.io/github/gh-aw-firewall/agent:0.25.58 ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58 ghcr.io/github/gh-aw-firewall/squid:0.25.58 ghcr.io/github/gh-aw-mcpg:v0.3.22 ghcr.io/github/github-mcp-server:v1.1.0 node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f - - name: Generate Safe Outputs Config - run: | - mkdir -p "${RUNNER_TEMP}/gh-aw/safeoutputs" - mkdir -p /tmp/gh-aw/safeoutputs - mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs - cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_40098289a87b7e38_EOF' - {"create_issue":{"labels":["fstar-master-build"],"max":1,"title_prefix":"[fstar-master-build]"}} - GH_AW_SAFE_OUTPUTS_CONFIG_40098289a87b7e38_EOF - - name: Generate Safe Outputs Tools - env: - GH_AW_TOOLS_META_JSON: | - { - "description_suffixes": { - "create_issue": " CONSTRAINTS: Maximum 1 issue(s) can be created. Title will be prefixed with \"[fstar-master-build]\". Labels [\"fstar-master-build\"] will be automatically added." - }, - "repo_params": {}, - "dynamic_tools": [] - } - GH_AW_VALIDATION_JSON: | - { - "create_issue": { - "defaultMax": 1, - "fields": { - "body": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 65000 - }, - "fields": { - "type": "array" - }, - "labels": { - "type": "array", - "itemType": "string", - "itemSanitize": true, - "itemMaxLength": 128 - }, - "parent": { - "issueOrPRNumber": true - }, - "repo": { - "type": "string", - "maxLength": 256 - }, - "temporary_id": { - "type": "string" - }, - "title": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 128 - } - } - } - } - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/generate_safe_outputs_tools.cjs'); - await main(); - - name: Generate Safe Outputs MCP Server Config - id: safe-outputs-config - run: | - # Generate a secure random API key (360 bits of entropy, 40+ chars) - # Mask immediately to prevent timing vulnerabilities - API_KEY=$(openssl rand -base64 45 | tr -d '/+=') - echo "::add-mask::${API_KEY}" - - PORT=3001 - - # Set outputs for next steps - { - echo "safe_outputs_api_key=${API_KEY}" - echo "safe_outputs_port=${PORT}" - } >> "$GITHUB_OUTPUT" - - echo "Safe Outputs MCP server will run on port ${PORT}" - - - name: Start Safe Outputs MCP HTTP Server - id: safe-outputs-start - env: - DEBUG: '*' - GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }} - GH_AW_SAFE_OUTPUTS_PORT: ${{ steps.safe-outputs-config.outputs.safe_outputs_port }} - GH_AW_SAFE_OUTPUTS_API_KEY: ${{ steps.safe-outputs-config.outputs.safe_outputs_api_key }} - GH_AW_SAFE_OUTPUTS_TOOLS_PATH: ${{ runner.temp }}/gh-aw/safeoutputs/tools.json - GH_AW_SAFE_OUTPUTS_CONFIG_PATH: ${{ runner.temp }}/gh-aw/safeoutputs/config.json - GH_AW_MCP_LOG_DIR: /tmp/gh-aw/mcp-logs/safeoutputs - run: | - # Environment variables are set above to prevent template injection - export DEBUG - export GH_AW_SAFE_OUTPUTS - export GH_AW_SAFE_OUTPUTS_PORT - export GH_AW_SAFE_OUTPUTS_API_KEY - export GH_AW_SAFE_OUTPUTS_TOOLS_PATH - export GH_AW_SAFE_OUTPUTS_CONFIG_PATH - export GH_AW_MCP_LOG_DIR - - bash "${RUNNER_TEMP}/gh-aw/actions/start_safe_outputs_server.sh" - - - name: Start MCP Gateway - id: start-mcp-gateway - env: - GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }} - GH_AW_SAFE_OUTPUTS_API_KEY: ${{ steps.safe-outputs-start.outputs.api_key }} - GH_AW_SAFE_OUTPUTS_PORT: ${{ steps.safe-outputs-start.outputs.port }} - GITHUB_MCP_GUARD_MIN_INTEGRITY: ${{ steps.determine-automatic-lockdown.outputs.min_integrity }} - GITHUB_MCP_GUARD_REPOS: ${{ steps.determine-automatic-lockdown.outputs.repos }} - GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - run: | - set -eo pipefail - mkdir -p "${RUNNER_TEMP}/gh-aw/mcp-config" - - # Export gateway environment variables for MCP config and gateway script - export MCP_GATEWAY_PORT="8080" - export MCP_GATEWAY_DOMAIN="host.docker.internal" - export MCP_GATEWAY_HOST_DOMAIN="localhost" - MCP_GATEWAY_API_KEY=$(openssl rand -base64 45 | tr -d '/+=') - echo "::add-mask::${MCP_GATEWAY_API_KEY}" - export MCP_GATEWAY_API_KEY - export MCP_GATEWAY_PAYLOAD_DIR="/tmp/gh-aw/mcp-payloads" - mkdir -p "${MCP_GATEWAY_PAYLOAD_DIR}" - export MCP_GATEWAY_PAYLOAD_SIZE_THRESHOLD="524288" - export DEBUG="*" - - export GH_AW_ENGINE="copilot" - MCP_GATEWAY_UID=$(id -u 2>/dev/null || echo '0') - MCP_GATEWAY_GID=$(id -g 2>/dev/null || echo '0') - case "${DOCKER_HOST:-}" in - unix://* ) DOCKER_SOCK_PATH="${DOCKER_HOST#unix://}" ;; - /* ) DOCKER_SOCK_PATH="$DOCKER_HOST" ;; - * ) DOCKER_SOCK_PATH=/var/run/docker.sock ;; - esac - DOCKER_SOCK_GID=$(stat -c '%g' "$DOCKER_SOCK_PATH" 2>/dev/null || echo '0') - export MCP_GATEWAY_DOCKER_COMMAND='docker run -i --rm --network host --add-host host.docker.internal:127.0.0.1 --user '"${MCP_GATEWAY_UID}"':'"${MCP_GATEWAY_GID}"' --group-add '"${DOCKER_SOCK_GID}"' -v '"${DOCKER_SOCK_PATH}"':/var/run/docker.sock -e MCP_GATEWAY_PORT -e MCP_GATEWAY_DOMAIN -e MCP_GATEWAY_API_KEY -e MCP_GATEWAY_PAYLOAD_DIR -e MCP_GATEWAY_PAYLOAD_SIZE_THRESHOLD -e DOCKER_HOST=unix:///var/run/docker.sock -e DEBUG -e MCP_GATEWAY_LOG_DIR -e GH_AW_MCP_LOG_DIR -e GH_AW_SAFE_OUTPUTS -e GH_AW_SAFE_OUTPUTS_CONFIG_PATH -e GH_AW_SAFE_OUTPUTS_TOOLS_PATH -e GH_AW_ASSETS_BRANCH -e GH_AW_ASSETS_MAX_SIZE_KB -e GH_AW_ASSETS_ALLOWED_EXTS -e DEFAULT_BRANCH -e GITHUB_MCP_SERVER_TOKEN -e GITHUB_MCP_GUARD_MIN_INTEGRITY -e GITHUB_MCP_GUARD_REPOS -e GITHUB_REPOSITORY -e GITHUB_SERVER_URL -e GITHUB_SHA -e GITHUB_WORKSPACE -e GITHUB_TOKEN -e GITHUB_RUN_ID -e GITHUB_RUN_NUMBER -e GITHUB_RUN_ATTEMPT -e GITHUB_JOB -e GITHUB_ACTION -e GITHUB_EVENT_NAME -e GITHUB_EVENT_PATH -e GITHUB_ACTOR -e GITHUB_ACTOR_ID -e GITHUB_TRIGGERING_ACTOR -e GITHUB_WORKFLOW -e GITHUB_WORKFLOW_REF -e GITHUB_WORKFLOW_SHA -e GITHUB_REF -e GITHUB_REF_NAME -e GITHUB_REF_TYPE -e GITHUB_HEAD_REF -e GITHUB_BASE_REF -e GH_AW_SAFE_OUTPUTS_PORT -e GH_AW_SAFE_OUTPUTS_API_KEY -v /tmp/gh-aw/mcp-payloads:/tmp/gh-aw/mcp-payloads:rw -v /opt:/opt:ro -v /tmp:/tmp:rw -v '"${GITHUB_WORKSPACE}"':'"${GITHUB_WORKSPACE}"':rw ghcr.io/github/gh-aw-mcpg:v0.3.22' - - mkdir -p /home/runner/.copilot - GH_AW_NODE=$(which node 2>/dev/null || command -v node 2>/dev/null || echo node) - cat << GH_AW_MCP_CONFIG_bb501b6f2b1412ea_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs" - { - "mcpServers": { - "github": { - "type": "stdio", - "container": "ghcr.io/github/github-mcp-server:v1.1.0", - "env": { - "GITHUB_HOST": "\${GITHUB_SERVER_URL}", - "GITHUB_PERSONAL_ACCESS_TOKEN": "\${GITHUB_MCP_SERVER_TOKEN}", - "GITHUB_READ_ONLY": "1", - "GITHUB_TOOLSETS": "context,repos,issues,pull_requests" - }, - "guard-policies": { - "allow-only": { - "min-integrity": "$GITHUB_MCP_GUARD_MIN_INTEGRITY", - "repos": "$GITHUB_MCP_GUARD_REPOS" - } - } - }, - "safeoutputs": { - "type": "http", - "url": "http://host.docker.internal:$GH_AW_SAFE_OUTPUTS_PORT", - "headers": { - "Authorization": "\${GH_AW_SAFE_OUTPUTS_API_KEY}" - }, - "guard-policies": { - "write-sink": { - "accept": [ - "*" - ] - } - } - } - }, - "gateway": { - "port": $MCP_GATEWAY_PORT, - "domain": "${MCP_GATEWAY_DOMAIN}", - "apiKey": "${MCP_GATEWAY_API_KEY}", - "payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}" - } - } - GH_AW_MCP_CONFIG_bb501b6f2b1412ea_EOF - - name: Mount MCP servers as CLIs - id: mount-mcp-clis - continue-on-error: true - env: - MCP_GATEWAY_API_KEY: ${{ steps.start-mcp-gateway.outputs.gateway-api-key }} - MCP_GATEWAY_DOMAIN: ${{ steps.start-mcp-gateway.outputs.gateway-domain }} - MCP_GATEWAY_PORT: ${{ steps.start-mcp-gateway.outputs.gateway-port }} - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io); - const { main } = require('${{ runner.temp }}/gh-aw/actions/mount_mcp_as_cli.cjs'); - await main(); - - name: Clean credentials - continue-on-error: true - run: bash "${RUNNER_TEMP}/gh-aw/actions/clean_git_credentials.sh" - - name: Audit pre-agent workspace - id: pre_agent_audit - continue-on-error: true - run: bash "${RUNNER_TEMP}/gh-aw/actions/audit_pre_agent_workspace.sh" - - name: Execute GitHub Copilot CLI - id: agentic_execution - # Copilot CLI tool arguments (sorted): - timeout-minutes: 180 - run: | - set -o pipefail - printf '%s' "$(date +%s%3N)" > /tmp/gh-aw/agent_cli_start_ms.txt - touch /tmp/gh-aw/agent-step-summary.md - GH_AW_NODE_BIN=$(command -v node 2>/dev/null || true) - export GH_AW_NODE_BIN - export COPILOT_API_KEY="$COPILOT_DUMMY_BYOK" - (umask 177 && touch /tmp/gh-aw/agent-stdio.log) - printf '%s\n' '{"$schema":"https://github.com/github/gh-aw-firewall/releases/download/v0.25.58/awf-config.schema.json","network":{"allowDomains":["api.business.githubcopilot.com","api.enterprise.githubcopilot.com","api.github.com","api.githubcopilot.com","api.individual.githubcopilot.com","api.snapcraft.io","archive.ubuntu.com","azure.archive.ubuntu.com","crl.geotrust.com","crl.globalsign.com","crl.identrust.com","crl.sectigo.com","crl.thawte.com","crl.usertrust.com","crl.verisign.com","crl3.digicert.com","crl4.digicert.com","crls.ssl.com","github.com","host.docker.internal","json-schema.org","json.schemastore.org","keyserver.ubuntu.com","ocsp.digicert.com","ocsp.geotrust.com","ocsp.globalsign.com","ocsp.identrust.com","ocsp.sectigo.com","ocsp.ssl.com","ocsp.thawte.com","ocsp.usertrust.com","ocsp.verisign.com","packagecloud.io","packages.cloud.google.com","packages.microsoft.com","ppa.launchpad.net","raw.githubusercontent.com","registry.npmjs.org","s.symcb.com","s.symcd.com","security.ubuntu.com","telemetry.enterprise.githubcopilot.com","ts-crl.ws.symantec.com","ts-ocsp.ws.symantec.com","www.googleapis.com"]},"apiProxy":{"enabled":true,"enableTokenSteering":true,"maxRuns":500,"maxEffectiveTokens":25000000,"models":{"agent":["sonnet-6x","gpt-5.4","gpt-5.3","gemini-pro","any"],"antigravity":["copilot/antigravity*","google/antigravity*","gemini/antigravity*"],"any":["copilot/*","anthropic/*","openai/*","google/*","gemini/*"],"claude":["agent"],"codex":["agent"],"coding":["copilot/gpt-5*codex*","openai/gpt-5*codex*","gpt-5-codex"],"computer-use":["copilot/*computer-use*","google/*computer-use*","gemini/*computer-use*","openai/*computer-use*"],"copilot":["agent"],"deep-research":["copilot/deep-research*","copilot/o3-deep-research*","copilot/o4-mini-deep-research*","google/deep-research*","gemini/deep-research*","openai/o3-deep-research*","openai/o4-mini-deep-research*"],"gemini":["agent"],"gemini-3-flash":["copilot/gemini-3*flash*","google/gemini-3*flash*","gemini/gemini-3*flash*"],"gemini-3-pro":["copilot/gemini-3*pro*","google/gemini-3*pro*","gemini/gemini-3*pro*"],"gemini-3.1-flash":["copilot/gemini-3.1*flash*","google/gemini-3.1*flash*","gemini/gemini-3.1*flash*"],"gemini-3.1-pro":["copilot/gemini-3.1*pro*","google/gemini-3.1*pro*","gemini/gemini-3.1*pro*"],"gemini-3.5-flash":["copilot/gemini-3.5*flash*","google/gemini-3.5*flash*","gemini/gemini-3.5*flash*"],"gemini-flash":["copilot/gemini-*flash*","google/gemini-*flash*","gemini/gemini-*flash*"],"gemini-flash-lite":["copilot/gemini-*flash*lite*","google/gemini-*flash*lite*","gemini/gemini-*flash*lite*"],"gemini-pro":["copilot/gemini-*pro*","google/gemini-*pro*","gemini/gemini-*pro*"],"gemma":["copilot/gemma*","google/gemma*","gemini/gemma*"],"gpt-5":["copilot/gpt-5*","openai/gpt-5*"],"gpt-5-codex":["copilot/gpt-5*codex*","openai/gpt-5*codex*"],"gpt-5-mini":["copilot/gpt-5*mini*","openai/gpt-5*mini*"],"gpt-5-nano":["copilot/gpt-5*nano*","openai/gpt-5*nano*"],"gpt-5-pro":["copilot/gpt-5*pro*","openai/gpt-5*pro*"],"gpt-5.2":["copilot/gpt-5.2*","openai/gpt-5.2*"],"gpt-5.3":["copilot/gpt-5.3*","openai/gpt-5.3*"],"gpt-5.4":["copilot/gpt-5.4*","openai/gpt-5.4*"],"gpt-5.5":["copilot/gpt-5.5*","openai/gpt-5.5*"],"haiku":["copilot/*haiku*","anthropic/*haiku*"],"large":["sonnet","gpt-5-pro","gpt-5","gemini-pro"],"mini":["haiku","gpt-5-mini","gpt-5-nano","gemini-flash-lite"],"opus":["copilot/*opus*","anthropic/*opus*"],"opusplan":["opus?effort=high"],"reasoning":["copilot/o1*","copilot/o3*","copilot/o4*","openai/o1*","openai/o3*","openai/o4*"],"robotics":["copilot/*robotics*","google/*robotics*","gemini/*robotics*"],"small":["mini"],"sonnet":["copilot/*sonnet*","anthropic/*sonnet*"],"sonnet-6x":["copilot/*sonnet-4-5-*","anthropic/*sonnet-4-5-*","copilot/*sonnet-4-6*","anthropic/*sonnet-4-6*"],"summarization":["haiku","gpt-5-mini","gemini-flash-lite","mini"],"vision":["copilot/gemini-*image*","gemini/gemini-*image*","copilot/gemini-*flash*","gemini/gemini-*flash*"]}},"container":{"imageTag":"0.25.58"}}' > "${RUNNER_TEMP}/gh-aw/awf-config.json" - GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs" - cp "${RUNNER_TEMP}/gh-aw/awf-config.json" /tmp/gh-aw/awf-config.json - GH_AW_DOCKER_HOST_PATH_PREFIX_ARGS="" - if [[ "${DOCKER_HOST:-}" =~ ^tcp:// ]]; then - GH_AW_DOCKER_HOST_PATH_PREFIX_ARGS="--docker-host-path-prefix /tmp/gh-aw" - fi - GH_AW_TOOL_CACHE_MOUNT="" - GH_AW_TOOL_CACHE="${RUNNER_TOOL_CACHE:-/opt/hostedtoolcache}" - if [ -d "$GH_AW_TOOL_CACHE" ]; then - if [[ "$GH_AW_TOOL_CACHE" != /opt/* ]]; then - GH_AW_TOOL_CACHE_MOUNT="$GH_AW_TOOL_CACHE:$GH_AW_TOOL_CACHE:ro" - fi - elif [ -d "/home/runner/work/_tool" ]; then - GH_AW_TOOL_CACHE_MOUNT="/home/runner/work/_tool:/home/runner/work/_tool:ro" - fi - # shellcheck disable=SC1003 - sudo -E awf --config "${RUNNER_TEMP}/gh-aw/awf-config.json" --container-workdir "${GITHUB_WORKSPACE}" --mount "${RUNNER_TEMP}/gh-aw:${RUNNER_TEMP}/gh-aw:ro" --mount "${RUNNER_TEMP}/gh-aw:/host${RUNNER_TEMP}/gh-aw:ro" ${GH_AW_TOOL_CACHE_MOUNT:+--mount "$GH_AW_TOOL_CACHE_MOUNT"} ${GH_AW_DOCKER_HOST_PATH_PREFIX_ARGS} --env-all --exclude-env COPILOT_GITHUB_TOKEN --exclude-env GITHUB_MCP_SERVER_TOKEN --exclude-env MCP_GATEWAY_API_KEY --log-level info --proxy-logs-dir /tmp/gh-aw/sandbox/firewall/logs --audit-dir /tmp/gh-aw/sandbox/firewall/audit --enable-host-access --allow-host-ports 80,443,8080 --skip-pull \ - -- /bin/bash -c 'set +o histexpand; export PATH="${RUNNER_TEMP}/gh-aw/mcp-cli/bin:$PATH" && GH_AW_TOOL_CACHE="${RUNNER_TOOL_CACHE:-/opt/hostedtoolcache}"; export PATH="$(find "$GH_AW_TOOL_CACHE" /opt/hostedtoolcache /home/runner/work/_tool -maxdepth 5 -type d -name bin 2>/dev/null | tr '\''\n'\'' '\'':'\'')$PATH"; [ -n "$GOROOT" ] && export PATH="$GOROOT/bin:$PATH" || true && GH_AW_NODE_EXEC="${GH_AW_NODE_BIN:-}"; if [ -z "$GH_AW_NODE_EXEC" ] || [ ! -x "$GH_AW_NODE_EXEC" ]; then GH_AW_NODE_EXEC="$(command -v node 2>/dev/null || true)"; fi; if [ -z "$GH_AW_NODE_EXEC" ]; then echo "node runtime missing on this runner — check runtimes.node in workflow YAML" >&2; exit 127; fi; "$GH_AW_NODE_EXEC" ${RUNNER_TEMP}/gh-aw/actions/copilot_harness.cjs /usr/local/bin/copilot --add-dir /tmp/gh-aw/ --log-level all --log-dir /tmp/gh-aw/sandbox/agent/logs/ --disable-builtin-mcps --no-ask-user --allow-all-tools --allow-all-paths --add-dir "${GITHUB_WORKSPACE}" --prompt-file /tmp/gh-aw/aw-prompts/prompt.txt' 2>&1 | tee -a /tmp/gh-aw/agent-stdio.log - env: - AWF_REFLECT_ENABLED: 1 - COPILOT_AGENT_RUNNER_TYPE: STANDALONE - COPILOT_DUMMY_BYOK: dummy-byok-key-for-offline-mode - COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }} - COPILOT_MODEL: ${{ vars.GH_AW_MODEL_AGENT_COPILOT || vars.GH_AW_DEFAULT_MODEL_COPILOT || 'claude-sonnet-4.6' }} - GH_AW_MCP_CONFIG: /home/runner/.copilot/mcp-config.json - GH_AW_PHASE: agent - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }} - GH_AW_VERSION: v0.77.5 - GITHUB_API_URL: ${{ github.api_url }} - GITHUB_AW: true - GITHUB_COPILOT_INTEGRATION_ID: agentic-workflows - GITHUB_HEAD_REF: ${{ github.head_ref }} - GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN || secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - GITHUB_REF_NAME: ${{ github.ref_name }} - GITHUB_SERVER_URL: ${{ github.server_url }} - GITHUB_STEP_SUMMARY: /tmp/gh-aw/agent-step-summary.md - GITHUB_WORKSPACE: ${{ github.workspace }} - GIT_AUTHOR_EMAIL: github-actions[bot]@users.noreply.github.com - GIT_AUTHOR_NAME: github-actions[bot] - GIT_COMMITTER_EMAIL: github-actions[bot]@users.noreply.github.com - GIT_COMMITTER_NAME: github-actions[bot] - RUNNER_TEMP: ${{ runner.temp }} - XDG_CONFIG_HOME: /home/runner - - name: Detect agent errors - if: always() - id: detect-agent-errors - continue-on-error: true - run: node "${RUNNER_TEMP}/gh-aw/actions/detect_agent_errors.cjs" - - name: Configure Git credentials - env: - REPO_NAME: ${{ github.repository }} - SERVER_URL: ${{ github.server_url }} - GITHUB_TOKEN: ${{ github.token }} - run: | - git config --global user.email "github-actions[bot]@users.noreply.github.com" - git config --global user.name "github-actions[bot]" - git config --global am.keepcr true - # Re-authenticate git with GitHub token - SERVER_URL_STRIPPED="${SERVER_URL#https://}" - git remote set-url origin "https://x-access-token:${GITHUB_TOKEN}@${SERVER_URL_STRIPPED}/${REPO_NAME}.git" - echo "Git configured with standard GitHub Actions identity" - - name: Copy Copilot session state files to logs - if: always() - continue-on-error: true - run: bash "${RUNNER_TEMP}/gh-aw/actions/copy_copilot_session_state.sh" - - name: Stop MCP Gateway - if: always() - continue-on-error: true - env: - MCP_GATEWAY_PORT: ${{ steps.start-mcp-gateway.outputs.gateway-port }} - MCP_GATEWAY_API_KEY: ${{ steps.start-mcp-gateway.outputs.gateway-api-key }} - GATEWAY_PID: ${{ steps.start-mcp-gateway.outputs.gateway-pid }} - run: | - bash "${RUNNER_TEMP}/gh-aw/actions/stop_mcp_gateway.sh" "$GATEWAY_PID" - - name: Redact secrets in logs - if: always() - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/redact_secrets.cjs'); - await main(); - env: - GH_AW_SECRET_NAMES: 'COPILOT_GITHUB_TOKEN,GH_AW_GITHUB_MCP_SERVER_TOKEN,GH_AW_GITHUB_TOKEN,GITHUB_TOKEN' - SECRET_COPILOT_GITHUB_TOKEN: ${{ secrets.COPILOT_GITHUB_TOKEN }} - SECRET_GH_AW_GITHUB_MCP_SERVER_TOKEN: ${{ secrets.GH_AW_GITHUB_MCP_SERVER_TOKEN }} - SECRET_GH_AW_GITHUB_TOKEN: ${{ secrets.GH_AW_GITHUB_TOKEN }} - SECRET_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - - name: Append agent step summary - if: always() - run: bash "${RUNNER_TEMP}/gh-aw/actions/append_agent_step_summary.sh" - - name: Copy Safe Outputs - if: always() - env: - GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }} - run: | - mkdir -p /tmp/gh-aw - cp "$GH_AW_SAFE_OUTPUTS" /tmp/gh-aw/safeoutputs.jsonl 2>/dev/null || true - - name: Ingest agent output - id: collect_output - if: always() - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_SAFE_OUTPUTS: ${{ steps.set-runtime-paths.outputs.GH_AW_SAFE_OUTPUTS }} - GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com" - GITHUB_SERVER_URL: ${{ github.server_url }} - GITHUB_API_URL: ${{ github.api_url }} - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/collect_ndjson_output.cjs'); - await main(); - - name: Parse agent logs for step summary - if: always() - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_AGENT_OUTPUT: /tmp/gh-aw/sandbox/agent/logs/ - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/parse_copilot_log.cjs'); - await main(); - - name: Parse MCP Gateway logs for step summary - if: always() - id: parse-mcp-gateway - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/parse_mcp_gateway_log.cjs'); - await main(); - - name: Print firewall logs - if: always() - continue-on-error: true - env: - AWF_LOGS_DIR: /tmp/gh-aw/sandbox/firewall/logs - run: | - # Fix permissions on firewall logs/audit dirs so they can be uploaded as artifacts - # AWF runs with sudo, creating files owned by root - sudo chmod -R a+rX /tmp/gh-aw/sandbox/firewall 2>/dev/null || true - # Only run awf logs summary if awf command exists (it may not be installed if workflow failed before install step) - if command -v awf &> /dev/null; then - awf logs summary | tee -a "$GITHUB_STEP_SUMMARY" - else - echo 'AWF binary not installed, skipping firewall log summary' - fi - - name: Parse token usage for step summary - if: always() - continue-on-error: true - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/parse_token_usage.cjs'); - await main(); - - name: Print AWF reflect summary - if: always() - continue-on-error: true - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - with: - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/awf_reflect_summary.cjs'); - await main(); - - name: Write agent output placeholder if missing - if: always() - run: | - if [ ! -f /tmp/gh-aw/agent_output.json ]; then - echo '{"items":[]}' > /tmp/gh-aw/agent_output.json - fi - - name: Upload agent artifacts - if: always() - continue-on-error: true - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 - with: - name: agent - path: | - /tmp/gh-aw/aw-prompts/prompt.txt - /tmp/gh-aw/sandbox/agent/logs/ - /tmp/gh-aw/redacted-urls.log - /tmp/gh-aw/mcp-logs/ - /tmp/gh-aw/agent_usage.json - /tmp/gh-aw/agent-stdio.log - /tmp/gh-aw/pre-agent-audit.txt - /tmp/gh-aw/agent/ - /tmp/gh-aw/github_rate_limits.jsonl - /tmp/gh-aw/safeoutputs.jsonl - /tmp/gh-aw/agent_output.json - /tmp/gh-aw/awf-config.json - /tmp/gh-aw/sandbox/firewall/logs/ - /tmp/gh-aw/sandbox/firewall/audit/ - /tmp/gh-aw/sandbox/firewall/awf-reflect.json - if-no-files-found: ignore - - conclusion: - needs: - - activation - - agent - - safe_outputs - if: > - always() && (needs.agent.result != 'skipped' || needs.activation.outputs.lockdown_check_failed == 'true' || - needs.activation.outputs.stale_lock_file_failed == 'true') - runs-on: ubuntu-slim - permissions: - contents: read - issues: write - concurrency: - group: "gh-aw-conclusion-fstar-master-build" - cancel-in-progress: false - queue: max - steps: - - name: Setup Scripts - id: setup - uses: github/gh-aw-actions/setup@v0.77.5 - with: - destination: ${{ runner.temp }}/gh-aw/actions - job-name: ${{ github.job }} - trace-id: ${{ needs.activation.outputs.setup-trace-id }} - parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }} - env: - GH_AW_SETUP_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/fstar-master-build.lock.yml@${{ github.ref }} - GH_AW_INFO_VERSION: "1.0.55" - GH_AW_INFO_AWF_VERSION: "v0.25.58" - GH_AW_INFO_ENGINE_ID: "copilot" - - name: Download agent output artifact - id: download-agent-output - continue-on-error: true - uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 - with: - name: agent - path: /tmp/gh-aw/ - - name: Setup agent output environment variable - id: setup-agent-output-env - if: steps.download-agent-output.outcome == 'success' - run: | - mkdir -p /tmp/gh-aw/ - find "/tmp/gh-aw/" -type f -print - echo "GH_AW_AGENT_OUTPUT=/tmp/gh-aw/agent_output.json" >> "$GITHUB_OUTPUT" - - name: Handle agent failure - id: handle_agent_failure - if: always() - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }} - GH_AW_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/fstar-master-build.md" - GH_AW_RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }} - GH_AW_AGENT_CONCLUSION: ${{ needs.agent.result }} - GH_AW_WORKFLOW_ID: "fstar-master-build" - GH_AW_ACTION_FAILURE_ISSUE_EXPIRES_HOURS: "168" - GH_AW_ENGINE_ID: "copilot" - GH_AW_SECRET_VERIFICATION_RESULT: ${{ needs.activation.outputs.secret_verification_result }} - GH_AW_CHECKOUT_PR_SUCCESS: ${{ needs.agent.outputs.checkout_pr_success }} - GH_AW_EFFECTIVE_TOKENS: ${{ needs.agent.outputs.effective_tokens || '' }} - GH_AW_EFFECTIVE_TOKENS_RATE_LIMIT_ERROR: ${{ needs.agent.outputs.effective_tokens_rate_limit_error || 'false' }} - GH_AW_INFERENCE_ACCESS_ERROR: ${{ needs.agent.outputs.inference_access_error }} - GH_AW_MCP_POLICY_ERROR: ${{ needs.agent.outputs.mcp_policy_error }} - GH_AW_AGENTIC_ENGINE_TIMEOUT: ${{ needs.agent.outputs.agentic_engine_timeout }} - GH_AW_MODEL_NOT_SUPPORTED_ERROR: ${{ needs.agent.outputs.model_not_supported_error }} - GH_AW_ENGINE_API_HOSTS: "api.enterprise.githubcopilot.com,api.githubcopilot.com,api.business.githubcopilot.com,api.individual.githubcopilot.com" - GH_AW_LOCKDOWN_CHECK_FAILED: ${{ needs.activation.outputs.lockdown_check_failed }} - GH_AW_STALE_LOCK_FILE_FAILED: ${{ needs.activation.outputs.stale_lock_file_failed }} - GH_AW_GROUP_REPORTS: "false" - GH_AW_FAILURE_REPORT_AS_ISSUE: "true" - GH_AW_MISSING_TOOL_REPORT_AS_FAILURE: "true" - GH_AW_MISSING_DATA_REPORT_AS_FAILURE: "true" - GH_AW_TIMEOUT_MINUTES: "180" - GH_AW_MAX_EFFECTIVE_TOKENS: "25000000" - with: - github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/handle_agent_failure.cjs'); - await main(); - - safe_outputs: - needs: - - activation - - agent - if: (!cancelled()) && needs.agent.result != 'skipped' - runs-on: ubuntu-slim - permissions: - contents: read - issues: write - timeout-minutes: 15 - env: - GH_AW_CALLER_WORKFLOW_ID: "${{ github.repository }}/fstar-master-build" - GH_AW_EFFECTIVE_TOKENS: ${{ needs.agent.outputs.effective_tokens }} - GH_AW_ENGINE_ID: "copilot" - GH_AW_ENGINE_MODEL: ${{ needs.agent.outputs.model }} - GH_AW_ENGINE_VERSION: "1.0.55" - GH_AW_WORKFLOW_ID: "fstar-master-build" - GH_AW_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/fstar-master-build.md" - outputs: - code_push_failure_count: ${{ steps.process_safe_outputs.outputs.code_push_failure_count }} - code_push_failure_errors: ${{ steps.process_safe_outputs.outputs.code_push_failure_errors }} - create_discussion_error_count: ${{ steps.process_safe_outputs.outputs.create_discussion_error_count }} - create_discussion_errors: ${{ steps.process_safe_outputs.outputs.create_discussion_errors }} - created_issue_number: ${{ steps.process_safe_outputs.outputs.created_issue_number }} - created_issue_url: ${{ steps.process_safe_outputs.outputs.created_issue_url }} - process_safe_outputs_processed_count: ${{ steps.process_safe_outputs.outputs.processed_count }} - process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }} - steps: - - name: Setup Scripts - id: setup - uses: github/gh-aw-actions/setup@v0.77.5 - with: - destination: ${{ runner.temp }}/gh-aw/actions - job-name: ${{ github.job }} - trace-id: ${{ needs.activation.outputs.setup-trace-id }} - parent-span-id: ${{ needs.activation.outputs.setup-parent-span-id || needs.activation.outputs.setup-span-id }} - env: - GH_AW_SETUP_WORKFLOW_NAME: "Build FStar master with Z3 master" - GH_AW_CURRENT_WORKFLOW_REF: ${{ github.repository }}/.github/workflows/fstar-master-build.lock.yml@${{ github.ref }} - GH_AW_INFO_VERSION: "1.0.55" - GH_AW_INFO_AWF_VERSION: "v0.25.58" - GH_AW_INFO_ENGINE_ID: "copilot" - - name: Download agent output artifact - id: download-agent-output - continue-on-error: true - uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 - with: - name: agent - path: /tmp/gh-aw/ - - name: Setup agent output environment variable - id: setup-agent-output-env - if: steps.download-agent-output.outcome == 'success' - run: | - mkdir -p /tmp/gh-aw/ - find "/tmp/gh-aw/" -type f -print - echo "GH_AW_AGENT_OUTPUT=/tmp/gh-aw/agent_output.json" >> "$GITHUB_OUTPUT" - - name: Configure GH_HOST for enterprise compatibility - id: ghes-host-config - shell: bash - run: | - # Derive GH_HOST from GITHUB_SERVER_URL so the gh CLI targets the correct - # GitHub instance (GHES/GHEC). On github.com this is a harmless no-op. - GH_HOST="${GITHUB_SERVER_URL#https://}" - GH_HOST="${GH_HOST#http://}" - echo "GH_HOST=${GH_HOST}" >> "$GITHUB_ENV" - - name: Process Safe Outputs - id: process_safe_outputs - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - GH_AW_AGENT_OUTPUT: ${{ steps.setup-agent-output-env.outputs.GH_AW_AGENT_OUTPUT }} - GH_AW_COMMENT_ID: ${{ needs.activation.outputs.comment_id }} - GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com" - GITHUB_SERVER_URL: ${{ github.server_url }} - GITHUB_API_URL: ${{ github.api_url }} - GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_issue\":{\"labels\":[\"fstar-master-build\"],\"max\":1,\"title_prefix\":\"[fstar-master-build]\"}}" - with: - github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} - script: | - const { setupGlobals } = require('${{ runner.temp }}/gh-aw/actions/setup_globals.cjs'); - setupGlobals(core, github, context, exec, io, getOctokit); - const { main } = require('${{ runner.temp }}/gh-aw/actions/safe_output_handler_manager.cjs'); - await main(); - - name: Upload Safe Outputs Items - if: always() - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 - with: - name: safe-outputs-items - path: | - /tmp/gh-aw/safe-output-items.jsonl - /tmp/gh-aw/temporary-id-map.json - if-no-files-found: ignore - diff --git a/.github/workflows/fstar-master-build.md b/.github/workflows/fstar-master-build.md deleted file mode 100644 index fad78d0d5..000000000 --- a/.github/workflows/fstar-master-build.md +++ /dev/null @@ -1,117 +0,0 @@ ---- -description: Build Z3 master and then build FStar master using that Z3 build -on: - schedule: daily - workflow_dispatch: -permissions: read-all -network: defaults -tools: - bash: true -timeout-minutes: 180 -steps: - - name: Checkout Z3 master - uses: actions/checkout@v6.0.2 - with: - ref: master - fetch-depth: 1 - persist-credentials: false ---- - -# Build FStar master with Z3 master - -You are an AI build agent. Build the latest `master` branch of Z3, then build the latest `master` branch of FStar using the Z3 you just built. - -## Constraints - -- Use `${{ github.workspace }}` as the workspace root. -- Put temporary files under `/tmp/gh-aw/agent`. -- Use only the Z3 built in this workflow when building FStar. -- Fail fast with clear error messages if any phase fails. - -## Phase 1: Build Z3 master - -```bash -set -euo pipefail - -cd "${{ github.workspace }}" - -echo "Building Z3 from branch: $(git rev-parse --abbrev-ref HEAD)" -git rev-parse HEAD - -sudo apt-get update -y -sudo apt-get install -y cmake ninja-build python3 git curl unzip - -cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release -ninja -C build/release z3 - -"${{ github.workspace }}/build/release/z3" --version | tee /tmp/gh-aw/agent/z3-version.txt -``` - -Extract the numeric version string from the `z3 --version` output and store it in `Z3_VERSION` (for example, `4.15.4`). - -## Phase 2: Prepare PATH aliases for FStar - -FStar expects versioned Z3 command names on PATH. Create local aliases pointing to the Z3 binary from Phase 1. - -```bash -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 -export PATH="/tmp/gh-aw/agent/z3-bin:$PATH" - -z3 --version -z3-4.8.5 --version -z3-4.13.3 --version -``` - -## Phase 3: Clone and build FStar master - -```bash -set -euo pipefail - -mkdir -p /tmp/gh-aw/agent -rm -rf /tmp/gh-aw/agent/FStar - -git clone --depth=1 --branch master https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar -cd /tmp/gh-aw/agent/FStar - -echo "FStar commit: $(git rev-parse HEAD)" - -sudo apt-get update -y -sudo apt-get install -y opam m4 pkg-config libgmp-dev - -opam init --disable-sandboxing --yes -OPAM_SWITCH=4.14.2 -opam switch create "$OPAM_SWITCH" --yes || opam switch "$OPAM_SWITCH" -eval "$(opam env --switch=$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)" -if [ -z "$Z3_VERSION" ]; then - echo "ERROR: could not parse Z3 version from /tmp/gh-aw/agent/z3-version.txt" - exit 1 -fi - -echo "Using Z3 version override: $Z3_VERSION" -PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION" make -j"$(nproc)" -``` - -## Phase 4: Verify artifacts and report - -```bash -set -euo pipefail - -test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe -/tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt - -echo "SUCCESS: built Z3 master and FStar master with that Z3" -``` - -## Usage - -- This workflow is scheduled daily and can also be started manually. -- It checks out Z3 `master`, builds `build/release/z3`, then clones FStar `master` and builds it using that Z3. 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 03/13] 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 + } + ); From 69c3b2e5a429c37317be62e3f7e3ed3691af6eaf Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 13:20:12 -0700 Subject: [PATCH 04/13] fix(ci): initialize FStar submodules in fstar-master-build workflow (#9746) 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> --- .github/workflows/fstar-master-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 64a9ee89b..a3fd90c0e 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -89,7 +89,7 @@ jobs: 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 + 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 From 2f280a7baf652bfe6dfbf5c6bbd69f5852c75080 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 13:23:44 -0700 Subject: [PATCH 05/13] =?UTF-8?q?sls=5Fseq=5Fplugin:=20fix=20`break`=20?= =?UTF-8?q?=E2=86=92=20`continue`=20in=20`add=5Fsubstr=5Fedit=5Fupdates`?= =?UTF-8?q?=20(#9735)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `add_substr_edit_updates` uses a `HashSet` to deduplicate substrings of `val_other`, but on a duplicate hit it `break`s the inner loop instead of skipping just that entry. This causes all longer substrings from the same starting position to be silently dropped as repair candidates. ## Change - **`src/ast/sls/sls_seq_plugin.cpp`** — replace `break` with `continue` in the inner substring-enumeration loop. ```cpp // Before — exits the inner loop on first duplicate, missing e.g. "ab" in "aab" if (set.contains(sub)) break; // After — skips only the duplicate, continues with longer substrings at same offset if (set.contains(sub)) continue; ``` For `val_other = "aab"`, the old code never proposed `"ab"` (i=1, j=2) as a repair candidate because the duplicate `"a"` (i=1, j=1) terminated the inner loop prematurely. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/sls/sls_seq_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 0221e9f1d..5563ade51 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -753,7 +753,7 @@ namespace sls { for (unsigned j = 1; j <= val_other.length() - i; ++j) { zstring sub = val_other.extract(i, j); if (set.contains(sub)) - break; + continue; set.insert(sub); } } From cf58fa027d3af2574d9fad14c4718e7970e765bf Mon Sep 17 00:00:00 2001 From: Julien Stephan Date: Sat, 6 Jun 2026 22:24:19 +0200 Subject: [PATCH 06/13] python: make Statistics doctests robust to optional ":time" counter (#9729) The doctests for Statistics.__len__ and Statistics.__getitem__ in src/api/python/z3/z3.py asserted a fixed counter count (len(st) == 7). This is fragile because the ":time" entry is only added to statistics when the elapsed wall-clock time of check() is non-zero (see collect_timer_stats in src/solver/check_sat_result.h). On fast native builds, ":time" rounds to 0 and is omitted; under slow environments (e.g. riscv64 under qemu emulation), it becomes non-zero and is included, changing len(st). Fix this by checking the presence of statistics rather than an exact count. Signed-off-by: Julien Stephan --- src/api/python/z3/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 34eb9f5f8..c8574f560 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7396,8 +7396,8 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> len(st) - 7 + >>> len(st) > 0 + True """ return int(Z3_stats_size(self.ctx.ref(), self.stats)) @@ -7410,8 +7410,8 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> len(st) - 7 + >>> len(st) > 0 + True >>> st[0] ('nlsat propagations', 2) >>> st[1] From d5779a6993988b7c167817b91d3b26f2e7ee94ea Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 13:26:01 -0700 Subject: [PATCH 07/13] sls_seq_plugin: remove hard aborts in `is_sat` for `str.len` and `seq.last_indexof` (#9736) `src/ast/sls/sls_seq_plugin.cpp::is_sat()` had two unconditional abort paths (`VERIFY(false)` and `NOT_IMPLEMENTED_YET()`) reachable from valid string formulas under SLS. This changes those paths to graceful repair/fail behavior so SLS can continue search instead of terminating the process. - **Length coherence fallback no longer aborts** - Replaced the terminal `VERIFY(false)` in the `str.len` coherence block with a normal `return false` repair failure path. - Effect: failed local repair is propagated to the outer SLS loop instead of crashing. - **Implemented `seq.last_indexof` coherence handling** - Replaced `NOT_IMPLEMENTED_YET()` with concrete coherence logic: - read current `x`, `y`, and `e`, - compute `actual = sx.last_indexof(sy)`, - update `e` when `e != actual`, - otherwise continue. - Effect: formulas containing `seq.last_indexof` are handled in SLS coherence checks instead of aborting. - **No new hard-abort behavior introduced** - In the new `last_index` block, non-numeral `e` is handled by graceful `return false` (repair failure), not assertion abort. ```cpp if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) { auto sx = strval0(x), sy = strval0(y); rational val_e; if (!a.is_numeral(ctx.get_value(e), val_e)) return false; rational actual(sx.last_indexof(sy)); if (val_e == actual) continue; update(e, actual); return false; } ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/sls/sls_seq_plugin.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 5563ade51..f516b2948 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -172,9 +172,7 @@ namespace sls { return false; if (r > sx.length() && update(x, sx + zstring(random_char()))) return false; - // This case seems to imply unsat - verbose_stream() << "The input might be unsat\n"; // example to trigger: (assert (and (>= (str.len X) 2) (= (str.substr X 0 1) ""))) - VERIFY(false); + // Both updates failed. Treat as unsatisfied and let outer search continue. return false; } @@ -198,8 +196,16 @@ namespace sls { return false; } if (seq.str.is_last_index(e, x, y) && seq.is_string(x->get_sort())) { - // TODO - NOT_IMPLEMENTED_YET(); + auto sx = strval0(x); + auto sy = strval0(y); + rational val_e; + if (!a.is_numeral(ctx.get_value(e), val_e)) + return false; + rational actual(sx.last_indexof(sy)); + if (val_e == actual) + continue; + update(e, actual); + return false; } if (seq.str.is_stoi(e, x) && seq.is_string(x->get_sort())) { auto sx = strval0(x); From 241c6211d6e0da7dd4ef8904314aa3db0775db30 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 6 Jun 2026 15:26:49 -0700 Subject: [PATCH 08/13] Fix build-and-report failure by removing unsupported default FStar HO-matching flag (#9748) 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> --- .github/workflows/fstar-master-build.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index a3fd90c0e..518c67ec4 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -26,9 +26,9 @@ on: required: false default: "4.14.2" fstar_otherflags: - description: "Extra FStar OTHERFLAGS (example: --smt.ho_matching true)" + description: "Extra FStar OTHERFLAGS" required: false - default: "--smt.ho_matching true" + default: "" discussion_category: description: Discussion category name required: false @@ -52,7 +52,7 @@ jobs: 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' }} + FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '' }} DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }} steps: - name: Checkout Z3 From 1f5132c396774d76dadbd64dc79c4d8b74d36cdf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jun 2026 14:17:25 -0700 Subject: [PATCH 09/13] refactor solver to include settable stats --- src/cmd_context/tactic_cmds.cpp | 4 +++- src/muz/spacer/spacer_iuc_solver.cpp | 2 +- src/muz/spacer/spacer_iuc_solver.h | 2 +- src/opt/opt_context.cpp | 2 +- src/opt/opt_context.h | 2 +- src/opt/opt_sls_solver.h | 2 +- src/opt/opt_solver.cpp | 2 +- src/opt/opt_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/sat_solver/sat_smt_solver.cpp | 2 +- src/smt/smt_solver.cpp | 2 +- src/solver/check_sat_result.cpp | 3 --- src/solver/check_sat_result.h | 18 +++++++++++++++--- src/solver/combined_solver.cpp | 2 +- src/solver/simplifier_solver.cpp | 2 +- src/solver/slice_solver.cpp | 2 +- src/solver/solver_pool.cpp | 2 +- src/solver/tactic2solver.cpp | 11 ++++++----- src/tactic/fd_solver/bounded_int2bv_solver.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 2 +- src/tactic/fd_solver/pb2bv_solver.cpp | 2 +- src/tactic/fd_solver/smtfd_solver.cpp | 2 +- 22 files changed, 42 insertions(+), 30 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index c183a816c..f1a8dee04 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -232,7 +232,9 @@ public: } ctx.validate_check_sat_result(r); } - t.collect_statistics(result->m_stats); + statistics stats; + t.collect_statistics(stats); + result->add_statistics(stats); } if (ctx.produce_unsat_cores()) { diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 0bc72190b..4bdb2f414 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -185,7 +185,7 @@ namespace spacer { return m_base_defs.is_proxy (a, def); } - void iuc_solver::collect_statistics (statistics &st) const { + void iuc_solver::collect_statistics_core (statistics &st) const { m_solver.collect_statistics (st); st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds()); st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds()); diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index cdf355f03..18ff4da34 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -147,7 +147,7 @@ public: /* check_sat_result interface */ - void collect_statistics(statistics &st) const override ; + void collect_statistics_core(statistics &st) const override ; virtual void reset_statistics(); void get_unsat_core(expr_ref_vector &r) override; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 0b79f6a31..b3a1661d6 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1745,7 +1745,7 @@ namespace opt { m_pareto1 = p != nullptr; } - void context::collect_statistics(statistics& stats) const { + void context::collect_statistics_core(statistics& stats) const { if (m_solver) m_solver->collect_statistics(stats); if (m_simplify) diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 2d6c329c0..95bb33d86 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -235,7 +235,7 @@ namespace opt { void get_model_core(model_ref& _m) override; void get_box_model(model_ref& _m, unsigned index) override; void fix_model(model_ref& _m) override; - void collect_statistics(statistics& stats) const override; + void collect_statistics_core(statistics& stats) const override; proof* get_proof_core() override { return nullptr; } void get_labels(svector & r) override; void get_unsat_core(expr_ref_vector & r) override; diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index c7a0cd998..a360de329 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -66,7 +66,7 @@ namespace opt { virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } - virtual void collect_statistics(statistics & st) const { + virtual void collect_statistics_core(statistics & st) const { m_solver->collect_statistics(st); if (m_bvsls) m_bvsls->collect_statistics(st); if (m_pbsls) m_pbsls->collect_statistics(st); diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index af19f9182..586f22698 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -76,7 +76,7 @@ namespace opt { m_context.collect_param_descrs(r); } - void opt_solver::collect_statistics(statistics & st) const { + void opt_solver::collect_statistics_core(statistics & st) const { m_context.collect_statistics(st); } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 74da51b96..d11e97520 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -89,7 +89,7 @@ namespace opt { solver* translate(ast_manager& m, params_ref const& p) override; void updt_params(params_ref const& p) override; void collect_param_descrs(param_descrs & r) override; - void collect_statistics(statistics & st) const override; + void collect_statistics_core(statistics & st) const override; void assert_expr_core(expr * t) override; void push_core() override; void pop_core(unsigned n) override; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 11b5c771d..2a98bc3ae 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -387,7 +387,7 @@ public: if (p1.euf() && !get_euf()) ensure_euf(); } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { if (m_preprocess) m_preprocess->collect_statistics(st); m_solver.collect_statistics(st); } diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 8548749be..5c960d7da 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -334,7 +334,7 @@ public: ensure_euf(); } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { m_solver.collect_statistics(st); } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e82f4277c..d1e5e5a6b 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -142,7 +142,7 @@ namespace { insert_ctrl_c(r); } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { m_context.collect_statistics(st); } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 1f86ca4f2..ad528644d 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -70,9 +70,6 @@ simple_check_sat_result::simple_check_sat_result(ast_manager & m): m_proof(m) { } -void simple_check_sat_result::collect_statistics(statistics & st) const { - st.copy(m_stats); -} void simple_check_sat_result::get_unsat_core(expr_ref_vector & r) { if (m_status == l_false) { diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 8a48d3277..0db1c3d1a 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -46,6 +46,8 @@ protected: lbool m_status = l_undef; model_converter_ref m_mc0; double m_time = 0; + statistics m_stats; + public: check_sat_result(ast_manager& m): m(m), m_log(m), m_proof(m) {} virtual ~check_sat_result() = default; @@ -53,7 +55,18 @@ public: void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } lbool set_status(lbool r) { return m_status = r; } lbool status() const { return m_status; } - virtual void collect_statistics(statistics & st) const = 0; + void collect_statistics(statistics &st) const { + collect_statistics_core(st); + st.copy(m_stats); + } + void add_statistics(statistics const &st) { + m_stats.copy(st); + } + void reset_statistics() { + m_stats.reset(); + } + + virtual void collect_statistics_core(statistics &st) const = 0; virtual void get_unsat_core(expr_ref_vector & r) = 0; void set_model_converter(model_converter* mc) { m_mc0 = mc; } model_converter* mc0() const { return m_mc0.get(); } @@ -92,7 +105,6 @@ public: \brief Very simple implementation of the check_sat_result object. */ struct simple_check_sat_result : public check_sat_result { - statistics m_stats; model_ref m_model; expr_ref_vector m_core; proof_ref m_proof; @@ -100,9 +112,9 @@ struct simple_check_sat_result : public check_sat_result { simple_check_sat_result(ast_manager & m); ast_manager& get_manager() const override { return m_proof.get_manager(); } - void collect_statistics(statistics & st) const override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & m) override; + void collect_statistics_core(statistics &st) const override {} proof * get_proof_core() override; std::string reason_unknown() const override; void get_labels(svector & r) override; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 44bda3ddf..f324b64b2 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -290,7 +290,7 @@ public: return m_solver1->display(out, n, es); } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { m_solver2->collect_statistics(st); if (m_use_solver1_results) m_solver1->collect_statistics(st); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index c75d574eb..79f5ea44e 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -229,7 +229,7 @@ public: return s->check_sat_core(num_assumptions, _assumptions.data()); } - void collect_statistics(statistics& st) const override { + void collect_statistics_core(statistics& st) const override { s->collect_statistics(st); m_preprocess.collect_statistics(st); } diff --git a/src/solver/slice_solver.cpp b/src/solver/slice_solver.cpp index ee95cfa94..e300d83af 100644 --- a/src/solver/slice_solver.cpp +++ b/src/solver/slice_solver.cpp @@ -319,7 +319,7 @@ public: return s->check_sat_core(num_assumptions, assumptions); } - void collect_statistics(statistics& st) const override { s->collect_statistics(st); } + void collect_statistics_core(statistics& st) const override { s->collect_statistics(st); } void get_model_core(model_ref& mdl) override { s->get_model_core(mdl); } diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index c98a2b57a..3cf97ce3b 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -83,7 +83,7 @@ public: void pop_params() override {m_base->pop_params();} void collect_param_descrs(param_descrs & r) override { m_base->collect_param_descrs(r); } - void collect_statistics(statistics & st) const override { m_base->collect_statistics(st); } + void collect_statistics_core(statistics & st) const override { m_base->collect_statistics(st); } unsigned get_num_assertions() const override { return m_base->get_num_assertions(); } expr * get_assertion(unsigned idx) const override { return m_base->get_assertion(idx); } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 7fd5fec56..1ed4d995e 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -49,7 +49,7 @@ class tactic2solver : public solver_na2as { bool m_produce_models; bool m_produce_proofs; bool m_produce_unsat_cores; - statistics m_stats; +// statistics m_stats; bool m_minimizing = false; public: @@ -70,7 +70,7 @@ public: void pop_core(unsigned n) override; lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override; - void collect_statistics(statistics & st) const override; + void collect_statistics_core(statistics & st) const override; void get_unsat_core(expr_ref_vector & r) override; void get_model_core(model_ref & m) override; proof * get_proof_core() override; @@ -284,8 +284,9 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as m_result->m_unknown = ex.what(); m_result->m_proof = pr; } - m_tactic->collect_statistics(m_result->m_stats); - m_tactic->collect_statistics(m_stats); + statistics stats; + m_tactic->collect_statistics(stats); + m_result->add_statistics(stats); m_result->m_model = md; m_result->m_proof = pr; if (m_produce_unsat_cores) { @@ -311,7 +312,7 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) { } -void tactic2solver::collect_statistics(statistics & st) const { +void tactic2solver::collect_statistics_core(statistics & st) const { st.copy(m_stats); if (m_stats.size() == 0 && m_tactic) m_tactic->collect_statistics(st); diff --git a/src/tactic/fd_solver/bounded_int2bv_solver.cpp b/src/tactic/fd_solver/bounded_int2bv_solver.cpp index 8ef39d0af..28cb5823a 100644 --- a/src/tactic/fd_solver/bounded_int2bv_solver.cpp +++ b/src/tactic/fd_solver/bounded_int2bv_solver.cpp @@ -159,7 +159,7 @@ public: void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); } void set_produce_models(bool f) override { m_solver->set_produce_models(f); } void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); } - void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); } + void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); } void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); } void set_phase(expr* e) override { m_solver->set_phase(e); } phase* get_phase() override { return m_solver->get_phase(); } diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 061f67010..d420aa796 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -85,7 +85,7 @@ public: void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); } void set_produce_models(bool f) override { m_solver->set_produce_models(f); } void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); } - void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); } + void collect_statistics_core(statistics & st) const override { m_solver->collect_statistics(st); } void get_unsat_core(expr_ref_vector & r) override { m_solver->get_unsat_core(r); } void set_phase(expr* e) override { m_solver->set_phase(e); } phase* get_phase() override { return m_solver->get_phase(); } diff --git a/src/tactic/fd_solver/pb2bv_solver.cpp b/src/tactic/fd_solver/pb2bv_solver.cpp index 7bc0f27dd..12ac45042 100644 --- a/src/tactic/fd_solver/pb2bv_solver.cpp +++ b/src/tactic/fd_solver/pb2bv_solver.cpp @@ -82,7 +82,7 @@ public: void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); m_rewriter.collect_param_descrs(r);} void set_produce_models(bool f) override { m_solver->set_produce_models(f); } void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { m_rewriter.collect_statistics(st); m_solver->collect_statistics(st); } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 8b765a04e..d20d5b706 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -2032,7 +2032,7 @@ namespace smtfd { void set_produce_models(bool f) override { } void set_progress_callback(progress_callback * callback) override { } - void collect_statistics(statistics & st) const override { + void collect_statistics_core(statistics & st) const override { if (m_fd_sat_solver) { m_fd_sat_solver->collect_statistics(st); m_fd_core_solver->collect_statistics(st); From 59bb444694b9e6981d3fc386164a8ebe0c99900d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jun 2026 14:18:21 -0700 Subject: [PATCH 10/13] include skills --- .github/agents/agentic-workflows.md | 224 ++++++++++++++++++++++ .github/mcp.json | 11 ++ .github/skills/agentic-workflows/SKILL.md | 35 ++++ 3 files changed, 270 insertions(+) create mode 100644 .github/agents/agentic-workflows.md create mode 100644 .github/mcp.json create mode 100644 .github/skills/agentic-workflows/SKILL.md diff --git a/.github/agents/agentic-workflows.md b/.github/agents/agentic-workflows.md new file mode 100644 index 000000000..9a2e0130e --- /dev/null +++ b/.github/agents/agentic-workflows.md @@ -0,0 +1,224 @@ +--- +name: Agentic Workflows +description: GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing. +disable-model-invocation: true +--- + +# GitHub Agentic Workflows Agent + +This agent helps you work with **GitHub Agentic Workflows (gh-aw)**, a CLI extension for creating AI-powered workflows in natural language using markdown files. + +## What This Agent Does + +This is a **dispatcher agent** that routes your request to the appropriate specialized prompt based on your task: + +- **Creating new workflows**: Routes to `create` prompt +- **Updating existing workflows**: Routes to `update` prompt +- **Debugging workflows**: Routes to `debug` prompt +- **Upgrading workflows**: Routes to `upgrade-agentic-workflows` prompt +- **Creating report-generating workflows**: Routes to `report` prompt — consult this whenever the workflow posts status updates, audits, analyses, or any structured output as issues, discussions, or comments +- **Creating shared components**: Routes to `create-shared-agentic-workflow` prompt +- **Fixing Dependabot PRs**: Routes to `dependabot` prompt — use this when Dependabot opens PRs that modify generated manifest files (`.github/workflows/package.json`, `.github/workflows/requirements.txt`, `.github/workflows/go.mod`). Never merge those PRs directly; instead update the source `.md` files and rerun `gh aw compile --dependabot` to bundle all fixes +- **Analyzing test coverage**: Routes to `test-coverage` prompt — consult this whenever the workflow reads, analyzes, or reports on test coverage data from PRs or CI runs +- **Rendering ASCII charts in markdown**: Routes to `asciicharts` guide — consult this whenever the workflow needs compact charts that render reliably in GitHub issues, comments, or discussions +- **CLI commands and triggering workflows**: Routes to `cli-commands` guide — consult this whenever the user asks how to run, compile, debug, or manage workflows from the command line, or when they need the MCP tool equivalent of a `gh aw` command +- **Reducing token consumption / cost optimization**: Routes to `token-optimization` guide — consult this whenever the user asks how to reduce token usage, lower costs, speed up workflows, or measure the impact of prompt changes with experiments +- **Choosing workflow architectures and design patterns**: Routes to `patterns` guide — consult this whenever the user asks for strategy, architecture, operating models, or pattern selection for agentic workflows + +Workflows may optionally include: + +- **Project tracking / monitoring** (GitHub Projects updates, status reporting) +- **Orchestration / coordination** (one workflow assigning agents or dispatching and coordinating other workflows) + +## Files This Applies To + +- Workflow files: `.github/workflows/*.md` and `.github/workflows/**/*.md` +- Workflow lock files: `.github/workflows/*.lock.yml` +- Shared components: `.github/workflows/shared/*.md` +- Configuration: `.github/aw/github-agentic-workflows.md` + +## Problems This Solves + +- **Workflow Creation**: Design secure, validated agentic workflows with proper triggers, tools, and permissions +- **Workflow Debugging**: Analyze logs, identify missing tools, investigate failures, and fix configuration issues +- **Version Upgrades**: Migrate workflows to new gh-aw versions, apply codemods, fix breaking changes +- **Component Design**: Create reusable shared workflow components that wrap MCP servers + +## How to Use + +When you interact with this agent, it will: + +1. **Understand your intent** - Determine what kind of task you're trying to accomplish +2. **Route to the right prompt** - Load the specialized prompt file for your task +3. **Execute the task** - Follow the detailed instructions in the loaded prompt + +## Available Prompts + +### Create New Workflow +**Load when**: User wants to create a new workflow from scratch, add automation, or design a workflow that doesn't exist yet + +**Prompt file**: `.github/aw/create-agentic-workflow.md` + +**Use cases**: +- "Create a workflow that triages issues" +- "I need a workflow to label pull requests" +- "Design a weekly research automation" + +### Update Existing Workflow +**Load when**: User wants to modify, improve, or refactor an existing workflow + +**Prompt file**: `.github/aw/update-agentic-workflow.md` + +**Use cases**: +- "Add web-fetch tool to the issue-classifier workflow" +- "Update the PR reviewer to use discussions instead of issues" +- "Improve the prompt for the weekly-research workflow" + +### Debug Workflow +**Load when**: User needs to investigate, audit, debug, or understand a workflow, troubleshoot issues, analyze logs, or fix errors + +**Prompt file**: `.github/aw/debug-agentic-workflow.md` + +**Use cases**: +- "Why is this workflow failing?" +- "Analyze the logs for workflow X" +- "Investigate missing tool calls in run #12345" + +### Upgrade Agentic Workflows +**Load when**: User wants to upgrade workflows to a new gh-aw version or fix deprecations + +**Prompt file**: `.github/aw/upgrade-agentic-workflows.md` + +**Use cases**: +- "Upgrade all workflows to the latest version" +- "Fix deprecated fields in workflows" +- "Apply breaking changes from the new release" + +### Create a Report-Generating Workflow +**Load when**: The workflow being created or updated produces reports — recurring status updates, audit summaries, analyses, or any structured output posted as a GitHub issue, discussion, or comment + +**Prompt file**: `.github/aw/report.md` + +**Use cases**: +- "Create a weekly CI health report" +- "Post a daily security audit to Discussions" +- "Add a status update comment to open PRs" + +### Create Shared Agentic Workflow +**Load when**: User wants to create a reusable workflow component or wrap an MCP server + +**Prompt file**: `.github/aw/create-shared-agentic-workflow.md` + +**Use cases**: +- "Create a shared component for Notion integration" +- "Wrap the Slack MCP server as a reusable component" +- "Design a shared workflow for database queries" + +### Fix Dependabot PRs +**Load when**: User needs to close or fix open Dependabot PRs that update dependencies in generated manifest files (`.github/workflows/package.json`, `.github/workflows/requirements.txt`, `.github/workflows/go.mod`) + +**Prompt file**: `.github/aw/dependabot.md` + +**Use cases**: +- "Fix the open Dependabot PRs for npm dependencies" +- "Bundle and close the Dependabot PRs for workflow dependencies" +- "Update @playwright/test to fix the Dependabot PR" + +### Analyze Test Coverage +**Load when**: The workflow reads, analyzes, or reports test coverage — whether triggered by a PR, a schedule, or a slash command. Always consult this prompt before designing the coverage data strategy. + +**Prompt file**: `.github/aw/test-coverage.md` + +**Use cases**: +- "Create a workflow that comments coverage on PRs" +- "Analyze coverage trends over time" +- "Add a coverage gate that blocks PRs below a threshold" + +### CLI Commands Reference +**Load when**: The user asks how to run, compile, debug, or manage workflows from the command line; needs the MCP tool equivalent of a `gh aw` command; or is in a restricted environment (e.g., Copilot Cloud) without direct CLI access. + +**Reference file**: `.github/aw/cli-commands.md` + +**Use cases**: +- "How do I trigger workflow X on the main branch?" +- "What's the MCP equivalent of `gh aw logs`?" +- "I'm in Copilot Cloud — how do I compile a workflow?" +- "Show me all available gh aw commands" + +### Token Consumption Optimization +**Load when**: The user asks how to reduce token usage, lower workflow costs, make a workflow faster or cheaper, or measure the impact of prompt or configuration changes. + +**Reference file**: `.github/aw/token-optimization.md` + +**Use cases**: +- "How do I reduce the token cost of this workflow?" +- "My workflow is too expensive — how do I optimize it?" +- "How do I compare token usage between two runs?" +- "Should I use gh-proxy or the MCP server?" +- "How do I use sub-agents to reduce costs?" +- "How do I measure the impact of a prompt change?" + +### Workflow Pattern Selection +**Load when**: The user asks for architecture, strategy, operating model selection, or pattern recommendations for building agentic workflows. + +**Reference file**: `.github/aw/patterns.md` + +**Use cases**: +- "Which pattern should I use for multi-repo rollout?" +- "How should I structure this workflow architecture?" +- "What pattern fits slash-command triage?" +- "Should this be DispatchOps or DailyOps?" + +## Instructions + +When a user interacts with you: + +1. **Identify the task type** from the user's request +2. **Load the appropriate prompt** from the repository paths listed above +3. **Follow the loaded prompt's instructions** exactly +4. **If uncertain**, ask clarifying questions to determine the right prompt + +## Quick Reference + +```bash +# Initialize repository for agentic workflows +gh aw init + +# Generate the lock file for a workflow +gh aw compile [workflow-name] + +# Trigger a workflow on demand (preferred over gh workflow run) +gh aw run # interactive input collection +gh aw run --ref main # run on a specific branch + +# Debug workflow runs +gh aw logs [workflow-name] +gh aw audit + +# Upgrade workflows +gh aw fix --write +gh aw compile --validate +``` + +## Key Features of gh-aw + +- **Natural Language Workflows**: Write workflows in markdown with YAML frontmatter +- **AI Engine Support**: Copilot, Claude, Codex, or custom engines +- **MCP Server Integration**: Connect to Model Context Protocol servers for tools +- **Safe Outputs**: Structured communication between AI and GitHub API +- **Strict Mode**: Security-first validation and sandboxing +- **Shared Components**: Reusable workflow building blocks +- **Repo Memory**: Persistent git-backed storage for agents +- **Sandboxed Execution**: All workflows run in the Agent Workflow Firewall (AWF) sandbox, enabling full `bash` and `edit` tools by default + +## Important Notes + +- Always reference the instructions file at `.github/aw/github-agentic-workflows.md` for complete documentation +- Use the MCP tool `agentic-workflows` when running in GitHub Copilot Cloud +- Workflows must be compiled to `.lock.yml` files before running in GitHub Actions +- **Bash tools are enabled by default** - Don't restrict bash commands unnecessarily since workflows are sandboxed by the AWF +- Follow security best practices: minimal permissions, explicit network access, no template injection +- **Network configuration**: Use ecosystem identifiers (`node`, `python`, `go`, etc.) or explicit FQDNs in `network.allowed`. Bare shorthands like `npm` or `pypi` are **not** valid. See `.github/aw/network.md` for the full list of valid ecosystem identifiers and domain patterns. +- **Single-file output**: When creating a workflow, produce exactly **one** workflow `.md` file. Do not create separate documentation files (architecture docs, runbooks, usage guides, etc.). If documentation is needed, add a brief `## Usage` section inside the workflow file itself. +- **Triggering runs**: Always use `gh aw run ` to trigger a workflow on demand — not `gh workflow run .lock.yml`. `gh aw run` handles workflow resolution by short name, input parsing and validation, and correct run-tracking for agentic workflows. Use `--ref ` to run on a specific branch. +- **CLI commands reference**: For a complete guide on all `gh aw` commands and their MCP tool equivalents (for restricted environments), see `.github/aw/cli-commands.md` diff --git a/.github/mcp.json b/.github/mcp.json new file mode 100644 index 000000000..b953af263 --- /dev/null +++ b/.github/mcp.json @@ -0,0 +1,11 @@ +{ + "mcpServers": { + "github-agentic-workflows": { + "command": "gh", + "args": [ + "aw", + "mcp-server" + ] + } + } +} \ No newline at end of file diff --git a/.github/skills/agentic-workflows/SKILL.md b/.github/skills/agentic-workflows/SKILL.md new file mode 100644 index 000000000..40aa1a58f --- /dev/null +++ b/.github/skills/agentic-workflows/SKILL.md @@ -0,0 +1,35 @@ +--- +name: agentic-workflows +description: Route gh-aw workflow create/debug/upgrade requests to the right prompts. +--- + +# Agentic Workflows Router + +Use this skill when a user asks to create, update, debug, or upgrade GitHub Agentic Workflows in this repository. + +This skill is a dispatcher: identify the task type, load the matching `.github/aw/*.md` file, and follow it directly. Keep responses concise and ask a clarifying question if the correct prompt is unclear. + +Read only the files you need: +Load these files from `github/gh-aw` (they are not available locally). +- `.github/aw/create-agentic-workflow.md` +- `.github/aw/create-shared-agentic-workflow.md` +- `.github/aw/debug-agentic-workflow.md` +- `.github/aw/github-agentic-workflows.md` +- `.github/aw/update-agentic-workflow.md` +- `.github/aw/upgrade-agentic-workflows.md` + +After loading the matching workflow prompt, follow it directly: +- Create new workflows: `.github/aw/create-agentic-workflow.md` +- Update existing workflows: `.github/aw/update-agentic-workflow.md` +- Debug, audit, or investigate workflows: `.github/aw/debug-agentic-workflow.md` +- Upgrade workflows and fix deprecations: `.github/aw/upgrade-agentic-workflows.md` +- Create shared components or MCP wrappers: `.github/aw/create-shared-agentic-workflow.md` +- Create report-generating workflows: `.github/aw/report.md` +- Fix Dependabot manifest PRs: `.github/aw/dependabot.md` +- Analyze coverage workflows: `.github/aw/test-coverage.md` +- Render compact markdown charts: `.github/aw/asciicharts.md` +- Map CLI commands to MCP usage: `.github/aw/cli-commands.md` +- Choose workflow architecture and patterns: `.github/aw/patterns.md` +- Optimize token usage and cost: `.github/aw/token-optimization.md` + +When the task involves OTEL, OTLP, traces, observability backends, or telemetry-driven analysis, also read and follow `skills/otel-queries/SKILL.md` after loading the matching workflow prompt. From bbadf919e7308bc9a756fd4a2d4952b440dd1aae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 8 Jun 2026 09:51:46 -0700 Subject: [PATCH 11/13] Update fstar-master-build.yml --- .github/workflows/fstar-master-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 518c67ec4..4e90654d7 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -101,7 +101,7 @@ jobs: 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)" + 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 From 3bba379ddf523e7ae8c551bb559d61a58d358151 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 8 Jun 2026 10:04:34 -0700 Subject: [PATCH 12/13] Update fstar-master-build.yml --- .github/workflows/fstar-master-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 4e90654d7..c49f71975 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -28,7 +28,7 @@ on: fstar_otherflags: description: "Extra FStar OTHERFLAGS" required: false - default: "" + default: "--split_queries --log_failing_queries" discussion_category: description: Discussion category name required: false From 42e6ec5644009525c7373528c95a820561c94229 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 8 Jun 2026 10:30:37 -0700 Subject: [PATCH 13/13] Update fstar-master-build.yml --- .github/workflows/fstar-master-build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index c49f71975..4b674fc33 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -20,7 +20,7 @@ on: fstar_ref: description: FStar ref to checkout and build required: false - default: master + default: _nik_higher_order_smt fstar_opam_switch: description: OCaml switch for FStar build required: false @@ -28,7 +28,7 @@ on: fstar_otherflags: description: "Extra FStar OTHERFLAGS" required: false - default: "--split_queries --log_failing_queries" + default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery" discussion_category: description: Discussion category name required: false