Automatically check if test runner is available

[Seasawher]

Automatically checks if test_driver or test_runner is defined in lakefile.lean and executes lake test if it is defined, otherwise does not.

It would be tedious to have the user manually enter whether or not to run lake test each time. default input should be auto.

[austinletson]

I think this is the right approach. What do you think about resolving this issue as well as #30 and #46 by introducing improved unified semantics for how users enable the lake build, lake test, and lake lint steps?

[austinletson]

Digging into the details a little more:

As an alternative to having test: auto and lint: auto, we could introduce a boolean auto_config parameter that indicates lean-action should try to determine which steps to run automatically. For now, this would be lake build plus use lake check-test and lake check-lint to determine lake test and lake lint. This input would provide more flexibility for delivering the best default experience as the Lean ecosystem develops and allow users to turn off automatic configuration entirely for more specific use cases, e.g., cron job workflows.

For example, lake init could initialize lean-action as:

- uses: leanprover/lean-action
  with:
    auto_config: true

Users could optionally override the behavior for specific steps while still taking advantage of the automatic configuration:

- uses: leanprover/lean-action
  with:
    auto_config: true
    test: false
    check-reservoir-eligibility: true

Or if they have a specific need in their workflow, such as just running lean4checker in a cron job, they could start from scratch:

- uses: leanprover/lean-action
  with:
    auto-config: false
    lean4checker: true

We could make auto-config: true the default, so 'auto-config' could be omitted in the first two examples above.

What are your thoughts @Seasawher?

[austinletson]

Also see related discussion on #30

[Seasawher]

I think auto-config is unnecessary. Default values for each input option are sufficient.

[Seasawher]

I don't think use-mathlib-cache needs true. The reason is that repositories that do not depend on Mathlib do not use the mathlib cache. I think auto and false are sufficient.

[austinletson]

I think auto-config is unnecessary. Default values for each input option are sufficient.

How do you envision users invoking lean-action when they have a specific need in their workflow, such as only running lean4checker in a cron job?

[Seasawher]

I now understand the intent of auto-config! A workflow that enables only lean4checker can be written concisely with auto-config and is guaranteed to work as originally intended even if new features are added to the lean-action. That sounds good.

[Seasawher]

As an alternative to having test: auto and lint: auto, we could introduce a boolean auto_config parameter that indicates lean-action should try to determine which steps to run automatically.

However, even with auto-config, it would make sense to implement test: auto, lint: auto, or use-mathlib-cache: auto.
This is because it makes no sense to run lake test without test_runner, or to get cache on a repository that does not depend on mathlib. The introduction of auto-config should be managed as a separate issue.

[Seasawher]

I don't think use-mathlib-cache needs true. The reason is that repositories that do not depend on Mathlib do not use the mathlib cache. I think auto and false are sufficient.

how about do you think?

[austinletson]

As an alternative to having test: auto and lint: auto, we could introduce a boolean auto_config parameter that indicates lean-action should try to determine which steps to run automatically.

However, even with auto-config, it would make sense to implement test: auto, lint: auto, or use-mathlib-cache: auto. This is because it makes no sense to run lake test without test_runner, or to get cache on a repository that does not depend on mathlib. The introduction of auto-config should be managed as a separate issue.

I agree that it doesn't make sense to run lake test without a test_runner target (same with lake lint), however, the intention behind adding the check with lake test-check in #26 was to give users a useful error message when trying to configure tests for their package.

If the only option that enables a lake test is test: auto, what happens when lean-action cannot find a test_runner target? Will it silently exclude a lake test step, or will it provide the user with an error?

[austinletson]

I don't think use-mathlib-cache needs true. The reason is that repositories that do not depend on Mathlib do not use the mathlib cache. I think auto and false are sufficient.

how about do you think?

The current mathlib dependency detection uses grep and is brittle. Giving users the option to manually enable the Mathlib cache is intended to safeguard against potential issues with automatic detection.

I just created #57 to use Lake's API instead of grep. After that issue is completed, I think you are right that we should simplify this input to remove the use-mathlib-cache: auto/use-mathlib-cache: true redundancy.

[Seasawher]

If the only option that enables a lake test is test: auto, what happens when lean-action cannot find a test_runner target? Will it silently exclude a lake test step, or will it provide the user with an error?

just exclude! otherwise its hard for other actions use this action in their workflows.

just now I want this action in https://github.com/oliver-butterley/lean-update, so I highly want automatic test_runner detection.

see also: oliver-butterley/lean-update#16

[austinletson]

just exclude! otherwise its hard for other actions use this action in their workflows.

This seems like it goes against the intention of #26, which is to provide users with useful information on lake test if lean-action is unable to detect a test_driver target.

Can you give an example of the use case where it is difficult to use lean-action in other actions workflows?

Sorry, I now understand the use case here in lean-update. Let me think about how this will work with auto-config.

[austinletson]

I have created #60 to track the auto-config input. I plan to open a PR for this soon.

The introduction of auto-config will impact the semantics of the test input, so I would be interested in seeing how that impacts this discussion.

[austinletson]

@Seasawher I just opened #61, which relates to both this issue and #30. Could you look to see if you think the proposed changes would address the use case in lean-update?

[Seasawher]

However with auto-config: true, if lake check-test fails, lean-action will not run lake test and this won't cause lean-action to fail.

This is exactly what we want! Thank you.

[austinletson]

Excellent. I will include this issue in the list of issues closed by #61.

[austinletson]

Closed by #61