name: "Lean update"
description: "Attempts to update lean and dependencies of a lean project"
author: "Oliver Butterley, Asei Inoue(Seasawher)"

inputs:
  # ----------------------------- #
  # general configuration options #
  # ----------------------------- #
  lake_package_directory:
    description: |
      The directory containing the Lake package to update.
      This parameter is passed to the lake-package-directory argument of leanprover/lean-action.
    required: false
    default: "."

  # -------------------------------- #
  # fetching the latest Lean release #
  # -------------------------------- #
  update_lean_toolchain:
    description: |
      Controls whether to update the lean-toolchain file for projects with no dependencies.
      Allowed values:
        * `auto`: Update the lean-toolchain file to the latest release (default behavior)
        * `never`: Do not update the lean-toolchain file
      Default: `auto`
    required: false
    default: "auto"

  release_kind_to_fetch:
    description: |
      The kind of the latest Lean release to fetch.
      This parameter is used only for Lean, not used for fetching other lake dependencies.
      Allowed values:
        * `nightly`: fetch the latest nightly release
        * `tagged`: fetch the latest tagged release (including both stable and pre-releases)
    required: false
    default: "tagged"

  # ----------------------------------------- #
  # run `lake update` and run build/test/lint #
  # ----------------------------------------- #
  legacy_update:
    description: |
      If set to `true`, executes `lake -R -Kenv=dev update` instead of `lake update`.
      Allowed values:
        * `true`: Execute `lake -R -Kenv=dev update`
        * `false`: Execute `lake update`
      Default: `false`
    required: false
    default: "false"
  build_args:
    description: |
      Build arguments to pass to `lake build` during post-update validation.
    required: false
    default: "--log-level=warning"

  # ------------------------- #
  # commit or notify the user #
  # ------------------------- #
  on_update_succeeds:
    description: |
      What to do when an update is available and post-update validation is successful.
      Allowed values:
        * `silent`: Do nothing
        * `commit`: directly commit the updated files
        * `issue`: notify the user by creating an issue. No new issue will be created if one already exists.
        * `pr`: notify the user by creating a pull request. No new PR will be created if one already exists.
      Default: `pr`.
    required: false
    default: "pr"
  on_update_fails:
    description: |
      What to do when an update is available and post-update validation fails.
      Allowed values:
        * `silent`: Do nothing
        * `issue`: notify the user by creating an issue. No new issue will be created if one already exists.
        * `fail`: fail the action.
      Default: `issue`.
    required: false
    default: "issue"
  update_if_modified:
    description: |
      Specifies which files, when updated during `lake update`, will cause the action to update code or notify the user.
      This option does not affect the behavior when post-update validation fails after `lake update`.
      Allowed values:
        * `lean-toolchain`:
          If `lean-toolchain` is specified, this GitHub Action will skip updates unless the Lean version is updated.
          Here, "skipping updates" means "not attempting to update code or send notifications when post-update validation succeeds after lake update".
        * `lake-manifest.json`: if `lake-manifest.json` is specified, this GitHub Action will perform an update if any dependent package is updated.
      Default: `lake-manifest.json`
    required: false
    default: "lake-manifest.json"
  token:
    description: |
      A Github token to be used for committing
    required: false
    default: ${{ github.token }}

outputs:
  has_dependency:
    description: |
      This value is `true` or `false` depending on whether the lake package has dependencies.
    value: ${{ steps.find-dependencies.outputs.has_dependency }}
  result:
    description: |
      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 post-update validation was successful.
        * `update-fail`: An update was available but post-update validation failed.
    value: ${{ steps.record-result.outputs.outcome }}
  latest_lean:
    description: |
      The latest Lean release version, including both stable and pre-release versions.
      This value could be also nightly.

      ## Note
      * This is not necessarily matching to the updated content of the lean-toolchain file of the lake package.
      * This value is fetched according to the `release_kind_to_fetch` option.
    value: ${{ steps.update-lean-toolchain.outputs.latest_lean }}
  notify:
    description: |
      Indicates whether there is an event worth notifying the user about.
      Returns `true` in the following cases:
        * When updates are available and post-update validation succeeds. However, if `update_if_modified` is set to `lean-toolchain`, this is only true when the Lean version has been updated.
        * When updates are available and post-update validation fails.
      Returns `false` in all other cases.
    value: ${{ steps.record-notify.outputs.notify }}

