refactor: use lean-action in makefile.yml CI workflow

[austinletson]

Description:

lean-action now supports the macOS runner so you can now use it in makefile.yml

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

Closes #82

[austinletson]

Hi @bollu. You may want to change this PR or create a new one based on what you need, but with the latest release, lean-action now supports macOS runners.

There is one thing I wanted to flag after looking at this. By default, lean-action will run lake build. Is this redundant since you also run lake build in the Makefile? Note you can still use lean-action to set up Elan without running lake build by using the auto-config: false input:

  uses: leanprover/lean-action@v1
  with:
    auto-config: false

[bollu]

@austinletson thank you very much :) If you could add the line

 with:
    auto-config: false

to the PR, @shigoel can merge this in tomorrow ^_^

[austinletson]

@austinletson thank you very much :) If you could add the line

 with:
    auto-config: false

to the PR, @shigoel can merge this in tomorrow ^_^

Done!

[bollu]

Thanks! @shigoel I think this is ready for "workflow approval"

[shigoel]

Thank you so much, @austinletson!