docs: improve README.md inputs usage section

README.md

@@ -26,49 +26,52 @@ jobs:
       - uses: leanprover/lean-action@v1-beta
 ```
 
-## Usage
+## Customization
+`lean-action` provides optional configuration inputs to customize the behavior for your specific workflow.
 
 ```yaml
 - uses: leanprover/lean-action@v1-beta
   with:
     # Run lake test.
-    # Allowed values: "true" or "false".
-    # Default: true
-    test: true
+    # Allowed values: "true" | "false".
+    # Default: "true"
+    test: ""
 
-    # Build arguments to pass to `lake build {args}`.
+    # 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.
     build-args: ""
 
     # 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"
+    # Default: "auto"
+    use-mathlib-cache: ""
 
-    # Run "lake exe runLinter" on the specified module.
+    # Run `lake exe runLinter {lint-module}` on the specified module.
     # Project must be downstream of Batteries.
     # Allowed values: name of module to lint.
-    # If lint-module input is not provided, linter will not run.
+    # By default, `lean-action` will not run the linter.
     lint-module: ""
 
-    # Check if the repository is eligible for the reservoir.
-    # Allowed values: "true" or "false".
-    # Default: false
-    check-reservoir-eligibility: false
+    # Check if the repository is eligible for the Reservoir.
+    # Allowed values: "true" | "false".
+    # Default: "false"
+    check-reservoir-eligibility: ""
 
     # 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" or "false".
-    # Default: false
-    lean4checker: false 
-
+    # Allowed values: "true" | "false".
+    # Default: "false"
+    lean4checker: ""
 
     # Enable GitHub caching.
     # Allowed values: "true" or "false".
     # If use-github-cache input is not provided, the action will use GitHub caching by default.
-    use-github-cache: true
+    # Default: "true"
+    use-github-cache: ""
 
     # 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.

action.yml

@@ -8,18 +8,20 @@ description: |
     - lake test (optional)
     - lake exe runLinter (optional, must be downstream of Batteries)
     - check reservoir eligibility (optional)
+    - check environment with lean4checker (optional)
 inputs:
   test:
     description: |
       Run lake test.
-      Allowed values: "true" or "false".
+      Allowed values: "true" | "false".
       If test input is not provided, tests will run by default.
     required: false
     default: "true"
   build-args:
     description: |
-      Build arguments to pass to `lake build {args}`.
+      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:
@@ -32,26 +34,24 @@ inputs:
     default: "auto"
   lint-module:
     description: |
-      Run "lake exe runLinter" on the specified module.
+      Run `lake exe runLinter {lint-module}` on the specified module.
       Project must be downstream of Batteries.
       Allowed values: name of module to lint.
-      If lint-module input is not provided, linter will not run.
+      By default, `lean-action` will not run the linter.
     required: false
     default: ""
   check-reservoir-eligibility:
     description: |
-      Check if the repository is eligible for the reservoir.
-      Allowed values: "true" or "false".
-      If check-reservoir-eligibility input is not provided, the action will not check for reservoir eligibility.
+      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" or "false".
-      If lean4checker input is not provided, the action will not check the environment with lean4checker.
+      Allowed values: "true" | "false".
     required: false
     default: "false"
   use-github-cache: