Getting the list of `lean_lib`s from a lakefile

Stream: lean4

[Eric Wieser]

Is there a better way to get a (name, globs) list than to run lake translate-config toml and reading the resulting toml file?

[Damiano Testa]

getLeanLibs from scripts/mk_all.lean gets close to this, right?

[Damiano Testa]

E.g., for mathlib, I get

/-- info: #[Mathlib, Archive, Counterexamples, docs, Mathlib/Tactic] -/
#guard_msgs in
#eval do
  dbg_trace ← getLeanLibs

[Eric Wieser]

Thanks, I knew we had an example of that somewhere!

[Damiano Testa]

open Lean System.FilePath

open Lake in
/-- `getLeanLibs` returns the names (as an `Array` of `String`s) of all the libraries
on which the current project depends.
If the current project is `mathlib`, then it excludes the libraries `Cache` and `LongestPole` and
it includes `Mathlib/Tactic`. -/
def getLeanLibs : IO (Array (String × Array String)) := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  let some ws ← loadWorkspace config |>.toBaseIO
    | throw <| IO.userError "failed to load Lake workspace"
  let package := ws.root
  let libs := (package.leanLibs.map (·.name)).map (·.toString)
  let globs := (package.leanLibs.map (·.config)).map (·.globs)
  let libsGlobs := libs.zip globs
  return libsGlobs.map fun (a, g) => (a, g.map (·.toString))

/--
info: #[(Mathlib, #[Mathlib]), (Cache, #[Cache]), (LongestPole, #[LongestPole]), (MathlibTest, #[MathlibTest.+]), (Archive, #[Archive]), (Counterexamples, #[Counterexamples]), (docs, #[docs])]
-/
#guard_msgs in
#eval do
  dbg_trace ← getLeanLibs

[Damiano Testa]

I edited the script, but not the docstring.

[Damiano Testa]

I see now that MathlibTest has MathlibTest.+ as a glob: funky!