From 488c9b1b3715fc535f9397aec899ba0160ad6099 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 6 Jun 2026 11:43:13 -0700 Subject: [PATCH] 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.