Update sui-prover.yml

[cos]

No description provided.

[Copilot]

Pull request overview

This PR updates the GitHub Actions workflow configuration for the sui-prover by changing the runner environment for the integer-mate-specs job from a GitHub-hosted runner to a self-hosted runner.

Changes:

• Modified the runner specification for the integer-mate-specs job from macos-latest to runner-base-1

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[cursor]

You have run out of free Bugbot PR reviews for this billing cycle. This will reset on March 1.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[cos]

@claude, use the same setup from scallop-bpl-generation in the integer-mate runner

[claude]

Claude finished @cos's task in 47s —— View job

---

Analysis Complete

• Read the workflow file to understand current configuration
• Identify setup from scallop-bpl-generation job
• Identify differences to apply to integer-mate-specs job

Findings

I've compared the scallop-bpl-generation job with integer-mate-specs and identified the key differences that need to be applied.

Current integer-mate-specs setup issues:

• Uses a symlink for boogie: ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie
• Missing .NET 8 setup (needed for running Boogie via dotnet)
• No boogie version verification

scallop-bpl-generation setup (the correct approach):

• Includes Setup .NET 8 step
• Uses a wrapper script for boogie that calls dotnet to execute BoogieDriver.dll
• Includes boogie version verification

Permission Limitation

I cannot modify workflow files due to GitHub App permissions restrictions. Workflow modifications require elevated permissions for security reasons.

Exact Changes Needed

Here are the specific changes to apply to the integer-mate-specs job in .github/workflows/sui-prover.yml:

1. Add .NET 8 setup step after line 247 (after the Download step):

      - name: Setup .NET 8
        uses: actions/setup-dotnet@v4
        with:
          dotnet-version: '8.0.x'

2. Replace lines 257 in the Setup step (change the boogie symlink to a wrapper script):

Replace this line:

ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

With:

# Create a wrapper script for boogie instead of symlink
cat <<'EOF' > ~/.local/bin/boogie
#!/bin/bash
exec dotnet "$HOME/prover-bundle/boogie/BoogieDriver.dll" "$@"
EOF

3. Add verification at the end of the Setup step (after line 267):

# Verify boogie version
~/.local/bin/boogie /version

Why These Changes Matter

The self-hosted runner (runner-base-1) needs to use the dotnet wrapper approach because:

• Symlinks may not work correctly with Boogie on self-hosted runners
• The wrapper script ensures Boogie runs through the .NET runtime properly
• This matches the proven working setup from scallop-bpl-generation

You'll need to apply these changes manually to the workflow file.

---