action.yml

name: "Lean Action - CI for Lean Projects"
description: |
  Standard CI for Lean projects. 
  Steps:
    - install elan
    - get Mathlib cache (optional, must be downstream of Mathlib)
    - lake build
    - lake test (optional)
    - lake exe runLinter (optional, must be downstream of Batteries)
    - check reservoir eligibility (optional)
    - check environment with lean4checker (optional)
inputs:
  auto-config:
    description: |
      Automatically configure `lean-action` based on the Lake workspace.
      When set to "true", `lean-action` will use the Lake workspace to determine
      the set of features to run on the repository, such as `lake build` and `lake test`.
      Even when set to "true", the user can still override the auto configuration
      with the `build` and `test` inputs.
      Allowed values: "true" or "false".
    required: false
    default: "true"
  build:
    description: |
      Run `lake build`.
      Note, this input takes precedence over `auto-config`.
      Allowed values: "true" | "false" | "default".
    required: false
    default: "default"
  test:
    description: |
      Run `lake test`.
      Note, this input takes precedence over `auto-config`.
      Allowed values: "true" | "false" | "default".
    required: false
    default: "default"
  lint:
    description: |
      Run `lake lint`.
      Note, this input takes precedence over `auto-config`.
      Allowed values: "true" | "false" | "default".
    required: false
    default: "default"
  build-args:
    description: |
      Build arguments to pass to `lake build {build-args}`.
      For example, `build-args: "--quiet"` will run `lake build --quiet`.
      By default, `lean-action` calls `lake build` with no arguments.
    required: false
    default: ""
  use-mathlib-cache:
    description: |
      By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly.
      Setting `use-mathlib-cache` will override automatic detection and run (or not run) `lake exe cache get`.
      Project must be downstream of Mathlib to use the Mathlib cache.
      Allowed values: "true" | "false" | "auto".
    required: false
    default: "auto"
  check-reservoir-eligibility:
    description: |
      Check if the repository is eligible for the Reservoir.
      Allowed values: "true" | "false".
    required: false
    default: "false"
  lean4checker:
    description: |
      Check environment with lean4checker.
      Lean version must be 4.8 or higher.
      The version of lean4checker is automatically detected using `lean-toolchain`.
      Allowed values: "true" | "false".
    required: false
    default: "false"
  use-github-cache:
    description: |
      Enable GitHub caching.
      Allowed values: "true" or "false".
      If use-github-cache input is not provided, `lean-action` will use GitHub caching by default.
    required: false
    default: "true"
  lake-package-directory:
    description: |
      The directory where `lean-action` will look for a Lake package and run `lake build`, etc.
      Allowed values: a valid directory containing a Lake package.
      If lake-package-directory is not provided, `lean-action` will use the root directory of the repository by default.
    required: false
    default: "."
outputs:
  build-status:
    description: |
      The status of the `lake build` step.
      Allowed values: "SUCCESS" | "FAILURE" | "".
    value: ${{ steps.build.outputs.build-status }}
  test-status:
    description: |
      The status of the `lake test` step.
      Allowed values: "SUCCESS" | "FAILURE" | "".
    value: ${{ steps.test.outputs.test-status }}
  lint-status:
    description: |
      The status of the `lake lint` step.
      Allowed values: "SUCCESS" | "FAILURE" | "".
    value: ${{ steps.lint.outputs.lint-status }}
  detected-mathlib:
    description: |
      If lean-action detected a mathlib dependency equals "true"
      otherwise equals "false".
    value: ${{ steps.detect-mathlib.outputs.detected-mathlib }}

runs:
  using: "composite"
  steps: 
    - name: install elan
      run: |
        : Install Elan
        ${GITHUB_ACTION_PATH}/scripts/install_elan.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: configure `lean-action`
      id: config
      env:
        AUTO_CONFIG: ${{ inputs.auto-config }}
        BUILD: ${{ inputs.build }}
        TEST: ${{ inputs.test }}
        LINT: ${{ inputs.lint }}
      run: |
        : Configure Lean Action
        ${GITHUB_ACTION_PATH}/scripts/config.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - uses: actions/cache/restore@v4
      if: ${{ inputs.use-github-cache == 'true' }}
      with:
        path: ${{ inputs.lake-package-directory }}/.lake
        key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
        # if no cache hit, fall back to the cache with same lean-toolchain and lake-manifest.json
        restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}

    - name: detect mathlib
      # only detect Mathlib if the user did not provide the mathlib-cache input
      if: ${{ inputs.use-mathlib-cache == 'auto' }}
      id: detect-mathlib
      run: |
        : Detect Mathlib
        ${GITHUB_ACTION_PATH}/scripts/detect_mathlib.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: get mathlib cache
      # only get the cache if Mathlib was detected by detect-mathlib step or if the user explicitly set mathlib-cache to true
      if: ${{ steps.detect-mathlib.outputs.detected-mathlib == 'true' || inputs.use-mathlib-cache == 'true' }}
      run: |
        : Get Mathlib Cache
        echo "::group::Mathlib Cache"
        lake exe cache get
        echo "::endgroup::"
        echo
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: build ${{ github.repository }}
      id: build
      if: ${{ steps.config.outputs.run-lake-build == 'true'}}
      env: 
          BUILD_ARGS: ${{ inputs.build-args }}
      run: |
        : Lake Build
        ${GITHUB_ACTION_PATH}/scripts/lake_build.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - uses: actions/cache/save@v4
      if: ${{ inputs.use-github-cache == 'true' }}
      with:
        path: ${{ inputs.lake-package-directory }}/.lake
        key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

    - name: test ${{ github.repository }}
      id: test
      if: ${{ steps.config.outputs.run-lake-test == 'true'}}
      run: |
        : Lake Test
        ${GITHUB_ACTION_PATH}/scripts/lake_test.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: lint ${{ github.repository }}
      id: lint
      # only run linter if the user provided a module to lint
      if: ${{ steps.config.outputs.run-lake-lint == 'true'}}
      run: |
        : Lake Lint
        ${GITHUB_ACTION_PATH}/scripts/lake_lint.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: check reservoir eligibility
      if: ${{ inputs.check-reservoir-eligibility == 'true' }}
      # Passes in the private status, number of stars, and license id of the repository to check_reservoir_eligibility.sh script
      run: |
        : Check Reservoir Eligibility
        ${GITHUB_ACTION_PATH}/scripts/check_reservoir_eligibility.sh \
          "${{ github.event.repository.private }}"\
          "${{ github.event.repository.stargazers_count }}"\
          "${{ github.event.repository.license.spdx_id }}"
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}

    - name: check environment with lean4checker
      if: ${{ inputs.lean4checker == 'true' }}
      run: |
        : Check Environment with lean4checker
        ${GITHUB_ACTION_PATH}/scripts/run_lean4checker.sh
      shell: bash
      working-directory: ${{ inputs.lake-package-directory }}