Environment import path

Stream: lean4

[Leni Aniva]

Hi people, I'm trying to create separated environments in Lean with Lean.importModules (from Lean/Environment.lean. However when I tried to import the name Lean.Elab, it says

uncaught exception: unknown package 'Lean'

Same thing happens if say I want to import Mathlib.Analysis.Seminorm. I tried to add the environment variable LEAN_PATH=~/.elan/toolchains/leanprover--lean4---nightly-2023-05-06/src/lean/Lean but this still happens. Does anyone know what can I do?

I searched for this error and it seems to come from Lean/Util/Path.lean:findOLean. I compiled Mathlib and I've also tried putting lake-packages/mathlib/build/lib/ into LEAN_PATH. I've confirmed Mathlib.olean exists here.

[Scott Morrison]

You may need to post a (not) working example for us to look at. It seems a lot of things could go wrong!

[Leni Aniva]

Scott Morrison said:

You may need to post a (not) working example for us to look at. It seems a lot of things could go wrong!

Here's the example:

import Lean.Environment

def strTransform (s: String): Lean.Import :=
    let li := s.split (λ c => c == '.')
    let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
    { module := name, runtimeOnly := false }
unsafe def main (args: List String): IO Unit := do
  let env ← Lean.importModules
    (imports := args.map strTransform)
    (opts := {})
    (trustLevel := 1)
  let n := env.constants.size
  IO.println s!"Size: {n}"

run it with

lake build
build/bin/lean-examples "Lean.Elab"

The version is Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

[Leni Aniva]

Also is there a way to see from which locations is Lean searching for modules during Lean.importModules?

[Leni Aniva]

The REPL example here https://github.com/leanprover-community/repl/blob/master/REPL/Main.lean uses IO.processInput which also uses the Lean.importModules function behind the scenes. When I run it, it also shows this error:

{ "cmd" : "import Mathlib.Data.List.Basic\ndef f := 2" }

{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1, "column": 0},
   "endPos": null,
   "data": "unknown package 'Mathlib'"},
  {"severity": "error",
   "pos": {"line": 2, "column": 9},
   "endPos": {"line": 2, "column": 10},
   "data": "unknown constant 'OfNat'"},
  {"severity": "error",
   "pos": {"line": 2, "column": 9},
   "endPos": {"line": 2, "column": 10},
   "data": "unknown constant 'sorryAx'"}],
 "env": 0}

[Sebastian Ullrich]

You are looking for docs4#Lean.initSearchPath, see e.g. how doc-gen4 uses it

[Scott Morrison]

The repl does work, however! Although it doesn't work if you compile it, maybe that is what is going on.

[Scott Morrison]

If you work out how to make the repl work when compiled please do let me know!

[Leni Aniva]

Sebastian Ullrich said:

You are looking for docs4#Lean.initSearchPath, see e.g. how doc-gen4 uses it

I read the code and it seems like this reads from the envvar $LEAN_PATH. I tried setting $LEAN_PATH but there doesn't seem to be any effect on loading.

e.g.

LEAN_PATH=./lib build/bin/lean-examples

[Leni Aniva]

Scott Morrison said:

The repl does work, however! Although it doesn't work if you compile it, maybe that is what is going on.

I just ran it with the ./run script and it gave the above output

[Mauricio Collares]

Does it work if you do lake env ./run?

[Leni Aniva]

Mauricio Collares said:

Does it work if you do lake env ./run?

where should I provide the mathlib path in this case? Nevertheless it does work if I'm importing Lean.Elab instead of Mathlib stuff

{ "cmd" : "import Lean.Elab" }

{"sorries": [], "messages": [], "env": 1}

[Mauricio Collares]

I think it find Mathlib automatically if it's in your lakefile (i.e., if lakefile.lean contains something like require mathlib from git "https://github.com/leanprover-community/mathlib4.git")

[Leni Aniva]

Mauricio Collares said:

Does it work if you do lake env ./run?

ok I just tried a couple more things. Using lake env lean --run Main.lean, my use case could successfully import Lean.Elab, but when I tried to import Mathlib.Analysis.Seminorm it shows

uncaught exception: unknown package 'Std'

Curiously if I do lake env build/bin/lean-examples it doesn't work anymore and shows the same missing package problem

[Leni Aniva]

Mauricio Collares said:

I think it find Mathlib automatically if it's in your lakefile (i.e., if lakefile.lean contains something like require mathlib from git "https://github.com/leanprover-community/mathlib4.git")

Is there a way to make it automatically find Std as well? Std is a dependency of mathlib but it seems like lake env can find mathlib stuff but not Std.

[Mauricio Collares]

It should have found it automatically (it does here). Is Std in your lake-manifest.json? If not, try running lake update

[Leni Aniva]

Scott Morrison said:

If you work out how to make the repl work when compiled please do let me know!

why does it not work when its compiled?

[Sebastian Ullrich]

Precisely because it's missing initSearchPath, which is called by the surrounding interpreter when not compiled

[Leni Aniva]

Mauricio Collares said:

It should have found it automatically (it does here). Is Std in your lake-manifest.json? If not, try running lake update

It is there, but it seems like I have to run lake build in its directory to generate all the .olean files:

$ find lake-packages/std -name "*.olean"

I have already ran lake build on my project directory and it did not compile the dependencies. From lake documentation we have

The next run of lake build (or refreshing dependencies in an editor like VSCode) will clone the mathlib repository and build it.

It did clone the repo but did not build mathlib or any of its dependencies.

[Leni Aniva]

Sebastian Ullrich said:

Precisely because it's missing initSearchPath, which is called by the surrounding interpreter when not compiled

so if I feed it the path it would work?

[Sebastian Ullrich]

Even after correctly setting up LEAN_PATH (which lake env does for your dependencies), something must still call this function

[Leni Aniva]

Sebastian Ullrich said:

Even after correctly setting up LEAN_PATH (which lake env does for your dependencies), something must still call this function

Thanks! I'll try this tomorrow

[Mac Malone]

Leni V. Aniva said:

I have already ran lake build on my project directory and it did not compile the dependencies.

You need to import a Lean module from std4 for Lake to build anything in std4 (e.g. import Std). Lake will only build necessary components. If nothing uses (imports) a module, it will not be built. However, you can force Lake to build a library like Std via lake build Std.

[Leni Aniva]

Scott Morrison said:

If you work out how to make the repl work when compiled please do let me know!

I figured out how to make it work. Following Sebastian's advice, just put

Lean.initSearchPath (<- Lean.findSysroot)

before any invocation to environment stuff, and then execute with lake env build/bin/lean-examples