Sync upstream leanprover-community/iris-lean and bump to Lean 4.28.0

.github/workflows/build.yml

@@ -8,6 +8,15 @@ on:
   workflow_dispatch:
 
 jobs:
+  cancel:
+    name: "Cancel Previous Runs"
+    runs-on: ubuntu-latest
+    steps:
+      - uses: styfle/cancel-workflow-action@0.12.1
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
   build:
     runs-on: ubuntu-latest
 

.github/workflows/check-imports.yml

@@ -0,0 +1,20 @@
+name: Check Imports
+
+on:
+  pull_request:
+    branches: ["main"]
+  workflow_dispatch:
+
+jobs:
+  check-imports:
+    name: Check Library File Imports
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Update Bluebell.lean
+        run: ./scripts/update-lib.sh
+
+      - name: Check that all files are imported
+        run: git diff --exit-code src/Bluebell.lean

.github/workflows/pr-summary.yml

@@ -0,0 +1,21 @@
+name: 'PR Summary'
+
+on:
+  pull_request:
+    types: [opened, synchronize]
+
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  summarize:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Generate PR Summary
+        uses: alexanderlhicks/lean-summary-workflow@main
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          gemini_api_key: ${{ secrets.GEMINI_API_KEY }}
+          github_repository: ${{ github.repository }}
+          pr_number: ${{ github.event.pull_request.number }}

.github/workflows/review.yml

@@ -0,0 +1,29 @@
+name: AI Code Review for Lean PRs
+
+on:
+  issue_comment:
+    types: [created]
+  workflow_dispatch:
+    inputs:
+      pr_number:
+        description: 'Pull Request Number'
+        required: true
+        type: string
+
+jobs:
+  ai_review_lean:
+    if: |
+      (github.event_name == 'issue_comment' && github.event.issue.pull_request && startsWith(github.event.comment.body, '/review') && (github.event.comment.author_association == 'OWNER' || github.event.comment.author_association == 'MEMBER')) ||
+      (github.event_name == 'workflow_dispatch')
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      pull-requests: write
+
+    steps:
+      - name: Run AI Code Review Action
+        uses: alexanderlhicks/lean-review-workflow@main
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          gemini_api_key: ${{ secrets.GEMINI_API_KEY }}
+          pr_number: ${{ github.event.issue.number || inputs.pr_number }}

.github/workflows/sync-upstream.yml

@@ -0,0 +1,150 @@
+name: Sync with Upstream
+
+on:
+  schedule:
+    - cron: "0 9 */14 * *" # Every 14 days at 09:00 AM UTC
+  workflow_dispatch: # Allow manual triggering
+
+jobs:
+  sync_upstream:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      pull-requests: write
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          fetch-depth: 0
+
+      - name: Configure Git
+        run: |
+          git config --global user.name "github-actions[bot]"
+          git config --global user.email "github-actions[bot]@users.noreply.github.com"
+
+      - name: Add upstream remote
+        run: |
+          git remote add upstream https://github.com/leanprover-community/iris-lean.git || true
+          git fetch upstream
+
+      - name: Create sync branch
+        id: sync
+        run: |
+          BRANCH_NAME="sync-upstream-$(date +%Y-%m-%d)"
+          echo "branch_name=$BRANCH_NAME" >> $GITHUB_OUTPUT
+
+          # Check if there are any differences between our master and upstream master
+          UPSTREAM_COMMITS=$(git rev-list --count HEAD..upstream/master 2>/dev/null || echo "0")
+          echo "upstream_commits=$UPSTREAM_COMMITS" >> $GITHUB_OUTPUT
+
+          if [ "$UPSTREAM_COMMITS" -eq "0" ]; then
+            echo "No new commits from upstream. Skipping sync."
+            echo "needs_sync=false" >> $GITHUB_OUTPUT
+            exit 0
+          fi
+
+          echo "needs_sync=true" >> $GITHUB_OUTPUT
+          echo "Found $UPSTREAM_COMMITS new commits from upstream"
+
+          # Create and switch to sync branch
+          git checkout -b "$BRANCH_NAME"
+
+          # Attempt to merge upstream changes
+          if git merge upstream/master --no-edit; then
+            echo "merge_success=true" >> $GITHUB_OUTPUT
+            echo "Upstream changes merged successfully"
+          else
+            echo "merge_success=false" >> $GITHUB_OUTPUT
+            echo "Merge conflicts detected"
+            # Add all files (including conflicted ones) and commit
+            git add .
+            git commit -m "WIP: Sync with upstream - merge conflicts need resolution"
+          fi
+
+      - name: Push sync branch
+        if: steps.sync.outputs.needs_sync == 'true'
+        run: |
+          git push origin ${{ steps.sync.outputs.branch_name }}
+
+      - name: Create Pull Request
+        if: steps.sync.outputs.needs_sync == 'true'
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const branchName = '${{ steps.sync.outputs.branch_name }}';
+            const mergeSuccess = '${{ steps.sync.outputs.merge_success }}' === 'true';
+            const upstreamCommits = '${{ steps.sync.outputs.upstream_commits }}';
+
+            let title, body;
+
+            if (mergeSuccess) {
+              title = `🔄 Sync with upstream (${upstreamCommits} commits)`;
+              body = `## Upstream Sync
+
+            This PR automatically syncs changes from \`leanprover-community/iris-lean\`.
+
+            ### Changes
+            - **${upstreamCommits}** new commits from upstream
+            - No merge conflicts detected ✅
+
+            ### Next Steps
+            - Review the changes
+            - Run tests to ensure compatibility
+            - Merge when ready
+
+            ---
+            *This PR was created automatically by the sync-upstream workflow.*`;
+            } else {
+              title = `⚠️ Sync with upstream (${upstreamCommits} commits) - Conflicts Need Resolution`;
+              body = `## Upstream Sync - Manual Resolution Required
+
+            This PR automatically syncs changes from \`leanprover-community/iris-lean\`, but **merge conflicts were detected** and need manual resolution.
+
+            ### Changes
+            - **${upstreamCommits}** new commits from upstream
+            - ⚠️ Merge conflicts detected - manual resolution required
+
+            ### Next Steps
+            1. Check out this branch locally: \`git checkout ${branchName}\`
+            2. Resolve merge conflicts in the affected files
+            3. Commit the resolved changes
+            4. Push the updates: \`git push origin ${branchName}\`
+            5. Review and merge this PR
+
+            ### Commands to resolve locally:
+            \`\`\`bash
+            git checkout ${branchName}
+            # Resolve conflicts in your editor
+            git add .
+            git commit -m "Resolve merge conflicts from upstream sync"
+            git push origin ${branchName}
+            \`\`\`
+
+            ---
+            *This PR was created automatically by the sync-upstream workflow.*`;
+            }
+
+            const { data: pr } = await github.rest.pulls.create({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              title: title,
+              head: branchName,
+              base: 'master',
+              body: body
+            });
+
+            console.log(`Created PR #${pr.number}: ${pr.html_url}`);
+
+            // Add labels based on merge status
+            const labels = ['upstream-sync'];
+            if (!mergeSuccess) {
+              labels.push('merge-conflicts');
+            }
+
+            await github.rest.issues.addLabels({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              issue_number: pr.number,
+              labels: labels
+            });

