action.yml

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, relative to the workspace.
      Accepts a comma- or space-separated list of directories, and an entry ending in `/*`
      expands to every immediate subdirectory containing a lakefile, so a repository of sibling
      packages can be updated in one invocation (e.g. `templates/*`). An entry ending in `/**`
      expands the same way but walks the whole tree, reaching a package nested inside another
      package — a fixture workspace that its parent requires by path, say. Both forms skip
      dotted directories, so the dependency checkouts under `.lake` are never swept up. An entry
      prefixed with `!` subtracts instead of adding: it names a directory and drops that directory
      together with everything beneath it, so a broad `benchmarks/**` can still leave one package
      alone (e.g. `benchmarks/** !benchmarks/pinned`). An exclusion carries no glob of its own,
      since it already covers its whole subtree, and one matching nothing is reported in the log.
      Quote the value in YAML: a scalar that starts with `!` is otherwise read as a YAML tag.
      With multiple directories the outputs aggregate: an update or failure in any directory
      reports as such, and each directory gets the Mathlib cache if its own manifest needs it.
    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"

  release_channel:
    description: |
      Which tagged release channel to track. Only meaningful when `release_kind_to_fetch` is `tagged`.
      Allowed values:
        * `stable`: track only the latest stable (non pre-release) tagged release (default)
        * `rc`: track the latest tagged release, including release candidates
      An update lands as a pull request against someone's repository, so moving onto a release
      candidate is opt-in.
    required: false
    default: "stable"

  bump_mode:
    description: |
      How to advance dependencies.
      Allowed values:
        * `lake-update`: run `lake update` to advance dependencies (the upstream behavior).
        * `pinned-tags`: bump `lean-toolchain` to the latest Lean version tag, moving the pinned
          `rev` of managed git dependencies with it. A dependency that has not tagged that version
          — Lean ships patch releases most of the ecosystem skips, so there is no `batteries`
          `v4.33.1` — moves to the newest tag it does publish below the target instead. Only one
          with nothing at or below the target keeps its pin and is reported; post-update
          validation decides whether the result builds. Use this when dependencies are pinned to
          Lean-version tags (e.g. `v4.31.0`) rather than tracking a branch.
      Default: `lake-update`
    required: false
    default: "lake-update"

  pinned_deps:
    description: |
      Only used when `bump_mode` is `pinned-tags`. A comma- or space-separated list of git
      dependency names whose pinned `rev` should be bumped. An empty value means every git
      `require` in the lakefile pinned to a Lean version tag; a dependency pinned to a commit hash
      or a branch is reported and left alone, since rewriting it would silently discard the pin.
      Naming it here opts it back in. Both `lakefile.toml` and `lakefile.lean` are supported.
    required: false
    default: ""

  update_lean4_nix:
    description: |
      When `true`, check argumentcomputer/lean4-nix's default branch for the latest Lean
      release before publishing an update. If it is missing, skip validation and notifications
      and report `update-deferred`; the next scheduled run retries. Otherwise run
      `nix flake update lean4-nix`, including flake.lock in the same PR.
      Requires Nix 2.19 or newer installed by the caller, and a root flake with
      `inputs.lean4-nix.url = "github:argumentcomputer/lean4-nix"`.
    required: false
    default: "false"

  # ----------------------------------------- #
  # 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"
  mathlib_cache:
    description: |
      What to do when a target package depends on Mathlib and `lake exe cache get` fails.
      Allowed values:
        * `require`: fail validation, reporting the directory and the cache output (default)
        * `optional`: report the failure and build without the cache
      Building Mathlib from source takes hours and usually ends in a timeout, so falling back to
      it silently costs far more than stopping does. Set `optional` when a slow build is
      preferable to no answer at all.
    required: false
    default: "require"
  validate:
    description: |
      Whether to run post-update validation (`lake build`, and `lake test`/`lake lint` when
      drivers exist) after an update: `true` or `false`.

      When unset, defaults to `false` if both `on_update_succeeds` and `on_update_fails` are
      `pr` — the same PR opens on either outcome and that PR's own CI is the authority on
      whether the update builds, so validation would rebuild the whole package (and its
      dependencies, uncached) only to produce a verdict nothing consumes — and `true`
      otherwise. Note the `commit` and `issue` outcomes require a real validation verdict and
      will not fire with `validate: false`.

      When validation is skipped and an update occurred, `result` reports `update-unvalidated`.
    required: false
    default: ""

  # ------------------------- #
  # commit or notify the user #
  # ------------------------- #
  pr:
    description: |
      When `true`, always open a pull request for an update, whatever the validation outcome:
      shorthand for setting both `on_update_succeeds` and `on_update_fails` to `pr`, taking
      precedence over both. With it, validation is skipped by default (see `validate`), since
      the PR's own CI is the authority on whether the update builds.
    required: false
    default: ""
  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.
        * `pr`: open a pull request anyway. Use this to review the bump even when the build fails.
        * `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.

      With the default `github.token`, opening a pull request also needs
      `Settings > Actions > General > Workflow permissions > Allow GitHub Actions to create and
      approve pull requests` enabled on the repository, and the PR it opens will not start any
      workflow runs — GitHub's guard against a workflow triggering itself — so its checks sit
      pending until someone pushes to the branch or reopens it. Pass a PAT or a GitHub App token
      to avoid both.
    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 reports whether an update was available, validated or deferred.

      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.
        * `update-unvalidated`: An update was available and validation was skipped (see `validate`).
        * `update-deferred`: An update is waiting for lean4-nix to publish the latest release.
    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.
        However, in `pinned-tags` bump mode an applied update always moves `lean-toolchain` to exactly
        this release, so workflows can read the resulting version from this output.
      * This value is fetched according to the `release_kind_to_fetch` option.
    value: ${{ steps.update-lean-toolchain.outputs.latest_lean || steps.bump-pinned.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, including an update deferred for lean4-nix.
    value: ${{ steps.record-notify.outputs.notify }}

runs:
  using: "composite"
  steps:
    # `pr: true` collapses the per-outcome settings; every later condition
    # reads the normalized values so the two forms cannot disagree.
    - name: Resolve update outcomes
      id: outcomes
      run: |
        : Resolve update outcomes
        succ="$ON_SUCCESS"
        fail="$ON_FAILURE"
        if [ "$PR" = "true" ]; then
          succ="pr"
          fail="pr"
        fi
        echo "on-success=$succ" | tee -a "$GITHUB_OUTPUT"
        echo "on-failure=$fail" | tee -a "$GITHUB_OUTPUT"
      shell: bash
      env:
        PR: ${{ inputs.pr }}
        ON_SUCCESS: ${{ inputs.on_update_succeeds }}
        ON_FAILURE: ${{ inputs.on_update_fails }}

    - name: Install elan
      # The appended path is the runner's own home directory, not event data.
      run: | # zizmor: ignore[github-env]
        : 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
      if: inputs.bump_mode == 'lake-update'
      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 }}
        RELEASE_CHANNEL: ${{ inputs.release_channel }}
        UPDATE_LEAN_TOOLCHAIN: ${{ inputs.update_lean_toolchain }}

    - name: Update dependencies of ${{ github.repository }}
      if: inputs.bump_mode == 'lake-update'
      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: Bump pinned dependency tags and lean-toolchain in lockstep
      if: inputs.bump_mode == 'pinned-tags'
      id: bump-pinned
      run: |
        : Bump pinned dependency tags
        lake exe leanUpdate bumpPinnedTags
      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 }}
        RELEASE_CHANNEL: ${{ inputs.release_channel }}
        PINNED_DEPS: ${{ inputs.pinned_deps }}

    - 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: Update lean4-nix and wait for toolchain support
      if: inputs.update_lean4_nix == 'true' && env.LEAN_UPDATE_FILES_CHANGED == 'true'
      id: update-lean4-nix
      run: |
        releases=$(gh api repos/argumentcomputer/lean4-nix/contents/data/toolchains.json \
          -H 'Accept: application/vnd.github.raw+json')
        ready=$(jq -r --arg tag "$LEAN_UPDATE_LATEST_LEAN" 'has($tag)' <<< "$releases")
        echo "ready=$ready" >> "$GITHUB_OUTPUT"
        if [ "$ready" != "true" ]; then
          echo "Waiting for lean4-nix to support $LEAN_UPDATE_LATEST_LEAN; skipping this update"
          exit 0
        fi
        nix flake update lean4-nix --refresh
      shell: bash
      working-directory: ${{ github.workspace }}
      env:
        GH_TOKEN: ${{ github.token }}

    - name: Decide whether to validate
      id: validation-mode
      run: |
        : Decide whether to validate
        if [ "$VALIDATE" = "false" ]; then
          run=false
        elif [ "$VALIDATE" = "true" ]; then
          run=true
        elif [ "$ON_SUCCESS" = "pr" ] && [ "$ON_FAILURE" = "pr" ]; then
          echo "Both outcomes open a PR, whose own CI is the authority; skipping validation"
          run=false
        else
          run=true
        fi
        echo "run=$run" | tee -a "$GITHUB_OUTPUT"
      shell: bash
      env:
        VALIDATE: ${{ inputs.validate }}
        ON_SUCCESS: ${{ steps.outcomes.outputs.on-success }}
        ON_FAILURE: ${{ steps.outcomes.outputs.on-failure }}

    - name: Validate updated Lean package
      if: steps.update-lean4-nix.outputs.ready != 'false' &&
          steps.validation-mode.outputs.run == 'true' && 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 }}
        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
        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
      env:
        LEAN4_NIX_READY: ${{ steps.update-lean4-nix.outputs.ready }}
        VALIDATE_OUTCOME: ${{ steps.validate-update.outcome }}
      run: |
        : Record the outcome
        if [ "$LEAN4_NIX_READY" == "false" ]; then
          echo "Update is waiting for lean4-nix"
          echo "outcome=update-deferred" >> "$GITHUB_OUTPUT"
        elif [ "$LEAN_UPDATE_FILES_CHANGED" == "false" ]; then
          echo "No update available"
          echo "outcome=no-update" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "success" ]; then
          echo "Update available and validation successful"
          echo "outcome=update-success" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "failure" ]; then
          echo "Update available but validation fails"
          echo "outcome=update-fail" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "skipped" ]; then
          echo "Update available; validation skipped"
          echo "outcome=update-unvalidated" >> "$GITHUB_OUTPUT"
        fi
      shell: bash

    - name: Record the notify status
      id: record-notify
      env:
        LEAN4_NIX_READY: ${{ steps.update-lean4-nix.outputs.ready }}
        VALIDATE_OUTCOME: ${{ steps.validate-update.outcome }}
      run: |
        : Record the notify status
        if [ "$LEAN4_NIX_READY" == "false" ]; then
          echo "Update deferred until lean4-nix is ready"
          echo "notify=false" >> "$GITHUB_OUTPUT"
        elif [ "$LEAN_UPDATE_FILES_CHANGED" == "false" ]; then
          echo "No updates available, no need to notify"
          echo "notify=false" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "success" ] && [ "$LEAN_UPDATE_DO_UPDATE" == "true" ]; then
          echo "Updates available and validation successful - should notify"
          echo "notify=true" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "failure" ]; then
          echo "Updates available but validation failed - should notify"
          echo "notify=true" >> "$GITHUB_OUTPUT"
        elif [ "$VALIDATE_OUTCOME" == "skipped" ] && [ "$LEAN_UPDATE_DO_UPDATE" == "true" ]; then
          echo "Updates available with validation skipped - 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 #
    # ------------------------- #
    # An open PR for this release is left untouched: it may carry review
    # fixes, and create-pull-request would force-push them away.
    - name: Check for an open update PR
      if: steps.update-lean4-nix.outputs.ready != 'false'
      id: existing-pr
      run: |
        : Check for an open update PR
        echo "open=$(gh pr list --repo "$GITHUB_REPOSITORY" --head "update/lean-$LEAN_UPDATE_LATEST_LEAN" --state open --json number --jq length)" | tee -a "$GITHUB_OUTPUT"
      shell: bash
      env:
        GH_TOKEN: ${{ inputs.token }}

    # One PR step for both outcomes: whether the update built is the PR's own
    # CI's job to report, not the title's.
    # A skipped lookup has no output, which compares equal to zero in expressions.
    - name: Open a pull request
      if: steps.existing-pr.outcome == 'success' && steps.existing-pr.outputs.open == '0' &&
          ((steps.validate-update.outcome == 'success' &&
          steps.outcomes.outputs.on-success == 'pr' &&
          env.LEAN_UPDATE_DO_UPDATE == 'true') ||
          (steps.validate-update.outcome == 'failure' &&
          steps.outcomes.outputs.on-failure == 'pr') ||
          (steps.validate-update.outcome == 'skipped' &&
          steps.outcomes.outputs.on-success == 'pr' &&
          steps.outcomes.outputs.on-failure == 'pr' &&
          env.LEAN_UPDATE_DO_UPDATE == 'true'))
      uses: peter-evans/create-pull-request@5f6978faf089d4d20b00c7766989d076bb2fc7f1 # v8.1.1
      with:
        token: ${{ inputs.token }}
        title: "chore: Update Lean to ${{ env.LEAN_UPDATE_LATEST_LEAN }}"
        commit-message: |
          chore: Update Lean to ${{ env.LEAN_UPDATE_LATEST_LEAN }}

          Toolchain and dependencies bumped by lean-update.
        body: |
          `lean-toolchain` and dependencies updated for Lean release `${{ env.LEAN_UPDATE_LATEST_LEAN }}` by [lean-update](https://github.com/argumentcomputer/lean-update).
        delete-branch: true
        branch: update/lean-${{ env.LEAN_UPDATE_LATEST_LEAN }}
        labels: "auto-update-lean"

    - name: Open issue if post-update validation was successful
      if: steps.validate-update.outcome == 'success' && steps.outcomes.outputs.on-success == '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 }}
        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
        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' && steps.outcomes.outputs.on-success == 'commit' && env.LEAN_UPDATE_DO_UPDATE == 'true'
      uses: EndBug/add-and-commit@cc9c08ba6c8df3b93a8f2db63e89b98368ae2ae8 # v11.1.1
      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' && steps.outcomes.outputs.on-failure == 'issue'
      run: |
        : Open issue if post-update validation fails
        lake exe leanUpdate createIssue
      env:
        GH_TOKEN: ${{ inputs.token }}
        BUILD_ARGS: ${{ inputs.build_args }}
        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
        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' && steps.outcomes.outputs.on-failure == 'fail'
      run: |
        : Action fails if post-update validation fails
        exit 1
      shell: bash

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