Austin Letson
Austin Letson
@cor @Elias-Graf there seems to be some discussion in the above linked issues as to what operations involving file management should be included in the editor as opposed to externally....
@antoyo @tysteiman What do you think about allowing the user to setting a format string containing the variables `col`, `row`, `total-line-number` like this: ``` [editor.statusline] position_format = "{row}/({total-line-numbers}:{col}" ``` This...
@Kenneth-Mata I am not sure if the behavior has changed since this issue was created, but I was able to bind `"space" "space"` to `:write` with the following entry in...
Based on these requirements, [GitHub recommends we put the custom action in it's own repository](https://docs.github.com/en/actions/creating-actions/about-custom-actions#choosing-a-location-for-your-action). This would allow lean projects to use the action by adding, ```yaml - uses: leanprovercommunity/lean-action@{version-number-tag}...
> I thought it would be nice to include caching the `.lake` directory in the CI. Would this not contribute to increased speeds? @Seasawher We could potentially cache some of...
> It would be fantastic if we could provide a good default for `mathlib-cache`, that just tries to check for Mathlib in the dependencies (a very simple test is "does...
Ah, okay. Thanks for the tip @Kha. I have added the cache action before running any lake commands with the following configuration: ```yaml - uses: actions/cache@v4 with: path: .lake key:...
The action now includes an [optional step to check reservoir eligibility](https://github.com/austinletson/lean-standard-action/blob/main/action.yml#L86) using the [inclusion criteria](https://reservoir.lean-lang.org/inclusion-criteria). It verifies the repository, - is not private - contains a `lake-manifest.json` file - contains...
Thanks for the suggestion, @nomeata. I've added a step to preserve the cache after `lake build` but before `lake test`. This ensures that even if any tests fail and halt...
Regarding `lean4checker` and `lake update && lake build`: Integrating tasks which should be scheduled with a cron job while maintaining user-friendly defaults presents a challenge. It appears that users would...