importModule

Stream: lean4

[Patrick Massot]

How is docs4#Lean.importModules meant to be used? If I create a new package with lake init TestImport and put in Main.lean

import Lean
import TestImport
open Lean

def main : IO Unit := do
  let _ ← importModules [{ module := `TestImport : Import }] {} 0
  pure ()

Then running the executable gives uncaught exception: unknown package 'TestImport'.

[Gabriel Ebner]

You need to call initSearchPath first, see also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PrettyPrinter/near/282225104

[Patrick Massot]

Using

import Lean
import TestImport
open Lean

def main : IO Unit := do
  initSearchPath (← findSysroot)
  let _ ← importModules [{ module := `TestImport : Import }] {} 0
  pure ()

doesn't change anything

[Patrick Massot]

(and it was already there is in my actual issue, I missed it while minimizing).

[Gabriel Ebner]

Ah, right. I think that's because findSysroot only works for core Lean executables, because it looks at the path of the current executable (which in your case is nowhere near the core library).

[Gabriel Ebner]

What you can do is embed the compile-time search path in the executable, and then set it at runtime.

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib4/blob/28a4767dc2d247a0d77c943ed689e756b57f946e/scripts/runLinter.lean#L15-L21

[Gabriel Ebner]

https://github.com/leanprover-community/mathlib4/blob/28a4767dc2d247a0d77c943ed689e756b57f946e/scripts/runLinter.lean#L36

[Patrick Massot]

Thanks!

[Mac]

Gabriel Ebner said:

Ah, right. I think that's because findSysroot only works for core Lean executables, because it looks at the path of the current executable (which in your case is nowhere near the core library).

No, findSysroot is specifically to find Lean outside of the core Lean executables. You were right with your initial suggestion. :smile:

@Patrick Massot's problem is simply that he needs to augment the search path with the local of TestImport which he could do, for example, by running the executable via lake env <his-exe> (assuming that TestImport is part of one of Lean libraries mentioned in his lakefle).

[Mac]

Gabriel Ebner said:

What you can do is embed the compile-time search path in the executable, and then set it at runtime.

This seems like really bad idea. Such hard-coding would break the executable on any system which is not your own. findSysroot is the proper way to do this.

[Patrick Massot]

I want to run my executable by executing it, without prefixing it with lake env.

[Mac]

Patrick Massot said:

I want to run my executable by executing it, without prefixing it with lake env.

In order to import TestImport, the Lean interpreter needs to know where to find its olean. Unless you plan to ship the import with the executable, this information needs to come from the outside. Three are three ways to do this: (1) modify the LEAN_PATH environment variable yourself to include the path of TestImport's olean, (2) have lake env do it for you, (3) have some CLI option on your executable that takes such a path and pass a list of such paths to initSearchPath as its second argument.

[Patrick Massot]

I would expect the content of TestImport to be put inside the executable, I don't understand the issue.

[Mac]

@Patrick Massot Sorry, sadly, that is not how the Lean interpreter works. In order to import modules you need an external olean corresponding to that module.

[Mac]

Even Lean's core modules are not exempt from this (their own oleans are distributed as part of the Lean toolchain).

[Patrick Massot]

But surely Lean's core module end up being part of the executable when you build a lean file, right?

[Mac]

Their native symbols / code does get built into the executable, yes, but that is separate from the Lean symbols / code imported by the Lean interpreter (via importModules) for the Lean elaborator to analyze (and use when elaborating / interpreting new Lean code).

[Patrick Massot]

I'll need to think about all that. What I'm trying to do is probably too meta. I need a break anyway. Thanks for your answers.