Accessing `lean_lib`s in a lake executable

Stream: lean4

[Damiano Testa]

In the context of making lake exe mkAll work, it would be nice to access the project libraries automatically within the command. (How) can that be achieved?

For instance, (how) could this main be extended so that it prints the lean_libs of the project?

import Mathlib

def main (args : List String) : IO UInt32 := do
  let libs ← wishfulGet leanLibs
  IO.println libs
  return 0

--  desired output:
--  [Mathlib, Cache, MathlibExtras, Archive, Counterexamples, docs]

[Henrik Böving]

You can technically speaking import Lake, parse the lake file with it and do your thing but that's rather wasteful. The proper way :tm: would be a facet instead of an exe I believe?

CC @Mac Malone

[Damiano Testa]

Even if it is wasteful, could you point me in the direction of how to parse the lakefile?

[Henrik Böving]

I don't remember anymore, you can dig through the lake module in the mathlib docs (alterantively go to definition through the lake code yourself, it has to call the parser somewhere after all). The data structure you want to obtain is a Workspace

Note that the lake API gives you no stability guarantees so if you do this it can be that you end up having to frequently fix your script.

[Damiano Testa]

Ok, thanks! I found a way to get a Workspace, but it was in a weird monad that did not play with IO...

[Damiano Testa]

Anyway, I'll play some more with it, but if someone knows how to do this, I would be very happy to hear about it!

[Henrik Böving]

I mean Mac knows for sure, you just have to wait until he wakes up :P

[Mario Carneiro]

yes, the recommended way to do this is to use the lake API

[Mario Carneiro]

adapting some code I wrote a while ago for a similar purpose:

import Lake.CLI.Main
open Lake Lean

def getLeanLibs : IO (List Name) := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig.{0} { elanInstall?, leanInstall?, lakeInstall? }
  let ws ← MonadError.runEIO <| (loadWorkspace config).run (.eio .normal)
  return ws.root.leanLibs.map (·.name) |>.toList

def main (args : List String) : IO UInt32 := do
  let libs ← getLeanLibs
  IO.println libs
  return 0

[Mario Carneiro]

yes, running stuff in lake's monad from IO is annoying

[Mario Carneiro]

unrelated aside: you don't need to return 0 from main, it can just return an IO Unit

[Damiano Testa]

This is great, Mario! Thank you very much!

[Damiano Testa]

Mario Carneiro said:

unrelated aside: you don't need to return 0 from main, it can just return an IO Unit

I had forgotten about this comment: in the actual implementation, the command returns the number of import all files that needed updating. I consider a "successful mkAll run" to be one where all the files are already imported and the script simply checks this. Otherwise, its exit code is the number of files that it modified.

[Mario Carneiro]

By the way, it sounds like you are writing something that overlaps with some automation @Joe Hendrix worked on for std4#498 (called check_imports.lean). Could the code there be repurposed or generalized, or otherwise unified with this mkAll program?

[Damiano Testa]

The code that Yaël and I have been working on is #11853. I will now take a look at the std PR that you mention. Thanks for the pointer!

[Damiano Testa]

After a quick glance through, it seems that the code in check_imports does something much more sophisticated than what mkAll does.

mkAll simply takes an input directory dir and creates a file dir.lean with lines import files for each .lean file in dir.

The std script seems to have expectations of what each dir content is supposed to be and it also creates a file for each subdir.

I can probably recycle writeImportModule. The mkAll script does very little on top of that, the rest is documentation and linking into the lake machinery.

[Damiano Testa]

The code is in Std.scripts.check_imports: can I import that file from Mathlib?

[Joe Hendrix]

The code in that file can't be imported. Potentially some of the logic could be put in a module actually part of Std. However, if it's a small amount of code (like writeImportModule), it may be better just to make a separate copy so there isn't risk of coupling and breaking downstream if either code ever needs to change.

[Damiano Testa]

Ok, thanks for the information! The whole PR is approximately 60 lines of code and the rest is documentation. I agree that recycling a few lines of code is not worth the effort (and can always be done if/when the writeImportModule code becomes visible).

[Damiano Testa]

After the huge upgrade the lake had recently, I went back to the code that Mario wrote for producing the list of libraries of a project and it no longer works.

Unfortunately, I did not understand the old version and I do not know how to write a new one: does anyone know how to write a function that returns an Array with the names of the libraries on which the current project depends?

Thanks!

[Kim Morrison]

@Damiano Testa, voodoo from poking around src/lake/Lake/Util/MainM.lean:

import Lake.CLI.Main
open Lake Lean

def getLeanLibs : IO (List Name) := do
  let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
  let config ← MonadError.runEIO <| mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
  let ws ← MonadError.runEIO <| (MainM.runLogIO (loadWorkspace config)).toEIO
  return ws.root.leanLibs.map (·.name) |>.toList

def main (args : List String) : IO UInt32 := do
  let libs ← getLeanLibs
  IO.println libs
  return 0

[Damiano Testa]

Kim, thank you very much! I'll try it as soon as I am at a computer!

[Damiano Testa]

Kim, your code worked very well!

I used it to update #11853 -- mk_all as a lean executable.