action.yml

name: "Lean update"
description: "Attempts to update lean and dependencies of a lean project"
author: "Oliver Butterley"
inputs:
  on_update_succeeds:
    description: |
      What to do when an update is available and the build is successful.
      Allowed values: "silent", "commit", "issue" or "pr".
      Default: "silent".
    required: true
    default: "silent"
  on_update_fails:
    description: |
      What to do when an update is available and the build fails.
      Allowed values: "silent", "issue" or "pr".
      Default: "silent".
    required: true
    default: "silent"
  token:
    description: |
      A Github token to be used for committing
    required: true
    default: ${{ github.token }}
outputs:
  result:
    description: "The action outputs `up-to-date`, `update-succeeds` or `update-fails` depending on the three possible scenarios."
    value: ${{ steps.record-outcome.outputs.outcome }}
runs:
  using: "composite"
  steps:
    - name: Update lean-toolchain
      run: ${{ github.action_path }}/scripts/getLatest.ps1
      env:
        GH_TOKEN: ${{ github.token }}
      shell: pwsh

    - name: Install elan
      run: |
        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: lake -R -Kenv=dev update
      shell: bash

    - name: Check if lean-toolchain or lake-manifest.json were updated
      id: check-update
      run: |
        OUTCOME=$(bash ${{ github.action_path }}/check-changes.sh)
        echo "$OUTCOME" >> "$GITHUB_OUTPUT"
        echo "info: $OUTCOME"
      shell: bash

    - name: Try to build lean if something was updated
      if: steps.check-update.outputs.files_changed == 'true'
      id: build-lean
      continue-on-error: true
      uses: leanprover/lean-action@v1

    - name: Record outcome
      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-lean.outcome == 'success'}}"; then
          echo "Update available and build successful"
          echo "outcome=update-success" >> "$GITHUB_OUTPUT";
        elif "${{steps.build-lean.outcome == 'failure'}}"; then
          echo "Update available but build fails"
          echo "outcome=update-fail" >> "$GITHUB_OUTPUT"
        fi
      shell: bash

    - name: Open PR if the updated lean build was successful
      if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'pr'
      uses: peter-evans/create-pull-request@v7
      with:
        title: "Updates available and ready to merge"
        body: "To do: add useful details here..."
        delete-branch: true
        branch-suffix: random
        branch: auto-update/patch
        labels: "auto-update-lean"

    - name: Open issue if the updated lean build was successful
      if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'issue'
      run: |
        gh issue create \
          --title "$TITLE" \
          --label "$LABELS" \
          --body "$BODY"
      env:
        # Could be best to use the default token here
        GH_TOKEN: ${{ inputs.token }}
        GH_REPO: ${{ github.repository }}
        TITLE: Updates available and have been tested to build correctly
        BODY: |
          Some more useful info could be added here...
      shell: bash

    - name: Commit update if the updated lean build was successful
      if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'commit'
      uses: EndBug/add-and-commit@v9.1.4
      with:
        default_author: github_actions

    - name: Open issue if the updated lean build fails
      if: steps.build-lean.outcome == 'failure' && inputs.on_update_fails == 'issue'
      run: |
        gh issue create \
          --title "$TITLE" \
          --label "$LABELS" \
          --body "$BODY"
      env:
        GH_TOKEN: ${{ inputs.token }}
        GH_REPO: ${{ github.repository }}
        TITLE: Updates available but manual intervention required
        # LABELS: bug
        BODY: |
          Try `lake update` and then investigate why this update causes the lean build to fail.
          Files changed in update: ${{ steps.check-update.outputs.changed_files }}
      shell: bash

    - name: Action fails if the updated lean build fails
      if: steps.build-lean.outcome == 'failure' && inputs.on_update_fails == 'fail'
      run: exit 1
      shell: bash

branding:
  icon: "download-cloud"
  color: "blue"