.gitignore

@@ -1 +1,19 @@
 /.lake
+/.claude
+/.cursor
+
+# LaTeX compilation files
+*.aux
+*.bbl
+*.blg
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.synctex.gz
+*.synctex(busy)
+
+# Generated paper PDF
+paper/paper.pdf
+
+.DS_Store.gemini_tmp/

CONTRIBUTING.md

@@ -0,0 +1,48 @@
+# Contributing to Iris-Lean
+
+We enthusiastically welcome contributions to this fork of Iris-Lean!
+
+This project aims to develop the [Bluebell](https://arxiv.org/abs/2402.18708) program logic on top of Iris. Whether you are fixing bugs, improving documentation, or adding new formalizations, your input is valuable. We particularly encourage contributions that address:
+
+* **Active formalizations:** Please see the [Bluebell paper](https://arxiv.org/abs/2402.18708) for the theoretical foundations and goals of this project.
+* **Open Issues:** Please see the list of open issues for bugs, requested features, and specific formalization tasks. Issues tagged as `good first issue` or `help wanted` are great places to start.
+* **Documentation:** Documentation is actively being worked on.
+
+If you are interested in contributing but unsure where to begin, please get in touch via the [Iris-Lean Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean).
+
+### Large Contributions
+
+For substantial contributions, such as formalizing a new section of the Bluebell logic, we strongly encourage aligning with the paper first.
+
+* **Bluebell Paper:** The [Bluebell paper](https://arxiv.org/abs/2402.18708) acts as the primary specification (or "blueprint") for this project.
+    * It outlines the definitions, theorems, and logical rules we aim to formalize.
+    * Please verify that your contributions match the definitions and theorems presented in the paper.
+* **Process:** Please open a new discussion or issue to propose your planned contribution and discuss how it fits into the existing formalization before starting implementation.
+
+### Style Guide
+
+Iris-Lean aims to align closely with the established conventions of the Lean community, particularly those used in `mathlib`.
+Please follow the [mathlib Style Guide](https://github.com/leanprover-community/mathlib4/blob/master/CONTRIBUTING.md#style-guide-and-conventions).
+This covers naming conventions, proof style, formatting, and more.
+
+Adhering to this style guide ensures consistency across the library, making it easier for everyone to read, understand, and maintain the code. Please ensure your code compiles and follows these standards.
+
+#### Citation Standards
+
+When referencing papers in Lean docstrings:
+
+* **Use citation keys in text**: Reference papers with citation keys (e.g., `[Bluebell24]`) rather than full titles or URLs.
+
+* **Include a References section**: Each file that cites papers should have a `## References` section in its docstring header.
+
+## Code of Conduct
+
+To ensure a welcoming and collaborative environment, this project follows the principles outlined in the [mathlib Code of Conduct](https://github.com/leanprover-community/mathlib4/blob/master/CODE_OF_CONDUCT.md).
+
+By participating in this project (e.g., contributing code, opening issues, commenting in discussions), you agree to abide by its terms. Please treat fellow contributors with respect. Unacceptable behavior can be reported to the project maintainers.
+
+## Licensing
+
+This project is licensed under the terms of the Apache License 2.0 license. The full license text can be found in the [LICENSE](LICENSE) file.
+
+By contributing to Iris-Lean, you agree that your contributions will be licensed under this same license. Ensure you are comfortable with these terms before submitting contributions.