Add manifest #2
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Check for updates | |
| # This workflow checks for updates to the Lean toolchain or Lake manifest and takes appropriate actions. | |
| # It will: | |
| # - Run `lake update` to check for updates. | |
| # - Attempt to build the Lean project if updates are found. | |
| # - Open a Pull Request (PR) if the build is successful. | |
| # - Open an issue if the build fails. | |
| # - Do nothing if no updates are found. | |
| on: | |
| # schedule: | |
| # - cron: "0 11 * * 4" # Run the workflow every Wednesday at 11:00 UTC | |
| push: | |
| branches: ["workflows/update"] # Trigger the workflow on pushes to the "main" branch (replace "main" with your default branch if different) | |
| workflow_dispatch: # Allow manual triggering of the workflow | |
| jobs: | |
| attempt-update: | |
| runs-on: ubuntu-latest # Use the latest Ubuntu environment for the job | |
| permissions: | |
| issues: write # Permission to create issues | |
| pull-requests: write # Permission to create pull requests | |
| contents: write # Permission to push changes | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v4 # Check out the repository code to the GitHub runner | |
| - name: Install elan | |
| run: | | |
| # Install elan, the Lean toolchain manager, for managing Lean versions | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y | |
| # Add elan to the system PATH so it's available in subsequent steps | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Update | |
| run: lake update # Run 'lake update' to check for updates in the Lean toolchain or Lake manifest | |
| - name: Check if anything was updated | |
| uses: tj-actions/verify-changed-files@v20 # Verify if any files were changed by the update | |
| id: check-update | |
| with: | |
| files: | | |
| lean-toolchain # Check for changes in the Lean toolchain configuration | |
| lake-manifest.json # Check for changes in the Lake manifest file | |
| - name: Try to build lean if something was updated | |
| if: steps.check-update.outputs.files_changed == 'true' # Only run this step if updates were detected | |
| id: build-lean | |
| continue-on-error: true # Continue the workflow even if the build fails | |
| run: | | |
| lake exe cache get || true # Attempt to retrieve cached build artifacts, continue if it fails | |
| lake build # Attempt to build the Lean project using Lake | |
| - name: Run step only if nothing was updated | |
| if: steps.check-update.outputs.files_changed == 'false' # Only run if no updates were detected | |
| run: | | |
| echo "No update available" # Output a message indicating no updates were found | |
| echo "outcome=no-update" >> "$GITHUB_ENV" # Set the outcome environment variable to 'no-update' | |
| - name: Run step only if the updated lean build was successful | |
| id: step | |
| if: steps.build-lean.outcome == 'success' # Only run if the build was successful | |
| run: | | |
| echo "Update available and build successful" # Output a message indicating the update was successful | |
| echo "outcome=update-success" >> "$GITHUB_ENV" # Set the outcome environment variable to 'update-success' | |
| - name: Open PR if the updated lean build was successful | |
| if: steps.build-lean.outcome == 'success' # Only run if the build was successful | |
| uses: peter-evans/create-pull-request@v6 # Create a pull request with the updated files | |
| with: | |
| title: "Updates available and ready to merge." # Title of the PR | |
| body: | | |
| The following files have been updated: | |
| - lean-toolchain | |
| - lake-manifest.json | |
| The build was successful, and this PR is ready to be merged. | |
| delete-branch: true # Automatically delete the branch after the PR is merged | |
| branch-suffix: random # Use a random suffix for the branch name to avoid conflicts | |
| branch: auto-update/patch # The branch name for the PR | |
| - name: Open issue if the updated lean build fails | |
| if: steps.build-lean.outcome == 'failure' # Only run if the build failed | |
| run: | | |
| echo "outcome=update-fail" >> "$GITHUB_ENV" # Set the outcome environment variable to 'update-fail' | |
| gh issue create \ | |
| --title "$TITLE" \ | |
| --label "$LABELS" \ | |
| --body "$BODY" | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} # GitHub token for authentication to create the issue | |
| GH_REPO: ${{ github.repository }} # The repository in which to create the issue | |
| TITLE: "Updates available but manual intervention required" # Title of the issue | |
| LABELS: "bug, needs-attention" # Labels to categorize the issue | |
| BODY: | | |
| The automatic update process detected changes and attempted to build Lean, but the build failed. | |
| Please run `lake update` and investigate the following files: | |
| ${{ steps.check-update.outputs.changed_files }} | |
| This issue will remain open until the build is fixed and the update can be successfully merged. | |
| Ensure to close this issue once resolved to avoid duplicate issues. # Detailed issue body explaining the problem and next steps | |
| - name: Show the outcome | |
| run: | | |
| echo "Outcome of the update process: ${{ env.outcome }}" # Display the outcome of the update process | |
| # This step shows the final outcome, whether no updates, a successful update, or a failed update occurred |