Merge pull request #114 from leanprover-community/develop

new toolchain in title/body of PR/issue

Author: Seasawher

action.yml

@@ -182,7 +182,27 @@ runs:
     # when update is successful #
     # ------------------------- #
     - name: Open PR if the updated lean build was successful
-      if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'pr' && steps.check-update.outputs.do_update == 'true'
+      if: steps.build-lean.outcome == 'success' &&
+          inputs.on_update_succeeds == 'pr' &&
+          steps.check-update.outputs.do_update == 'true' &&
+          steps.check-update.outputs.lean_toolchain_updated == 'true'
+      uses: peter-evans/create-pull-request@v7
+      with:
+        title: "Updates available and ready to merge"
+        body: |
+          The `lean-toolchain` file has been updated to the following version:
+          ```
+          ${{ steps.record-latest-lean.outputs.latest_lean }}
+          ```
+        delete-branch: true
+        branch: auto-update-lean/patch
+        labels: "auto-update-lean"
+
+    - name: Open PR if the updated lean build was successful
+      if: steps.build-lean.outcome == 'success' &&
+          inputs.on_update_succeeds == 'pr' &&
+          steps.check-update.outputs.do_update == 'true' &&
+          steps.check-update.outputs.lean_toolchain_updated == 'false'
       uses: peter-evans/create-pull-request@v7
       with:
         title: "Updates available and ready to merge"

scripts/checkChanges.js

@@ -46,7 +46,8 @@ if (updateIfModified === 'lean-toolchain') {
 const result = {
   files_changed: changedFiles.length > 0,
   do_update: doUpdate,
-  changed_files: changedFiles.join(' ')
+  changed_files: changedFiles.join(' '),
+  lean_toolchain_updated: fileChanges['lean-toolchain']
 };
 
 console.log('info:', JSON.stringify(result, null, 2));
@@ -57,4 +58,5 @@ if (githubOutput) {
   fs.appendFileSync(githubOutput, `files_changed=${result.files_changed}\n`);
   fs.appendFileSync(githubOutput, `changed_files=${result.changed_files}\n`);
   fs.appendFileSync(githubOutput, `do_update=${result.do_update}\n`);
+  fs.appendFileSync(githubOutput, `lean_toolchain_updated=${result.lean_toolchain_updated}\n`);
 }