Auto update

action.yml

@@ -1,6 +1,6 @@
 name: "Lean Action - CI for Lean Projects"
 description: |
-  Standard CI for Lean projects. 
+  Standard CI for Lean projects.
   Steps:
     - install elan
     - get Mathlib cache (optional, must be downstream of Mathlib)
@@ -84,6 +84,12 @@ inputs:
       If lake-package-directory is not provided, `lean-action` will use the root directory of the repository by default.
     required: false
     default: "."
+  run-auto-update:
+    description: |
+      This is for debugging only. Run auto update script to make dependencies up-to-date.
+      Allowed values: "true" | "false".
+    required: false
+    default: "false"
 outputs:
   build-status:
     description: |
@@ -108,7 +114,7 @@ outputs:
 
 runs:
   using: "composite"
-  steps: 
+  steps:
     - name: install elan
       run: |
         : Install Elan
@@ -129,6 +135,32 @@ runs:
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    # TODO: test for `lake-package-directory`
+    # TODO: `${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}` is too long
+    - name: // 👻 auto update // get latest lean-toolchain
+      if: ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      run: ${{ github.action_path }}/scripts/getLatest.ps1
+      env:
+        GH_TOKEN: ${{ github.token }}
+      shell: pwsh
+      working-directory: ${{ inputs.lake-package-directory }}
+
+    - name: // 👻 auto update // update dependencies of ${{ github.repository }}
+      if: ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      run: lake -R -Kenv=dev update
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
+
+    - name: // 👻 auto update // check if lean-toolchain or lake-manifest.json were updated
+      if: ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      id: check-update
+      run: |
+        OUTCOME=$(bash ${{ github.action_path }}/scripts/check_changes.sh)
+        echo "$OUTCOME" >> "$GITHUB_OUTPUT"
+        echo "info: $OUTCOME"
+      shell: bash
+      working-directory: ${{ inputs.lake-package-directory }}
+
     - uses: actions/cache/restore@v4
       if: ${{ inputs.use-github-cache == 'true' }}
       with:
@@ -161,15 +193,54 @@ runs:
 
     - name: build ${{ github.repository }}
       id: build
-      if: ${{ steps.config.outputs.run-lake-build == 'true'}}
-      env: 
-          BUILD_ARGS: ${{ inputs.build-args }}
+      if: ${{ steps.config.outputs.run-lake-build == 'true'}} && ${{ github.event_name != 'schedule' }} && ${{ inputs.run-auto-update != 'true' }}
+      env:
+        BUILD_ARGS: ${{ inputs.build-args }}
       run: |
         : Lake Build
         ${GITHUB_ACTION_PATH}/scripts/lake_build.sh
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
+    - name: // 👻 auto update // build ${{ github.repository }} for auto-update
+      if: ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      id: build-for-update
+      env:
+        BUILD_ARGS: ${{ inputs.build-args }}
+      run: |
+        : Lake Build
+        ${GITHUB_ACTION_PATH}/scripts/lake_build.sh
+      shell: bash
+      continue-on-error: true
+      working-directory: ${{ inputs.lake-package-directory }}
+
+    - name: // 👻 auto update // record outcome
+      if: ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      id: record-outcome
+      run: |
+        if "${{steps.check-update.outputs.files_changed == 'false'}}" ; then
+          echo "No update available"
+          echo "outcome=no-update" >> "$GITHUB_OUTPUT"
+        elif "${{steps.build-for-update.outcome == 'success'}}"; then
+          echo "Update available and build successful"
+          echo "outcome=update-success" >> "$GITHUB_OUTPUT";
+        elif "${{steps.build-for-update.outcome == 'failure'}}"; then
+          echo "Update available but build fails"
+          echo "outcome=update-fail" >> "$GITHUB_OUTPUT"
+        fi
+      shell: bash
+
+    - name: // 👻 auto update // open PR if the updated lean build was successful
+      if: ${{ steps.build-lean.outcome == 'success' }} && ${{ github.event_name == 'schedule' }} || ${{ inputs.run-auto-update == 'true' }}
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: "Updates available and ready to merge"
+        body: "ready to merge"
+        delete-branch: true
+        branch-suffix: random
+        branch: auto-update/patch
+        labels: "auto-update-lean"
+
     - uses: actions/cache/save@v4
       if: ${{ inputs.use-github-cache == 'true' }}
       with:
@@ -196,7 +267,7 @@ runs:
       working-directory: ${{ inputs.lake-package-directory }}
 
     - name: check reservoir eligibility
-      if: ${{ inputs.check-reservoir-eligibility == 'true' }}
+      if: ${{ inputs.check-reservoir-eligibility == 'true' }} && ${{ github.event_name == 'push' }}
       # Passes in the private status, number of stars, and license id of the repository to check_reservoir_eligibility.sh script
       run: |
         : Check Reservoir Eligibility

scripts/check_changes.sh

@@ -0,0 +1,10 @@
+#!/bin/bash
+
+# Check if either "lean-toolchain" or "lake-manifest.json" have been modified,
+# ignoring white space changes.
+
+if [[ -n $(git diff -w "lean-toolchain") ]] || [[ -n $(git diff -w "lake-manifest.json") ]]; then
+    echo "files_changed=true"
+else
+    echo "files_changed=false"
+fi

scripts/getLatest.ps1

@@ -0,0 +1,18 @@
+# get all release tags from leanprover/lean4
+$versions = gh release list `
+  --repo leanprover/lean4 `
+  --json tagName | `
+  ConvertFrom-Json | `
+  ForEach-Object { $_.tagName } | `
+  ForEach-Object { $_ -replace '^v' }
+
+# parse the version tags as semver
+$semvers = $versions | ForEach-Object { [System.Management.Automation.SemanticVersion]::new($_) }
+
+# sort the versions and get the latest one
+$latest = $semvers | Sort-Object | Select-Object -Last 1
+Write-Host "Latest Lean release is: $latest"
+
+# update `lean-toolchain` file
+$leanStyleVersion = "leanprover/lean4:v$latest"
+$leanStyleVersion | Set-Content -Path lean-toolchain