From 2b9013ef881af2d02132136365bff36cbbc3e175 Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Fri, 17 May 2024 14:18:13 -0400
Subject: [PATCH] fix: rename `mathlib-cache` -> `get-mathlib-cache` and
 improve interface

---
 CHANGELOG.md |  1 +
 README.md    | 12 ++++++------
 action.yml   | 16 ++++++++--------
 3 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f40a835..bc38c64 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Changed
 - `lean-action` no longer contains an `actions/checkout` step
+- `mathlib-cache` renamed to `get-mathlib-cache`
 
 ## v1-alpha - 2024-05-12
 
diff --git a/README.md b/README.md
index c517180..c669887 100644
--- a/README.md
+++ b/README.md
@@ -40,11 +40,11 @@ jobs:
     # For example, `build-args: "--quiet"` will run `lake build --quiet`.
     build-args: ""
 
-    # Run "lake exe cache get" before build.
-    # Project must be downstream of Mathlib.
-    # Allowed values: "true" or "false".
-    # If mathlib-cache input is not provided, the action will attempt to automatically detect if the project is downstream of Mathlib.
-    mathlib-cache: ""
+    # 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".
+    use-mathlib-cache: "auto"
 
     # Run "lake exe runLinter" on the specified module.
     # Project must be downstream of Batteries.
@@ -82,7 +82,7 @@ jobs:
 - uses: leanprover/lean-action@v1-alpha
   with:
     test: false
-    mathlib-cache: false
+    use-mathlib-cache: false
 ```
 
 ### Run lake build with `--wfail`
diff --git a/action.yml b/action.yml
index 43bf34b..2f2ee80 100644
--- a/action.yml
+++ b/action.yml
@@ -22,14 +22,14 @@ inputs:
       For example, `build-args: "--quiet"` will run `lake build --quiet`.
     required: false
     default: ""
-  mathlib-cache:
+  use-mathlib-cache:
     description: |
-      Run "lake exe cache get" before build.
-      Project must be downstream of Mathlib.
-      Allowed values: "true" or "false".
-      If mathlib-cache input is not provided, the action will attempt to automatically detect if the project is downstream of Mathlib.
+      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: ""
+    default: "auto"
   lint-module:
     description: |
       Run "lake exe runLinter" on the specified module.
@@ -71,14 +71,14 @@ runs:
 
     - name: detect mathlib
       # only detect Mathlib if the user did not provide the mathlib-cache input
-      if: ${{ inputs.mathlib-cache == '' }}
+      if: ${{ inputs.use-mathlib-cache == 'auto' }}
       id: detect-mathlib
       run: ${{ github.action_path }}/scripts/detect_mathlib.sh
       shell: bash
 
     - 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.mathlib-cache == 'true' }}
+      if: ${{ steps.detect-mathlib.outputs.DETECTED_MATHLIB == 'true' || inputs.use-mathlib-cache == 'true' }}
       run: |
         echo "::group::Mathlib Cache"
         lake exe cache get