open a PR when update succeed

leanprover · Sep 25, 2024 · 68a8c56 · 68a8c56
1 parent 5299d35
commit 68a8c56
Show file tree

Hide file tree

Showing 2 changed files with 68 additions and 2 deletions.
diff --git a/action.yml b/action.yml
@@ -136,6 +136,7 @@ runs:
       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
@@ -144,6 +145,22 @@ runs:
       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:
@@ -176,15 +193,54 @@ runs:
 
     - name: build ${{ github.repository }}
       id: build
-      if: ${{ steps.config.outputs.run-lake-build == 'true'}}
+      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:
@@ -211,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

diff --git a/scripts/check_changes.sh b/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