Running lean-action in all files

Stream: general

[Iván Renison]

Hi, I'm using leanprover/lean-action@v1 in my project. Currently it only checks the files that are imported in the main project file. I wanted to ask if it is possible to get it to check all Lean files in the repository instead of only those?
And in case that is not possible, is it at least possible to make it check that all lean files are imported in the main file (as it happens in Mathlib)?

[Chris Henson]

Have you seen the mk_all-check input? Not sure if this is what you mean.

[Adam Topaz]

IIUC, this is something you need to set up properly in your lakefile. If you have a lean_lib Foo you can add globs that will become part of the library. The default behavior is that lean_lib Foo means that Foo.lean in the same directory is the entrypoint for the library. You will also need to set up default targets so that the libraries you want to build are built when you call lake build. It would be easier to help if you post your lakefile here.

Edit: I didn't know about mk_all-check. Curious to see if that works!

[Iván Renison]

I didn't see mk_all-check before, sorry, it helps, thank you

[Iván Renison]

I have the default lakefile:

name = "LeanOJProblems"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["LeanOJProblems"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.26.0"

[[lean_lib]]
name = "LeanOJProblems"

[Iván Renison]

Can I make the defaultTargets to be all files? (with out listing each file)

[Adam Topaz]

Add globs to the lean_lib. I assume all your files are inside the LeanOJProblems directory?

[Adam Topaz]

IIRC, this is the syntax:

[[lean_lib]]
name = "LeanOJProblems"
globs = ["LeanOJProblems.*"]

[Iván Renison]

Yes, I my files are in the LeanOJProblems, I will try the globs thing

[Iván Renison]

Is there documentation about the lakefile somewhere? I'm not able to find it

[Chris Henson]

I usually add the glob and also to be explicit have the action run lake exe mk_all --check (enabled by the input I mentioned above)

[Adam Topaz]

https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/

[Iván Renison]

The globs option worked. Thank you very much!