Lake script for automatically generating files with imports

Stream: lean4

[Anand Rao Tadipatri]

I have written a Lake script to automatically detect the top-level folders in a Lean repository and generate the corresponding top-level files that import all the files from these folders. Here is the code, in case anyone else finds it useful:

script mkImports do
  let ws ← Lake.getWorkspace
  let [pkg] := ws.packageList.filter (·.dir = ⟨"."⟩) | throw <| IO.userError "Current package not found"
  IO.println s!"Creating imports for package {pkg.name} ...\n"
  for (libName, _) in pkg.leanLibConfigs do
    let dir ← FilePath.walkDir libName.toString >>= Array.filterM (not <$> ·.isDir)
    let filePathToImport : FilePath → String := fun fp ↦ fp.toString.takeWhile (· != FilePath.extSeparator) |>.map <|
      fun c ↦ if c = FilePath.pathSeparator then '.' else c
    let imports := dir.foldl (init := "") <| fun s f ↦ s ++ s!"import {filePathToImport f}\n"
    IO.FS.writeFile (libName.toString ++ ".lean") imports
    IO.println s!"Created imports file for {libName} library."
  return 1

This can be inserted at the end of the lakefile of any Lean4 repository and run using the command lake run mkImports.

[Scott Morrison]

@Anand Rao Tadipatri, would you mind PRing it to mathlib4?

(A question about scripts: do downstream projects inherit them?)

[Anand Rao Tadipatri]

Sure, I will do that in a short while.

(I'm not sure about the answer, actually. I'll try it out on a test set-up.)

[Arthur Paulino]

You might want to look at https://github.com/lurk-lab/yatima/blob/main/lakefile.lean#L133-L144

[Arthur Paulino]

You can run lake run import_all? on CI. Or lake run import_allto generate the file.
The code from the link I posted has a two-fold role, such that the bash script could be scrapped

[Anand Rao Tadipatri]

@Arthur Paulino Thanks for the link. The idea of having a separate import_all?function is a neat one; I have modified my code to emulate the design of the Yatima lakefile.

def getCurrentPackage : ScriptM Package := do
  let ws ← Lake.getWorkspace
  let [pkg] := ws.packageList.filter (·.dir = ⟨"."⟩) | throw <| IO.userError "Current package not found"
  return pkg

def importsForLib (lib : Name) : IO String := do
  let dir ← FilePath.walkDir lib.toString >>= Array.filterM (not <$> ·.isDir)
  let filePathToImport : FilePath → String := fun fp ↦ fp.toString.takeWhile (· != FilePath.extSeparator) |>.map <|
    fun c ↦ if c = FilePath.pathSeparator then '.' else c
  let imports := dir.foldl (init := "") <| fun s f ↦ s ++ s!"import {filePathToImport f}\n"
  return imports

script import_all do
  let pkg ← getCurrentPackage
  IO.println s!"Creating imports for package {pkg.name} ...\n"
  for (lib, _) in pkg.leanLibConfigs do
    let fileName : FilePath := lib.toString ++ ".lean"
    let imports ← importsForLib lib
    IO.FS.writeFile fileName imports
    IO.println s!"Created imports file for {lib} library."
  return 0

script import_all? do
  let pkg ← getCurrentPackage
  IO.println s!"Checking imports for package {pkg.name} ...\n"
  for (lib, _) in pkg.leanLibConfigs do
    let fileName : FilePath := lib.toString ++ ".lean"
    let allImports ← importsForLib lib
    let existingImports ← IO.FS.readFile fileName
    unless existingImports = allImports do
      IO.eprintln s!"Invalid import list for {lib} library."
      IO.eprintln s!"Try running `lake run mkImports`."
      return 1
  IO.println s!"The imports for package {pkg.name} are up to date."
  return 0

[Anand Rao Tadipatri]

Unfortunately, it seems that downstream projects do not inherit lake scripts.

[Anand Rao Tadipatri]

@Scott Morrison I have created a pull request for this on mathlib4: #5593. The existing order of imports in Mathlib.lean is alphabetical, while the order of imports generated by the script import_all is according to the depth-first traversal of the Mathlib directory, which is why import_all? may fail initially (but will succeed after running lake run import_all).

[Mac Malone]

@Anand Rao Tadipatri Some tips. The "current package" (as your script appears to define it) is always simply ws.root. Also, your getCurrentPackage will break if lake is run from another directory via lake -d /some/pkg).

[Mac Malone]

Also, there does not need to be correlation between Lean library's name and its root module. For example, the following is a permissible style:

package foo
lean_lib lib {roots := #[`Foo]}
lean_exe exe {root := `Main}

Thus, I would suggest you use libConfig.roots to find the root module(s) instead. Similarly, I would suggest you iterator over leanLibs instead ofleanLibConfigs and use lib.srcDir to determine the directory where the root modules are stored (as it may not be the current working directory).

[Anand Rao Tadipatri]

Thanks a lot for the suggestions, @Mac. I have updated the script on #5593.