Add option to disable lake build

[Seasawher]

I sometimes want just to install elan and not to run lake build

[oliver-butterley]

In all the use cases I have encountered it works well to simply include the step:

      - name: Install elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

Do you have something in mind where it would be better to use lean-action with extra options for the task?

[Seasawher]

It is an advantage to be able to provide standard commands to install elan.
After lake build has been replaced by lean-action, it may not be clear what the standard commands are for installing elan.

[Seasawher]

For example, I often see elan installed with commands such as

          run: |
            curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
            echo "$USERPROFILE\.elan\bin" >> $GITHUB_PATH

[oliver-butterley]

• Having such functionality built into an action does have the advantage that if the way to install elan changes then only lean-action needs updating, all other workflows which use it remain as before.

• Additionally, gh action caching is built into lean-action and so could make workflows that use it faster without them needing to add the extra lines to setup caching.

[oliver-butterley]

For example, I often see elan installed with commands such as

          run: |
            curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
            echo "$USERPROFILE\.elan\bin" >> $GITHUB_PATH

Documentation for the possible arguments for elan-init.sh is a bit hidden, I've only seen it in the script file. Different options here to fit different purposes.

Concerning the path, there are various ways that work, the prior one is the suggested way.

[austinletson]

As we expand the inputs to support more use cases, we may want to consider changing the behavior of the inputs so that all the steps are disabled by default and you specify what you want when you call the action. This style is inspired by python-action.

For example,

- uses: leanprover/lean-action
  with:
    build: true
    test: true
    lint: true

The current behavior is a set of steps which are enabled by default (lake build and lake test) and a set which are disabled by default (linting, checking reservoir eligibility, and lean4checker). We then expect the user to know which of the first set they wish to disable and which of the second set they wish to enable. It may be simpler to give the user a menu of steps which they can enable and let them choose what they want.

Note we could still provide a sensible default configuration either when the action is called with no inputs or with a default input:

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

[austinletson]

I ran into a use case for this today while adding some automated functional testing. link

[austinletson]

Closed by #61