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.

[Damiano Testa]

This is a very old thread, but I am probably hitting a similar problem.

I have a project (called UpdateDeprecations) that defines a lean script. When I try to get mathlib to depend on it, I add a require line to Mathlib's lakefile, I run lake update UpdateDeprecations and after that lake env update_deprecations works as expected.

However, if I run once lake exe update_deprecations, this appears to have the effect of corrupting the library and the only way out seems to be to run lake update UpdateDeprecations.

[Damiano Testa]

Is there something that I can do so that running lake exe update_deprecations ideally works or at least does not corrupt the command?

[Kim Morrison]

Can you tell us which files change when you run lake exe ...?

[Damiano Testa]

Actually, I am in a worst situation than I thought I was. Trying to find out the latest modified file, I created a fresh copy of mathlib and I realise now that

  Lean.initSearchPath (← Lean.findSysroot)
  -- create the environment with `import UpdateDeprecations`
  let env : Environment ← importModules (leakEnv := true) #[{module := `UpdateDeprecations}] {}

probably only worked before because I had stale cache for UpdateDeprecations. Now, the importModules command reports

uncaught exception: unknown package 'UpdateDeprecations'
You might need to open '/home/damiano/Lean4' as a workspace in your editor

[Damiano Testa]

However, if in VSCode I open a new file with import UpdateDeprecation everything is fine and the declarations in the package are in the environment.

[Damiano Testa]

To reproduce:

• in lakefile.lean, add

require UpdateDeprecations from git "https://github.com/adomani/UpdateDeprecations" @ "caps_dev"

• run

lake update UpdateDeprecations
## make sure that `update_deprecations` exists, print the help page
lake exe update_deprecations --help
## build the cache for an early file
lake build Mathlib.Tactic.Have
## the next command should do nothing (other than printing some debugging messages), but fails instead
lake exe update_deprecations --mods Mathlib/Tactic/Have.lean