Merge pull request #143 from leanprover-community/develop

Develop

Author: Seasawher

README.md

@@ -178,6 +178,16 @@ This parameter is passed to the lake-package-directory argument of leanprover/le
 
 Default: `.`
 
+### `update_lean_toolchain`
+
+Controls whether to update the lean-toolchain file for projects with no dependencies.
+
+Allowed values:
+* `auto`: Automatically update lean-toolchain to the latest stable release (default behavior)
+* `never`: Never update the lean-toolchain file
+
+Default: `auto`
+
 ### `token`
 
 A Github token to be used for committing and creating issues/PRs.

action.yml

@@ -52,6 +52,15 @@ inputs:
       This parameter is passed to the lake-package-directory argument of leanprover/lean-action.
     required: false
     default: "."
+  update_lean_toolchain:
+    description: |
+      Controls whether to update the lean-toolchain file for projects with no dependencies.
+      Allowed values:
+        * `auto`: Automatically update lean-toolchain to the latest stable release (default behavior)
+        * `never`: Never update the lean-toolchain file
+      Default: `auto`
+    required: false
+    default: "auto"
   token:
     description: |
       A Github token to be used for committing
@@ -107,7 +116,7 @@ runs:
       working-directory: ${{ inputs.lake_package_directory }}
 
     - name: Update lean-toolchain
-      if: ${{ steps.find-dependencies.outputs.outcome == 'no-depencency' }}
+      if: ${{ steps.find-dependencies.outputs.outcome == 'no-depencency' && inputs.update_lean_toolchain == 'auto' }}
       run: |
         : Update lean-toolchain
         node ${{ github.action_path }}/scripts/getLatest.js