z3/.github/workflows/fstar-master-build.yml

name: Build FStar master with Z3 master

on:
  schedule:
    - cron: "9 4 * * *"
  workflow_dispatch:
    inputs:
      z3_ref:
        description: Z3 ref to checkout and build
        required: false
        default: master
      z3_cmake_args:
        description: Extra CMake arguments for Z3 build
        required: false
        default: ""
      z3_runtime_args:
        description: "Extra Z3 runtime args (example: smt.ho_matching=true)"
        required: false
        default: "smt.ho_matching=true"
      fstar_ref:
        description: FStar ref to checkout and build
        required: false
        default: master
      fstar_opam_switch:
        description: OCaml switch for FStar build
        required: false
        default: "4.14.2"
      fstar_otherflags:
        description: "Extra FStar OTHERFLAGS (example: --smt.ho_matching true)"
        required: false
        default: "--smt.ho_matching true"
      discussion_category:
        description: Discussion category name
        required: false
        default: "Agentic Workflows"

permissions:
  contents: read
  discussions: write

concurrency:
  group: ${{ github.workflow }}
  cancel-in-progress: false

jobs:
  build-and-report:
    runs-on: ubuntu-latest
    timeout-minutes: 180
    env:
      Z3_REF: ${{ github.event.inputs.z3_ref || 'master' }}
      Z3_CMAKE_ARGS: ${{ github.event.inputs.z3_cmake_args || '' }}
      Z3_RUNTIME_ARGS: ${{ github.event.inputs.z3_runtime_args || 'smt.ho_matching=true' }}
      FSTAR_REF: ${{ github.event.inputs.fstar_ref || 'master' }}
      FSTAR_OPAM_SWITCH: ${{ github.event.inputs.fstar_opam_switch || '4.14.2' }}
      FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '--smt.ho_matching true' }}
      DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
    steps:
      - name: Checkout Z3
        uses: actions/checkout@v6.0.3
        with:
          ref: ${{ env.Z3_REF }}
          fetch-depth: 1

      - name: Install dependencies
        run: |
          set -euo pipefail
          sudo apt-get update -y
          sudo apt-get install -y cmake ninja-build python3 git curl unzip opam m4 pkg-config libgmp-dev

      - name: Build Z3
        run: |
          set -euo pipefail
          mkdir -p /tmp/gh-aw/agent
          cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release $Z3_CMAKE_ARGS
          ninja -C build/release z3
          ./build/release/z3 --version | tee /tmp/gh-aw/agent/z3-version.txt
          printf '(check-sat)\n' | ./build/release/z3 $Z3_RUNTIME_ARGS -in | tee /tmp/gh-aw/agent/z3-runtime-check.txt

      - name: Prepare Z3 aliases for FStar
        run: |
          set -euo pipefail
          mkdir -p /tmp/gh-aw/agent/z3-bin
          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3
          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.8.5
          ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.13.3
          /tmp/gh-aw/agent/z3-bin/z3 --version

      - name: Build FStar
        run: |
          set -euo pipefail
          rm -rf /tmp/gh-aw/agent/FStar
          git clone --depth=1 --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
          cd /tmp/gh-aw/agent/FStar
          echo "FStar commit: $(git rev-parse HEAD)" | tee /tmp/gh-aw/agent/fstar-commit.txt

          opam init --disable-sandboxing --yes
          opam switch create "$FSTAR_OPAM_SWITCH" --yes || opam switch "$FSTAR_OPAM_SWITCH"
          eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")"
          opam install --deps-only . --yes

          Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)"
          test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; cat /tmp/gh-aw/agent/z3-version.txt || true; exit 1; }

          PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)"
          test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; }
          /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt

      - name: Create discussion summary
        uses: actions/github-script@v9
        env:
          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
        with:
          script: |
            const fs = require('fs');

            const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim();
            const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim();
            const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
            const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim();
            const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, '');
            const date = new Date().toISOString().slice(0, 10);

            const owner = context.repo.owner;
            const repo = context.repo.repo;
            const categoryName = process.env.DISCUSSION_CATEGORY;

            const categoryQuery = await github.graphql(
              `query($owner:String!, $repo:String!) {
                repository(owner:$owner, name:$repo) {
                  id
                  discussionCategories(first:50) {
                    nodes { id name }
                  }
                }
              }`,
              { owner, repo }
            );

            const categories = categoryQuery.repository.discussionCategories.nodes || [];
            const normalized = categoryName.trim().toLowerCase();
            const category = categories.find(c => c.name.toLowerCase() === normalized);
            if (!category) {
              throw new Error(`Discussion category '${categoryName}' not found`);
            }

            const body = [
              `### Build status`,
              `- ✅ Z3 build completed`,
              `- ✅ FStar build completed`,
              ``,
              `### Inputs used`,
              `- z3_ref: \`${process.env.Z3_REF}\``,
              `- z3_cmake_args: \`${process.env.Z3_CMAKE_ARGS}\``,
              `- z3_runtime_args: \`${process.env.Z3_RUNTIME_ARGS}\``,
              `- fstar_ref: \`${process.env.FSTAR_REF}\``,
              `- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``,
              `- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``,
              ``,
              `### Produced versions`,
              `- Z3: \`${z3VersionText}\``,
              `- FStar: \`${fstarVersionText}\``,
              `- FStar commit: \`${fstarCommit}\``,
              ``,
              `### Run`,
              `- Workflow run: ${process.env.RUN_URL}`
            ].join('\n');

            await github.graphql(
              `mutation($repositoryId:ID!, $categoryId:ID!, $title:String!, $body:String!) {
                createDiscussion(input:{
                  repositoryId:$repositoryId,
                  categoryId:$categoryId,
                  title:$title,
                  body:$body
                }) {
                  discussion { url }
                }
              }`,
              {
                repositoryId: categoryQuery.repository.id,
                categoryId: category.id,
                title: `FStar build with configurable Z3 inputs — ${date}`,
                body
              }
            );