runs:
  using: "composite"
  steps:
    - name: Install elan
      run: |
        : Install elan
        curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
        echo "$HOME/.elan/bin" >> $GITHUB_PATH
      shell: bash

    - name: read lake-manifest.json and find dependencies
      id: find-dependencies
      run: |
        lake exe leanUpdate findDependencies
      shell: bash
      working-directory: ${{ github.action_path }}
      env:
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}

    - name: Update lean-toolchain file
      id: update-lean-toolchain
      run: |
        : Update lean-toolchain file
        lake exe leanUpdate updateLeanToolchain
      shell: bash
      working-directory: ${{ github.action_path }}
      env:
        GH_TOKEN: ${{ github.token }}
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
        RELEASE_KIND_TO_FETCH: ${{ inputs.release_kind_to_fetch }}
        UPDATE_LEAN_TOOLCHAIN: ${{ inputs.update_lean_toolchain }}

    - name: Update dependencies of ${{ github.repository }}
      run: |
        : Update dependencies
        lake exe leanUpdate updateDependencies
      shell: bash
      working-directory: ${{ github.action_path }}
      env:
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
        LEGACY_UPDATE: ${{ inputs.legacy_update }}

    - name: Check if lean-toolchain or lake-manifest.json were updated
      run: |
        lake exe leanUpdate checkChanges
      env:
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
        UPDATE_IF_MODIFIED: ${{ inputs.update_if_modified }}
      shell: bash
      working-directory: ${{ github.action_path }}

    - name: Prepare Lean and get Mathlib cache
      if: env.LEAN_UPDATE_FILES_CHANGED == 'true'
      id: prepare-lean
      continue-on-error: true
      uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1
      with:
        auto-config: "false"
        build: "false"
        test: "false"
        lint: "false"
        use-github-cache: "false"
        lake-package-directory: ${{ inputs.lake_package_directory }}
      env:
        GH_TOKEN: ${{ github.token }}

    - name: Validate updated Lean package
      if: env.LEAN_UPDATE_FILES_CHANGED == 'true'
      id: validate-update
      continue-on-error: true
      run: |
        : Validate updated Lean package
        lake exe leanUpdate validateUpdate
      env:
        BUILD_ARGS: ${{ inputs.build_args }}
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
      shell: bash
      working-directory: ${{ github.action_path }}

    # -------------------------------- #
    # record the output of this action #
    # -------------------------------- #
    - name: Record the outcome
      id: record-result
      run: |
        : Record the outcome
        if [ "${{ env.LEAN_UPDATE_FILES_CHANGED }}" == "false" ]; then
          echo "No update available"
          echo "outcome=no-update" >> $GITHUB_OUTPUT
        elif [ "${{ steps.validate-update.outcome }}" == "success" ]; then
          echo "Update available and validation successful"
          echo "outcome=update-success" >> $GITHUB_OUTPUT
        elif [ "${{ steps.validate-update.outcome }}" == "failure" ]; then
          echo "Update available but validation fails"
          echo "outcome=update-fail" >> $GITHUB_OUTPUT
        fi
      shell: bash

    - name: Record the notify status
      id: record-notify
      run: |
        : Record the notify status
        if [ "${{ env.LEAN_UPDATE_FILES_CHANGED }}" == "false" ]; then
          echo "No updates available, no need to notify"
          echo "notify=false" >> $GITHUB_OUTPUT
        elif [ "${{ steps.validate-update.outcome }}" == "success" ] && [ "${{ env.LEAN_UPDATE_DO_UPDATE }}" == "true" ]; then
          echo "Updates available and validation successful - should notify"
          echo "notify=true" >> $GITHUB_OUTPUT
        elif [ "${{ steps.validate-update.outcome }}" == "failure" ]; then
          echo "Updates available but validation failed - should notify"
          echo "notify=true" >> $GITHUB_OUTPUT
        else
          echo "No need to notify in this case"
          echo "notify=false" >> $GITHUB_OUTPUT
        fi
      shell: bash

    # ------------------------- #
    # when update is successful #
    # ------------------------- #
    - name: Open PR if post-update validation was successful
      if: steps.validate-update.outcome == 'success' &&
          inputs.on_update_succeeds == 'pr' &&
          env.LEAN_UPDATE_DO_UPDATE == 'true' &&
          env.LEAN_UPDATE_LEAN_TOOLCHAIN_UPDATED == 'true'
      uses: peter-evans/create-pull-request@5f6978faf089d4d20b00c7766989d076bb2fc7f1 # v8
      with:
        title: "Updates available and ready to merge"
        body: |
          The `lean-toolchain` file has been updated to the following content:
          ```
          ${{ env.LEAN_UPDATE_NEW_LEAN_TOOLCHAIN_CONTENT }}
          ```
        delete-branch: true
        branch: auto-update-lean/patch
        labels: "auto-update-lean"

    - name: Open PR if post-update validation was successful
      if: steps.validate-update.outcome == 'success' &&
          inputs.on_update_succeeds == 'pr' &&
          env.LEAN_UPDATE_DO_UPDATE == 'true' &&
          env.LEAN_UPDATE_LEAN_TOOLCHAIN_UPDATED == 'false'
      uses: peter-evans/create-pull-request@5f6978faf089d4d20b00c7766989d076bb2fc7f1 # v8
      with:
        title: "Updates available and ready to merge"
        body: ""
        delete-branch: true
        branch: auto-update-lean/patch
        labels: "auto-update-lean"

    - name: Open issue if post-update validation was successful
      if: steps.validate-update.outcome == 'success' && inputs.on_update_succeeds == 'issue' && env.LEAN_UPDATE_DO_UPDATE == 'true'
      run: |
        : Open issue if post-update validation was successful
        lake exe leanUpdate createIssue
      env:
        # Could be best to use the default token here
        GH_TOKEN: ${{ inputs.token }}
        BUILD_ARGS: ${{ inputs.build_args }}
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
      shell: bash
      working-directory: ${{ github.action_path }}

    - name: Commit update if post-update validation was successful
      if: steps.validate-update.outcome == 'success' && inputs.on_update_succeeds == 'commit' && env.LEAN_UPDATE_DO_UPDATE == 'true'
      uses: EndBug/add-and-commit@645ecc0dd0a57f4d86d26c0aa5fc42c0a856fbca # v11.0.0
      with:
        default_author: github_actions
      env:
        ON_UPDATE_SUCCEEDS: ${{ inputs.on_update_succeeds }}
        DO_UPDATE: ${{ env.LEAN_UPDATE_DO_UPDATE }}

    # ----------------- #
    # when update fails #
    # ----------------- #
    - name: Open issue if post-update validation fails
      if: steps.validate-update.outcome == 'failure' && inputs.on_update_fails == 'issue'
      run: |
        : Open issue if post-update validation fails
        lake exe leanUpdate createIssue
      env:
        GH_TOKEN: ${{ inputs.token }}
        BUILD_ARGS: ${{ inputs.build_args }}
        LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
      shell: bash
      working-directory: ${{ github.action_path }}

    - name: Action fails if post-update validation fails
      if: steps.validate-update.outcome == 'failure' && inputs.on_update_fails == 'fail'
      run: |
        : Action fails if post-update validation fails
        exit 1
      shell: bash

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