Merge pull request #29 from Seasawher/develop

add latest_lean to output

Author: Seasawher

.github/workflows/test.yaml

@@ -39,4 +39,26 @@ jobs:
 
       - name: This update should fail
         if: steps.update.outputs.result != 'update-fail'
-        run: exit 1
+        run: exit 1
+
+  output_test:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Update Lean package
+        id: update
+        uses: Seasawher/lean-update@develop
+        with:
+          on_update_succeeds: "silent"
+          lake_package_directory: "./test/Foo"
+
+      - name: output assertion of latest_lean
+        run: |
+          echo "Latest Lean version: ${{ steps.update.outputs.latest_lean }}"
+          if [[ ! "${{ steps.update.outputs.latest_lean }}" =~ ^v ]]; then
+            echo "Error: The latest_lean output should start with 'v'"
+            exit 1
+          fi
+          echo "latest_lean output test passed"

README.md

@@ -161,6 +161,21 @@ A Github token to be used for committing and creating issues/PRs.
 
 Default: `${{ github.token }}`
 
+## Outputs
+
+### `result`
+
+The action outputs `no-update`, `update-success` or `update-fail` depending on the three possible scenarios.
+
+Description of each value:
+* `no-update`: No update was available.
+* `update-success`: An update was available and lean-action step was successful.
+* `update-fail`: An update was available but the lean-action step failed.
+
+### `latest_lean`
+
+The latest Lean release version, including both stable and pre-release versions.
+
 ## Usage Examples
 
 I am using this GitHub Action in the following repository. This might be helpful as a reference.

action.yml

@@ -61,38 +61,46 @@ outputs:
         * `no-update`: No update was available.
         * `update-success`: An update was available and lean-action step was successful.
         * `update-fail`: An update was available but the lean-action step failed.
-    value: ${{ steps.record-outcome.outputs.outcome }}
+    value: ${{ steps.record-result.outputs.outcome }}
+  latest_lean:
+    description: | # markdown
+      The latest Lean release version, including both stable and pre-release versions.
+    value: ${{ steps.record-latest-lean.outputs.latest_lean }}
 runs:
   using: "composite"
   steps:
     - name: Update lean-toolchain
       run: |
-        cd ${{ inputs.lake_package_directory }}
+        : Update lean-toolchain
         node ${{ github.action_path }}/scripts/getLatest.js
       env:
         GH_TOKEN: ${{ github.token }}
       shell: bash
+      working-directory: ${{ inputs.lake_package_directory }}
 
     - name: Install elan
       run: |
+        : Install elan
         curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
         echo "$HOME/.elan/bin" >> $GITHUB_PATH
       shell: bash
 
     - name: Update dependencies of ${{ github.repository }}
       run: |
-        cd ${{ inputs.lake_package_directory }}
+        : Update dependencies
         lake update
       shell: bash
+      working-directory: ${{ inputs.lake_package_directory }}
 
     - name: Check if lean-toolchain or lake-manifest.json were updated
       id: check-update
       run: |
-        cd ${{ inputs.lake_package_directory }}
+        : Check if lean-toolchain or lake-manifest.json were updated
         node ${{ github.action_path }}/scripts/checkChanges.js
       env:
         UPDATE_IF_MODIFIED: ${{ inputs.update_if_modified }}
       shell: bash
+      working-directory: ${{ inputs.lake_package_directory }}
 
     - name: Try to build lean if something was updated
       if: steps.check-update.outputs.files_changed == 'true'
@@ -103,9 +111,13 @@ runs:
         build-args: ${{ inputs.build_args }}
         lake-package-directory: ${{ inputs.lake_package_directory }}
 
-    - name: Record outcome
-      id: record-outcome
+    # -------------------------------- #
+    # record the output of this action #
+    # -------------------------------- #
+    - name: Record the outcome
+      id: record-result
       run: | # bat
+        : Record the outcome
         if [ "${{ steps.check-update.outputs.files_changed }}" == "false" ]; then
           echo "No update available"
           echo "outcome=no-update" >> $GITHUB_OUTPUT
@@ -118,6 +130,16 @@ runs:
         fi
       shell: bash
 
+    - name: Record the latest Lean version
+      id: record-latest-lean
+      run: |
+        : Record the latest Lean version
+        LEAN_VERSION=$(cat lean-toolchain | sed 's/leanprover\/lean4://')
+        echo "Latest Lean release is: $LEAN_VERSION"
+        echo "latest_lean=$LEAN_VERSION" >> $GITHUB_OUTPUT
+      shell: bash
+      working-directory: ${{ inputs.lake_package_directory }}
+
     # ------------------------- #
     # when update is successful #
     # ------------------------- #
@@ -135,6 +157,7 @@ runs:
     - name: Open issue if the updated lean build was successful
       if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'issue' && steps.check-update.outputs.do_update == 'true'
       run: | # bat
+        : Open issue if the updated lean build was successful
         CHANGED_FILES="${{ steps.check-update.outputs.changed_files }}"
         BULLET_LIST=""
         for file in $CHANGED_FILES; do
@@ -164,6 +187,7 @@ runs:
     - name: Open issue if the updated lean build fails
       if: steps.build-lean.outcome == 'failure' && inputs.on_update_fails == 'issue'
       run: | # bat
+        : Open issue if the updated lean build fails
         CHANGED_FILES="${{ steps.check-update.outputs.changed_files }}"
         BULLET_LIST=""
         for file in $CHANGED_FILES; do
@@ -182,7 +206,9 @@ runs:
 
     - name: Action fails if the updated lean build fails
       if: steps.build-lean.outcome == 'failure' && inputs.on_update_fails == 'fail'
-      run: exit 1
+      run: |
+        : Action fails if the updated lean build fails
+        exit 1
       shell: bash
 
 branding: