Add comprehensive macOS testing to PR workflow (#4857)

F-WRunTime · web-flow · commit ec6b3c2c7a9c · 2025-10-07T13:05:46.000-06:00
## Overview

This PR adds macOS testing to the pull request workflow to monitor
macOS-specific build issues without blocking development. The approach
uses `continue-on-error: true` to collect failure data while maintaining
a working CI/CD pipeline.

## Changes Made

### PR Workflow (test-pr.yml)
- **Added `test-macos-build` job** that runs on `macos-15`
- **Non-blocking execution**: Uses `continue-on-error: true` to prevent
PR failures
- **Comprehensive testing**:
  - Homebrew formula validation using `brew audit --strict`
- Formula installation from source using `brew install
--build-from-source`
- Basic functionality testing with `kompile` for both LLVM and Haskell
backends
  - Formula debugging artifacts uploaded for troubleshooting

### Release Workflow (release.yml)
- **Made macOS jobs non-blocking**: Added `continue-on-error: true` to
both:
  - `macos-build` job (Build MacOS Package)
  - `macos-test` job (Test MacOS Package)
- **Prevents release blocking**: macOS failures won't prevent releases
from completing

## Key Benefits

- **Data Collection**: Monitor macOS build issues without breaking the
pipeline
- **Early Detection**: Catch macOS-specific problems in PRs before they
reach releases
- **Incremental Fixes**: Address issues over time without pressure to
fix immediately
- **Working CI/CD**: Maintain functional builds for all other platforms
- **Debugging Support**: Upload artifacts for troubleshooting failed
builds

## Current Status

- ✅ **PR testing**: macOS tests run but don't block PR merges
- ✅ **Release testing**: macOS builds don't block releases
- ✅ **Clean codebase**: No complex workarounds or modifications to core
build files
- ✅ **Monitoring**: Can collect data on macOS-specific failures

## Remaining TODOs

After further investigation of the collected failure data, the following
items need to be addressed:

### High Priority
- [ ] **Java 17 Compatibility**: Resolve Spotless/Google Java Format
compatibility issues on macOS
- [ ] **Maven Dependencies**: Fix dependency resolution problems in
Homebrew build environment
- [ ] **Build Environment**: Address macOS-specific build toolchain
issues

### Medium Priority  
- [ ] **Homebrew Formula**: Optimize formula for better macOS
compatibility
- [ ] **Error Handling**: Improve error reporting and debugging
capabilities
- [ ] **Performance**: Optimize build times for macOS runners

### Future Enhancements
- [ ] **CloudRepo Integration**: Enable proper Maven artifact publishing
for PR testing
- [ ] **Staging Repositories**: Integration with staging Maven
repositories
- [x] **Enhanced Monitoring**: Better failure analysis and reporting

## Testing Strategy

The macOS testing job will:
1. Run on all PRs targeting the `develop` branch
2. Execute comprehensive Homebrew formula testing
3. Upload debugging artifacts on failure
4. **Not block PR merges** if it fails (due to `continue-on-error:
true`)

## Related Issues

- Addresses macOS build reliability issues in the release workflow
- Provides foundation for incremental macOS build improvements
- Establishes monitoring system for macOS-specific problems
- Complements existing non-blocking macOS testing in release workflow

## Next Steps

1. Monitor macOS test results over several PR cycles
2. Analyze failure patterns and root causes
3. Implement targeted fixes based on collected data
4. Gradually improve macOS build reliability
5. Eventually remove `continue-on-error` when issues are resolved
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -302,6 +302,7 @@ jobs:
     timeout-minutes: 120
     environment: production
     needs: [set-release-id, source-tarball]
+    continue-on-error: true # Do not fail releases due to MacOS builds at this time. Oct. 6, 2025
     steps:
       - name: Check out code
         uses: actions/checkout@v4
@@ -400,7 +401,7 @@ jobs:
     timeout-minutes: 60
     environment: production
     needs: [macos-build, set-release-id]
-    continue-on-error: true
+    continue-on-error: true # Do not fail releases due to MacOS tests at this time. Oct. 6, 2025
     steps:
       - name: 'Check out matching homebrew repo branch'
         uses: actions/checkout@v4
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -337,3 +337,121 @@ jobs:
           docker stop --time=0 k-pyk-regression-${{ github.sha }}
 
 
+  test-macos-build:
+    name: 'K: macOS Build & Test'
+    runs-on: macos-15
+    timeout-minutes: 60
+    needs: code-quality
+    continue-on-error: true # Do not fail PRs due to MacOS builds at this time. Oct. 6, 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: 'Build brew bottle'
+        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}"
+          git commit "Formula/$PACKAGE.rb" -m "Update ${PACKAGE} to ${VERSION}: part 1"
+          ../kframework/package/macos/brew-build-and-update-to-local-bottle "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
+          git reset HEAD^
+          LOCAL_BOTTLE_NAME=$(basename "$(find . -name "kframework--${VERSION}.arm64_sonoma.bottle*.tar.gz")")
+          # shellcheck disable=2001
+          BOTTLE_NAME=$(echo "${LOCAL_BOTTLE_NAME#./}" | sed 's!kframework--!kframework-!')
+          ../kframework/package/macos/brew-update-to-final "${PACKAGE}" "${VERSION}" "${ROOT_URL}"
+          echo "path=${LOCAL_BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
+          echo "path_remote=${BOTTLE_NAME}" >> "${GITHUB_OUTPUT}"
+
+      - name: 'Upload bottle'
+        uses: actions/upload-artifact@v4
+        with:
+          name: homebrew-bottle
+          path: homebrew-k
+          retention-days: 1
+
+      - 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
+          MAVEN_OPTS: >-
+            -Dhttp.keepAlive=false
+            -Dmaven.wagon.http.pool=false
+            -Dmaven.wagon.httpconnectionManager.ttlSeconds=30
+        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 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
+
+
