expose sub-jobs of the main action

[b-mehta]

In some of my projects, I'd like to only install elan, or only install elan and get cache, without wanting to do any of the (potentially slow) later steps. For instance, if I have a multi-job flow which can run on different setups, the first one needs elan and mathlib cache, can build the oleans for the project, and the next job doesn't need to (slowly) get the cache again. As such, it would be helpful if this action gave me either
a) the option to control which setup / cooldown parts run
b) sub-actions (like the cache action does) which let me do only parts of it

[austinletson]

Thank you for submitting an issue.

You can configure lean-action to only run certain sub-jobs using the action inputs. There are some examples in the Configuring which features lean-action runs section of the README.

Setting auto-config: False is the key here because this will keep lean-action from trying to guess which sub-jobs to run based on the lakefile. See the Breaking up lean-action across workflows for details on auto-config.

Here is an example which only sets up elan:

- name: "use lean-action to set up elan"
  id: lean-action
  uses: leanprover/lean-action@v1
  with:
    auto-config: false # don't automatically run lake build, lake test, lake lint
    use-mathlib-cache: false # don't get the Mathlib cache

Does this help with your use case?

[b-mehta]

Is there a way to run lake exe mk_all after installing elan but before doing the build in this way?

[austinletson]

Yes, you can call lean-action twice. First to setup elan and fetch the mathlib cache and then a second time to run lake build:

steps:
  - uses: actions/checkout@v4
  - uses: leanprover/lean-action@v1 # setup elan and fetch the Mathlib cache
    with:
        auto-config: false # don't automatically run lake build, lake test, lake lint
        use-github-cache: false # avoid using the GitHub cache twice in one workflow
  - name: run `lake exe mk_all`
    run: |
      lake exe mk_all
  - uses: leanprover/lean-action@v1 # will run `lake build`, `lake test`, and `lake lint`

[b-mehta]

Doesn't that mean elan gets setup twice?

[b-mehta]

I have just tested this, and indeed it sets up elan twice, and uses both the mathlib and github caches: mathlib cache in the first step and github cache in the second...

[austinletson]

You are right. It is awkward to run lean-action twice in a single workflow because it installs elan both times.

Although the caches can be configured to run as needed with the use-mathlib-cache and use-github-cache inputs.

I agree that adding functionality similar to your original request would improve this use case. We should at least add an input to control if elan is setup, similar to the existing build/test/lint inputs. I have created #128 to track this specifically.

In addition, it would be nice to expose a setup-lean subaction that only installs elan and downloads the right lean version. This might need a bit more work. If I recall correctly, there was a potential issue with adding subactions. I think it had implications for publishing lean-action on the action marketplace. I will dig up the zulip conversation where we discussed this.

Thanks again for sharing this example!

[b-mehta]

That would indeed help!