diff --git a/.github/workflows/fstar-master-build.lock.yml b/.github/workflows/fstar-master-build.lock.yml index 7a4350e69..fde80fbf3 100644 --- a/.github/workflows/fstar-master-build.lock.yml +++ b/.github/workflows/fstar-master-build.lock.yml @@ -1,5 +1,5 @@ -# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"b848fe30dfc98176eaac646426908d3ebf50f167961e0a4dcb6e7003263d48d1","body_hash":"c79e05b4b93a87f009893bf3519b4df5e359f8026120c64dff4e5d47fc9a183b","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/setup-node","sha":"48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e","version":"v6.4.0"},{"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"}]} +# 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"}]} # ___ _ _ # / _ \ | | (_) # | |_| | __ _ ___ _ __ | |_ _ ___ @@ -22,7 +22,7 @@ # # For more information: https://github.github.com/gh-aw/introduction/overview/ # -# Build latest FStar master using Z3 built from latest Z3 master +# Build Z3 master and then build FStar master using that Z3 build # # Secrets used: # - COPILOT_GITHUB_TOKEN @@ -35,7 +35,6 @@ # - actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1 # - actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 # - actions/github-script@v9 -# - actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0 # - actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 # - github/gh-aw-actions/setup@v0.77.5 # @@ -47,7 +46,7 @@ # - ghcr.io/github/github-mcp-server:v1.1.0 # - node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f -name: "Build Latest F* with Latest Z3" +name: "Build FStar master with Z3 master" on: schedule: - cron: "9 4 * * *" @@ -65,7 +64,7 @@ permissions: {} concurrency: group: "gh-aw-${{ github.workflow }}" -run-name: "Build Latest F* with Latest Z3" +run-name: "Build FStar master with Z3 master" jobs: activation: @@ -92,7 +91,7 @@ jobs: destination: ${{ runner.temp }}/gh-aw/actions job-name: ${{ github.job }} env: - GH_AW_SETUP_WORKFLOW_NAME: "Build Latest F* with Latest Z3" + 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" @@ -106,7 +105,7 @@ jobs: 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 Latest F* with Latest Z3" + 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" @@ -188,20 +187,23 @@ jobs: run: | bash "${RUNNER_TEMP}/gh-aw/actions/create_prompt_first.sh" { - cat << 'GH_AW_PROMPT_af92df500d7f7c80_EOF' + cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - GH_AW_PROMPT_af92df500d7f7c80_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_af92df500d7f7c80_EOF' + cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' - Tools: create_issue, create_discussion, missing_tool, missing_data, noop + 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_af92df500d7f7c80_EOF + GH_AW_PROMPT_4e12b9cf31810404_EOF cat "${RUNNER_TEMP}/gh-aw/prompts/mcp_cli_tools_prompt.md" - cat << 'GH_AW_PROMPT_af92df500d7f7c80_EOF' + cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' The following GitHub context information is available for this workflow: {{#if github.actor}} @@ -230,12 +232,12 @@ jobs: {{/if}} - GH_AW_PROMPT_af92df500d7f7c80_EOF + GH_AW_PROMPT_4e12b9cf31810404_EOF cat "${RUNNER_TEMP}/gh-aw/prompts/github_mcp_tools_with_safeoutputs_prompt.md" - cat << 'GH_AW_PROMPT_af92df500d7f7c80_EOF' + cat << 'GH_AW_PROMPT_4e12b9cf31810404_EOF' {{#runtime-import .github/workflows/fstar-master-build.md}} - GH_AW_PROMPT_af92df500d7f7c80_EOF + GH_AW_PROMPT_4e12b9cf31810404_EOF } > "$GH_AW_PROMPT" - name: Interpolate variables and render templates uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 @@ -352,7 +354,7 @@ jobs: 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 Latest F* with Latest Z3" + 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" @@ -448,49 +450,21 @@ jobs: 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_157b0989e46a4bff_EOF' - {"create_discussion":{"category":"agentic workflows","close_older_discussions":true,"expires":336,"fallback_to_issue":true,"max":1,"title_prefix":"[F* Build] "},"create_issue":{"labels":["build","fstar"],"max":1,"title_prefix":"[F* Build Failure] "},"create_report_incomplete_issue":{},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}} - GH_AW_SAFE_OUTPUTS_CONFIG_157b0989e46a4bff_EOF + 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_discussion": " CONSTRAINTS: Maximum 1 discussion(s) can be created. Title will be prefixed with \"[F* Build] \". Discussions will be created in category \"agentic workflows\".", - "create_issue": " CONSTRAINTS: Maximum 1 issue(s) can be created. Title will be prefixed with \"[F* Build Failure] \". Labels [\"build\" \"fstar\"] will be automatically added." + "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_discussion": { - "defaultMax": 1, - "fields": { - "body": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 65000, - "minLength": 64 - }, - "category": { - "type": "string", - "sanitize": true, - "maxLength": 128 - }, - "repo": { - "type": "string", - "maxLength": 256 - }, - "title": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 128 - } - } - }, "create_issue": { "defaultMax": 1, "fields": { @@ -526,79 +500,6 @@ jobs: "maxLength": 128 } } - }, - "missing_data": { - "defaultMax": 20, - "fields": { - "alternatives": { - "type": "string", - "sanitize": true, - "maxLength": 256 - }, - "context": { - "type": "string", - "sanitize": true, - "maxLength": 256 - }, - "data_type": { - "type": "string", - "sanitize": true, - "maxLength": 128 - }, - "reason": { - "type": "string", - "sanitize": true, - "maxLength": 256 - } - } - }, - "missing_tool": { - "defaultMax": 20, - "fields": { - "alternatives": { - "type": "string", - "sanitize": true, - "maxLength": 512 - }, - "reason": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 256 - }, - "tool": { - "type": "string", - "sanitize": true, - "maxLength": 128 - } - } - }, - "noop": { - "defaultMax": 1, - "fields": { - "message": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 65000 - } - } - }, - "report_incomplete": { - "defaultMax": 5, - "fields": { - "details": { - "type": "string", - "sanitize": true, - "maxLength": 65000 - }, - "reason": { - "required": true, - "type": "string", - "sanitize": true, - "maxLength": 1024 - } - } } } uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 @@ -686,7 +587,7 @@ jobs: 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_226c5fb482aaa3af_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs" + cat << GH_AW_MCP_CONFIG_bb501b6f2b1412ea_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs" { "mcpServers": { "github": { @@ -727,7 +628,7 @@ jobs: "payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}" } } - GH_AW_MCP_CONFIG_226c5fb482aaa3af_EOF + GH_AW_MCP_CONFIG_bb501b6f2b1412ea_EOF - name: Mount MCP servers as CLIs id: mount-mcp-clis continue-on-error: true @@ -752,7 +653,7 @@ jobs: - name: Execute GitHub Copilot CLI id: agentic_execution # Copilot CLI tool arguments (sorted): - timeout-minutes: 120 + timeout-minutes: 180 run: | set -o pipefail printf '%s' "$(date +%s%3N)" > /tmp/gh-aw/agent_cli_start_ms.txt @@ -957,8 +858,6 @@ jobs: /tmp/gh-aw/github_rate_limits.jsonl /tmp/gh-aw/safeoutputs.jsonl /tmp/gh-aw/agent_output.json - /tmp/gh-aw/aw-*.patch - /tmp/gh-aw/aw-*.bundle /tmp/gh-aw/awf-config.json /tmp/gh-aw/sandbox/firewall/logs/ /tmp/gh-aw/sandbox/firewall/audit/ @@ -969,7 +868,6 @@ jobs: needs: - activation - agent - - detection - safe_outputs if: > always() && (needs.agent.result != 'skipped' || needs.activation.outputs.lockdown_check_failed == 'true' || @@ -977,17 +875,11 @@ jobs: runs-on: ubuntu-slim permissions: contents: read - discussions: write issues: write concurrency: group: "gh-aw-conclusion-fstar-master-build" cancel-in-progress: false queue: max - outputs: - incomplete_count: ${{ steps.report_incomplete.outputs.incomplete_count }} - noop_message: ${{ steps.noop.outputs.noop_message }} - tools_reported: ${{ steps.missing_tool.outputs.tools_reported }} - total_count: ${{ steps.missing_tool.outputs.total_count }} steps: - name: Setup Scripts id: setup @@ -998,7 +890,7 @@ jobs: 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 Latest F* with Latest Z3" + 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" @@ -1017,79 +909,13 @@ jobs: 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: Process no-op messages - id: noop - 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_NOOP_MAX: "1" - GH_AW_WORKFLOW_NAME: "Build Latest F* with Latest Z3" - 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_NOOP_REPORT_AS_ISSUE: "false" - 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_noop_message.cjs'); - await main(); - - name: Log detection run - id: detection_runs - 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 Latest F* with Latest Z3" - 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_DETECTION_CONCLUSION: ${{ needs.detection.outputs.detection_conclusion }} - GH_AW_DETECTION_REASON: ${{ needs.detection.outputs.detection_reason }} - 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_detection_runs.cjs'); - await main(); - - name: Record missing tool - id: missing_tool - 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_MISSING_TOOL_CREATE_ISSUE: "true" - GH_AW_MISSING_TOOL_TITLE_PREFIX: "[missing tool]" - GH_AW_WORKFLOW_NAME: "Build Latest F* with Latest Z3" - GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/fstar-master-build.md" - 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/missing_tool.cjs'); - await main(); - - name: Record incomplete - id: report_incomplete - 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_REPORT_INCOMPLETE_CREATE_ISSUE: "true" - GH_AW_WORKFLOW_NAME: "Build Latest F* with Latest Z3" - GH_AW_WORKFLOW_SOURCE_URL: "${{ github.server_url }}/${{ github.repository }}/blob/${{ github.ref_name }}/.github/workflows/fstar-master-build.md" - 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/report_incomplete_handler.cjs'); - await main(); - 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 Latest F* with Latest Z3" + 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 }} @@ -1105,15 +931,13 @@ jobs: 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_CREATE_DISCUSSION_ERRORS: ${{ needs.safe_outputs.outputs.create_discussion_errors }} - GH_AW_CREATE_DISCUSSION_ERROR_COUNT: ${{ needs.safe_outputs.outputs.create_discussion_error_count }} 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: "120" + GH_AW_TIMEOUT_MINUTES: "180" GH_AW_MAX_EFFECTIVE_TOKENS: "25000000" with: github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }} @@ -1123,244 +947,24 @@ jobs: const { main } = require('${{ runner.temp }}/gh-aw/actions/handle_agent_failure.cjs'); await main(); - detection: - needs: - - activation - - agent - if: > - always() && needs.agent.result != 'skipped' && (needs.agent.outputs.output_types != '' || needs.agent.outputs.has_patch == 'true') - runs-on: ubuntu-latest - permissions: - contents: read - outputs: - detection_conclusion: ${{ steps.detection_conclusion.outputs.conclusion }} - detection_reason: ${{ steps.detection_conclusion.outputs.reason }} - detection_success: ${{ steps.detection_conclusion.outputs.success }} - 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 Latest F* with Latest Z3" - 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: Checkout repository for patch context - if: needs.agent.outputs.has_patch == 'true' - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - with: - persist-credentials: false - # --- Threat Detection --- - - name: Clean stale firewall files from agent artifact - run: | - rm -rf /tmp/gh-aw/sandbox/firewall/logs - rm -rf /tmp/gh-aw/sandbox/firewall/audit - - 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 - - name: Check if detection needed - id: detection_guard - if: always() - env: - OUTPUT_TYPES: ${{ needs.agent.outputs.output_types }} - HAS_PATCH: ${{ needs.agent.outputs.has_patch }} - run: | - if [[ -n "$OUTPUT_TYPES" || "$HAS_PATCH" == "true" ]]; then - echo "run_detection=true" >> "$GITHUB_OUTPUT" - echo "Detection will run: output_types=$OUTPUT_TYPES, has_patch=$HAS_PATCH" - else - echo "run_detection=false" >> "$GITHUB_OUTPUT" - echo "Detection skipped: no agent outputs or patches to analyze" - fi - - name: Clear MCP Config for detection - if: always() && steps.detection_guard.outputs.run_detection == 'true' - run: | - rm -f "${RUNNER_TEMP}/gh-aw/mcp-config/mcp-servers.json" - rm -f /home/runner/.copilot/mcp-config.json - rm -f "$GITHUB_WORKSPACE/.gemini/settings.json" - - name: Prepare threat detection files - if: always() && steps.detection_guard.outputs.run_detection == 'true' - run: | - mkdir -p /tmp/gh-aw/threat-detection/aw-prompts - cp /tmp/gh-aw/aw-prompts/prompt.txt /tmp/gh-aw/threat-detection/aw-prompts/prompt.txt 2>/dev/null || true - if [ ! -s /tmp/gh-aw/threat-detection/aw-prompts/prompt.txt ]; then - echo "::warning::ERR_VALIDATION: Missing or empty detection context prompt at /tmp/gh-aw/threat-detection/aw-prompts/prompt.txt. Ensure the agent artifact includes /tmp/gh-aw/aw-prompts/prompt.txt. Detection will continue with fallback workflow context." - fi - cp /tmp/gh-aw/agent_output.json /tmp/gh-aw/threat-detection/agent_output.json 2>/dev/null || true - for f in /tmp/gh-aw/aw-*.patch; do - [ -f "$f" ] && cp "$f" /tmp/gh-aw/threat-detection/ 2>/dev/null || true - done - for f in /tmp/gh-aw/aw-*.bundle; do - [ -f "$f" ] && cp "$f" /tmp/gh-aw/threat-detection/ 2>/dev/null || true - done - echo "Prepared threat detection files:" - ls -la /tmp/gh-aw/threat-detection/ 2>/dev/null || true - - name: Setup threat detection - if: always() && steps.detection_guard.outputs.run_detection == 'true' - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - WORKFLOW_NAME: "Build Latest F* with Latest Z3" - WORKFLOW_DESCRIPTION: "Build latest FStar master using Z3 built from latest Z3 master" - HAS_PATCH: ${{ needs.agent.outputs.has_patch }} - 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/setup_threat_detection.cjs'); - await main(); - - name: Ensure threat-detection directory and log - if: always() && steps.detection_guard.outputs.run_detection == 'true' - run: | - mkdir -p /tmp/gh-aw/threat-detection - touch /tmp/gh-aw/threat-detection/detection.log - - name: Setup Node.js - uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0 - with: - node-version: '24' - package-manager-cache: false - - 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: Execute GitHub Copilot CLI - if: always() && steps.detection_guard.outputs.run_detection == 'true' - continue-on-error: true - id: detection_agentic_execution - # Copilot CLI tool arguments (sorted): - timeout-minutes: 20 - 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/threat-detection/detection.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","github.com","host.docker.internal","registry.npmjs.org","telemetry.enterprise.githubcopilot.com"]},"apiProxy":{"enabled":true,"enableTokenSteering":true,"maxRuns":500,"maxEffectiveTokens":25000000},"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 --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; 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 --add-dir "${GITHUB_WORKSPACE}" --prompt-file /tmp/gh-aw/aw-prompts/prompt.txt' 2>&1 | tee -a /tmp/gh-aw/threat-detection/detection.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_DETECTION_COPILOT || vars.GH_AW_DEFAULT_MODEL_COPILOT || 'claude-sonnet-4.6' }} - GH_AW_PHASE: detection - GH_AW_PROMPT: /tmp/gh-aw/aw-prompts/prompt.txt - 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_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: Upload threat detection log - if: always() && steps.detection_guard.outputs.run_detection == 'true' - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 - with: - name: detection - path: /tmp/gh-aw/threat-detection/detection.log - if-no-files-found: ignore - - name: Parse and conclude threat detection - id: detection_conclusion - if: always() - continue-on-error: true - uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0 - env: - RUN_DETECTION: ${{ steps.detection_guard.outputs.run_detection }} - DETECTION_AGENTIC_EXECUTION_OUTCOME: ${{ steps.detection_agentic_execution.outcome }} - GH_AW_DETECTION_CONTINUE_ON_ERROR: "true" - with: - script: | - try { - 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_threat_detection_results.cjs'); - await main(); - } catch (loadErr) { - const continueOnError = process.env.GH_AW_DETECTION_CONTINUE_ON_ERROR !== 'false'; - const detectionExecutionFailed = process.env.DETECTION_AGENTIC_EXECUTION_OUTCOME === 'failure'; - const msg = 'ERR_SYSTEM: \u274C Unexpected error loading threat detection module: ' + (loadErr && loadErr.message ? loadErr.message : String(loadErr)); - core.error(msg); - core.setOutput('reason', 'parse_error'); - if (continueOnError && !detectionExecutionFailed) { - core.warning('\u26A0\uFE0F ' + msg); - core.setOutput('conclusion', 'warning'); - core.setOutput('success', 'false'); - } else { - core.setOutput('conclusion', 'failure'); - core.setOutput('success', 'false'); - core.setFailed(msg); - } - } - safe_outputs: needs: - activation - agent - - detection - if: (!cancelled()) && needs.agent.result != 'skipped' && needs.detection.result == 'success' + if: (!cancelled()) && needs.agent.result != 'skipped' runs-on: ubuntu-slim permissions: contents: read - discussions: write issues: write timeout-minutes: 15 env: GH_AW_CALLER_WORKFLOW_ID: "${{ github.repository }}/fstar-master-build" - GH_AW_DETECTION_CONCLUSION: ${{ needs.detection.outputs.detection_conclusion }} - GH_AW_DETECTION_REASON: ${{ needs.detection.outputs.detection_reason }} 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 Latest F* with Latest Z3" + 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 }} @@ -1381,7 +985,7 @@ jobs: 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 Latest F* with Latest Z3" + 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" @@ -1418,7 +1022,7 @@ jobs: 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_discussion\":{\"category\":\"agentic workflows\",\"close_older_discussions\":true,\"expires\":336,\"fallback_to_issue\":true,\"max\":1,\"title_prefix\":\"[F* Build] \"},\"create_issue\":{\"labels\":[\"build\",\"fstar\"],\"max\":1,\"title_prefix\":\"[F* Build Failure] \"},\"create_report_incomplete_issue\":{},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}" + 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: | diff --git a/.github/workflows/fstar-master-build.md b/.github/workflows/fstar-master-build.md index 86ab4275d..fad78d0d5 100644 --- a/.github/workflows/fstar-master-build.md +++ b/.github/workflows/fstar-master-build.md @@ -1,35 +1,13 @@ --- -description: Build latest FStar master using Z3 built from latest Z3 master - +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 - github: - toolsets: [default] - -safe-outputs: - create-discussion: - title-prefix: "[F* Build] " - category: "Agentic Workflows" - close-older-discussions: true - expires: 14d - create-issue: - title-prefix: "[F* Build Failure] " - labels: ["build", "fstar"] - missing-tool: - create-issue: true - noop: - report-as-issue: false - -timeout-minutes: 120 - +timeout-minutes: 180 steps: - name: Checkout Z3 master uses: actions/checkout@v6.0.2 @@ -37,76 +15,103 @@ steps: ref: master fetch-depth: 1 persist-credentials: false - --- -# Build Latest F* with Latest Z3 +# Build FStar master with Z3 master -You are an automation engineer validating interoperability between Z3 and F*. +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. -Your goal is to build **latest Z3 master** from this repository, then build **latest FStarLang/FStar master** using the Z3 you built. +## Constraints -## Requirements +- 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. -1. Use `${{ github.workspace }}` as the Z3 source (already checked out at `master`). -2. Build Z3 from source with CMake + Ninja in Release mode. -3. Install Z3 into `/tmp/gh-aw/agent/z3-install`. -4. Verify the installed Z3 binary and capture its full version string. -5. Fetch latest `master` from `FStarLang/FStar` and capture the exact commit SHA used. -6. Build F* from that latest master using the locally built Z3 (not a system Z3). -7. If F* requires setup steps, follow the current instructions from the checked-out FStar repository (for example `INSTALL.md`, `README.md`, `flake.nix`, or build scripts). -8. Keep all temporary files under `/tmp/gh-aw/agent`. +## Phase 1: Build Z3 master -## Execution Plan +```bash +set -euo pipefail -### Phase 1: Environment Setup +cd "${{ github.workspace }}" -- Install required build dependencies for Z3 and F* (for example: `cmake`, `ninja-build`, `opam`, `m4`, `pkg-config`, `libgmp-dev`, `curl`, `git`, `python3`). -- Print tool versions (`cmake`, `ninja`, `opam`, `ocaml` if available). +echo "Building Z3 from branch: $(git rev-parse --abbrev-ref HEAD)" +git rev-parse HEAD -### Phase 2: Build and Install Z3 (master) +sudo apt-get update -y +sudo apt-get install -y cmake ninja-build python3 git curl unzip -- Build in `/tmp/gh-aw/agent/z3-build`. -- Use: - - `cmake -G Ninja -DCMAKE_BUILD_TYPE=Release` - - `ninja` - - `ninja install` with prefix `/tmp/gh-aw/agent/z3-install` -- Verify: - - `/tmp/gh-aw/agent/z3-install/bin/z3 --version` -- Record: - - Z3 commit from `git -C "${{ github.workspace }}" rev-parse HEAD` - - Z3 version output +cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release +ninja -C build/release z3 -### Phase 3: Fetch Latest F* Master +"${{ github.workspace }}/build/release/z3" --version | tee /tmp/gh-aw/agent/z3-version.txt +``` -- Clone `https://github.com/FStarLang/FStar.git` into `/tmp/gh-aw/agent/fstar` with branch `master`. -- Record exact commit SHA: - - `git -C /tmp/gh-aw/agent/fstar rev-parse HEAD` +Extract the numeric version string from the `z3 --version` output and store it in `Z3_VERSION` (for example, `4.15.4`). -### Phase 4: Build F* with Local Z3 +## Phase 2: Prepare PATH aliases for FStar -- Ensure the local Z3 is used by exporting: - - `PATH=/tmp/gh-aw/agent/z3-install/bin:$PATH` - - `Z3_EXE=/tmp/gh-aw/agent/z3-install/bin/z3` -- Discover and follow the repository’s current build path from checked-in docs/scripts. -- Execute the build commands needed for F* master. -- Capture concise logs into files under `/tmp/gh-aw/agent/logs/`. +FStar expects versioned Z3 command names on PATH. Create local aliases pointing to the Z3 binary from Phase 1. -### Phase 5: Report Results +```bash +set -euo pipefail -- On success, call `create-discussion` with: - - Z3 commit + version - - FStar commit - - Key build commands executed - - Build outcome summary -- On failure, call `create-issue` with: - - Failing phase - - Error summary - - Relevant log excerpt - - Z3 commit/version and FStar commit (if available) +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" -## Safety and Quality +z3 --version +z3-4.8.5 --version +z3-4.13.3 --version +``` -- Fail fast on command errors. -- Do not modify repository files. -- Keep the report concise and actionable. +## 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.