Add comprehensive macOS testing to PR workflow

.github/workflows/test-pr.yml

@@ -337,3 +337,100 @@ jobs:
           docker stop --time=0 k-pyk-regression-${{ github.sha }}
 
 
+  test-macos-build:
+    name: 'K: macOS Build & Test'
+    runs-on: macos-14
+    timeout-minutes: 60
+    needs: code-quality
+    continue-on-error: true # Do not fail PRs due to MacOS builds at this time. Sept. 9, 2025
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+          path: kframework
+
+      - name: 'Check out homebrew repo'
+        uses: actions/checkout@v4
+        with:
+          repository: runtimeverification/homebrew-k
+          path: homebrew-k
+          ref: master
+
+      - name: 'Mac Dependencies'
+        run: |
+          # Via: https://github.com/ledger/ledger/commit/1eec9f86667cad3b0bbafb82a83739a0d30ca09f
+          # Unlink and re-link to prevent errors when github mac runner images
+          # install python outside of brew, for example:
+          # https://github.com/orgs/Homebrew/discussions/3895
+          # https://github.com/actions/setup-python/issues/577
+          # https://github.com/actions/runner-images/issues/6459
+          # https://github.com/actions/runner-images/issues/6507
+          # https://github.com/actions/runner-images/issues/2322
+
+          # shellcheck disable=SC2162
+          brew list -1 | grep python | while read formula; do brew unlink "$formula"; brew link --overwrite "$formula"; done
+
+          # uninstall pre-installed cmake
+          brew uninstall cmake
+
+      - name: 'Prepare Homebrew formula for testing'
+        id: build
+        env:
+          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
+          MAVEN_OPTS: >-
+              -Dhttp.keepAlive=false
+              -Dmaven.wagon.http.pool=false
+              -Dmaven.wagon.httpconnectionManager.ttlSeconds=30
+        run: |
+          PACKAGE=kframework
+          VERSION=$(cat kframework/package/version)
+          ROOT_URL='https://github.com/runtimeverification/k/releases/download'
+
+          # For PR testing, we'll use the latest available source tarball
+          # or create a test tarball from the current code
+          if [ -f "$ROOT_URL/v${VERSION}/kframework-${VERSION}-src.tar.gz" ]; then
+            wget "$ROOT_URL/v${VERSION}/kframework-${VERSION}-src.tar.gz"
+          else
+            # Create a test tarball from current code for PR testing
+            echo "Creating test tarball for PR testing..."
+            tar czf "kframework-${VERSION}-src.tar.gz" --exclude='.git' --exclude='homebrew-k' .
+          fi
+
+          cd homebrew-k
+          ../kframework/package/macos/brew-update-to-local "${PACKAGE}" "${VERSION}"
+          echo "Formula prepared for testing"
+
+      - name: 'Test Homebrew formula validation'
+        id: test
+        env:
+          # github actions sets the JAVA_HOME variable to Java 8 explicitly for
+          # some reason. There doesn't seem to be a way to tell it to unset the
+          # variable, so instead we just have to tell it to use Java 17
+          # explicitly instead.
+          JAVA_HOME: ${{ env.JAVA_HOME_17_X64 }}
+          HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK: 1
+        run: |
+          # Test the Homebrew formula validation and basic functionality
+          cd homebrew-k
+
+          # Validate the formula syntax by installing it as a local tap
+          brew tap --force-local runtimeverification/k .
+          brew audit --strict kframework
+
+          # Test formula installation from source
+          brew install --build-from-source kframework -v
+
+          # Basic functionality test
+          echo 'module TEST imports BOOL endmodule' > test.k
+          kompile test.k --backend llvm
+          kompile test.k --backend haskell
+          echo "✅ macOS build and test completed successfully"
+
+      - name: 'Upload formula for debugging'
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: macos-formula-test
+          path: homebrew-k/Formula/kframework.rb
+          retention-days: 1