Austin Letson

@semorrison A repository under `leanprover` sounds great! For naming, what about `leanprover/lean-action`? Forks will be more clear: `austinletson/lean-action` instead of `austinletson/action`. I an create a README.md and make an initial...

> @austinletson, I have created leanprover/lean-action, and added you as a maintainer. Thanks! I will move over the current version and update documentation to reflect the change.

> I worry that `lean-action` is very generic as a name, particularly when it is likely there will be other lean actions. How about a name that describes what it...

Alright, thanks for the context. @semorrison I have moved the work which was done for this issue to [leanprover/lean-action](https://github.com/leanprover/lean-action) and created a few initial issues there from todos in this...

`lake install lean4checker` will be useful for ci as in #3950

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...

> @austinletson thank you very much :) If you could add the line > > ```lean > with: > auto-config: false > ``` > > to the PR, @shigoel can...

I created draft PR #811, in which the current target module is either the first `lean_exe` root module or the module corresponding to the first `lean_lib` in Lake's environment. However,...

I have updated #811 to use any root modules of `lean_exe` or `lean_lib` default targets.

I created #4608 to get started on this. I am waiting for additional input before adding a way for the user to specify if the `lake init/new` should create the...