From 863e3043308ccad417c32e7c29acb43cc5d0e1b5 Mon Sep 17 00:00:00 2001 From: austinletson Date: Thu, 23 May 2024 07:59:18 -0400 Subject: [PATCH 1/6] docs: improve README.md inputs usage section --- README.md | 27 ++++++++++++++------------- action.yml | 15 +++++++-------- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index fcdea93..9a7d22a 100644 --- a/README.md +++ b/README.md @@ -32,38 +32,39 @@ jobs: - uses: leanprover/lean-action@v1-beta with: # Run lake test. - # Allowed values: "true" or "false". + # Allowed values: "true" | "false". # Default: true - test: 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 + # 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". diff --git a/action.yml b/action.yml index 73251bf..5b76498 100644 --- a/action.yml +++ b/action.yml @@ -12,14 +12,15 @@ 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,17 +33,16 @@ 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. + Allowed values: "true" | "false". required: false default: "false" lean4checker: @@ -50,8 +50,7 @@ inputs: 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: From f90d13cefd9decd9d4808dc57c4120ff99caf5d0 Mon Sep 17 00:00:00 2001 From: austinletson Date: Thu, 23 May 2024 08:46:05 -0400 Subject: [PATCH 2/6] fix: quote -> backtick --- README.md | 2 +- action.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 9a7d22a..74ed9f5 100644 --- a/README.md +++ b/README.md @@ -48,7 +48,7 @@ jobs: # Default: "auto" use-mathlib-cache: "" - # Run "lake exe runLinter {lint-module}" 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. # By default, `lean-action` will not run the linter. diff --git a/action.yml b/action.yml index 5b76498..87f132f 100644 --- a/action.yml +++ b/action.yml @@ -33,7 +33,7 @@ inputs: default: "auto" lint-module: description: | - Run "lake exe runLinter {lint-module}" 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. By default, `lean-action` will not run the linter. From 1d543d30ed441c6b44f7a788cab1706690d3bfeb Mon Sep 17 00:00:00 2001 From: austinletson Date: Thu, 30 May 2024 07:05:31 -0400 Subject: [PATCH 3/6] docs: correct punctuation. --- README.md | 4 ++-- action.yml | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 74ed9f5..d51ef78 100644 --- a/README.md +++ b/README.md @@ -33,12 +33,12 @@ jobs: with: # Run lake test. # Allowed values: "true" | "false". - # Default: true + # Default: "true" test: "" # 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 + # 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. diff --git a/action.yml b/action.yml index 87f132f..8c71c5d 100644 --- a/action.yml +++ b/action.yml @@ -8,6 +8,7 @@ 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: | @@ -20,7 +21,7 @@ inputs: 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 + By default, `lean-action` calls `lake build` with no arguments. required: false default: "" use-mathlib-cache: From 45bfcdfa43d19d49668981e9a9be843dbb00e9b0 Mon Sep 17 00:00:00 2001 From: austinletson Date: Thu, 30 May 2024 07:12:40 -0400 Subject: [PATCH 4/6] docs: add description to Usage section --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index d51ef78..3e3c442 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,8 @@ 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 From 5261d23290703d1f55f741a4b2b1848a67a10acd Mon Sep 17 00:00:00 2001 From: austinletson Date: Sat, 1 Jun 2024 07:28:36 -0400 Subject: [PATCH 5/6] doc: update `use-github-cache` to new default formatting --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 3e3c442..981a17c 100644 --- a/README.md +++ b/README.md @@ -70,7 +70,8 @@ jobs: # 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: "" ``` ## Examples From 6cfdec46fccecc56f5441b3e6c8d2ef7958b6c4c Mon Sep 17 00:00:00 2001 From: austinletson Date: Sat, 1 Jun 2024 07:32:27 -0400 Subject: [PATCH 6/6] fix: capitalize Reservoir --- README.md | 2 +- action.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 981a17c..f657dff 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ jobs: # By default, `lean-action` will not run the linter. lint-module: "" - # Check if the repository is eligible for the reservoir. + # Check if the repository is eligible for the Reservoir. # Allowed values: "true" | "false". # Default: "false" check-reservoir-eligibility: "" diff --git a/action.yml b/action.yml index 8c71c5d..6b1964f 100644 --- a/action.yml +++ b/action.yml @@ -42,7 +42,7 @@ inputs: default: "" check-reservoir-eligibility: description: | - Check if the repository is eligible for the reservoir. + Check if the repository is eligible for the Reservoir. Allowed values: "true" | "false". required: false default: "false"