Utility functions for finding all .lean files or modules in a project.

TODO: getLeanLibs contains a hard-coded choice of which dependencies should be built and which ones should not. Could this be made more structural and robust, possibly with extra Lake support?

def getAllFiles (git : Bool) (ml : String) : IO (Array System.FilePath)

getAllFiles git ml takes all .lean files in the directory ml (recursing into sub-directories) and returns the Array of Strings

#[file₁, ..., fileₙ]

of all their file names. These are not sorted in general.

The input git is a Boolean flag:

• true means that the command uses git ls-files to find the relevant files;
• false means that the command recursively scans all dirs searching for .lean files.

Equations

• One or more equations did not get rendered due to their size.

def getAllModulesSorted (git : Bool) (ml : String) : IO (Array String)

Like getAllFiles, but return an array of module names instead, i.e. names of the form Mathlib.Algebra.Algebra.Basic. In addition, these names are sorted in a platform-independent order.

Equations

• One or more equations did not get rendered due to their size.