Why can't all subdirectories, subfolders, or functions impor

Stream: lean4

[Lewis]

Why can't all subdirectories, subfolders, or Lean functions under a directory be imported when a folder of Mathib is imported? Thanks.

[Shreyas Srinivas]

You can do that by transitive imports

[Shreyas Srinivas]

If I have <subfolder> and <subfolder>.lean which contains all the imports of toplevel files in that subfolder, then you just have to import <subfolder>

[Tomas Skrivan]

Yes I want this too!!! Very often I create a lean file with the same name as the directory and in the file I just include all the files in that directory.

It's really annoying to keep up to date and it is just an unnecessary boilerplate.

[Damiano Testa]

I wrote something like this a long time ago. I do not know if it still works or not, though.

[Shreyas Srinivas]

I think this design comes from rust. There it is useful in choosing which modules you wish to expose to the outside world and which ones are just internal

[Damiano Testa]

I just tried it: the code at the link above essentially works. I am going to copy it here, with just enough adjustments to remove the deprecation!

import Mathlib.Util.GetAllModules
import Lean.Elab.Command

syntax (name := importStar) "import*" "?"? (colGt ident) : command

open Lean in
elab_rules : command | `(command| import* $[?%$info]? $pat:ident) => do
  let stripImp ← getAllModulesSorted false "Mathlib"
  let withDots := stripImp.filter (String.isPrefixOf pat.getId.toString)
  let paths := withDots.map fun s =>
    let spl := String.splitOn s "."
    System.mkFilePath <| spl.dropLast ++ [(spl.getLast?.getD "") ++ ".lean"]
  let names := ← paths.mapM (moduleNameOfFileName . none)
  let newImports : Array Import := names.map ({ module := · })
  let oldAndNewImports := (← getEnv).imports ++ newImports
  if info.isSome then logInfo m!"{"\n".intercalate (withDots.map ("import " ++ ·)).toList}"
  let newEnv := ← importModules oldAndNewImports (← getOptions)
  unsafe enableInitializersExecution
  setEnv newEnv

import* ? Mathlib.Da

#check ENNReal  -- works

[Kim Morrison]

lean4checker will reject this, of course. :-)

[Damiano Testa]

Kim, are you saying that I should not PR this? :smile:

Anyway, this is really just a hack to show that you can do it, not that you should do it!