lake env for search paths

Stream: lean4

[Adam Topaz]

I'm looking for help about getting the search path from the lake env.
In a new project made using lake new test, I have the following Main.lean

import Lean
import «Test»

def main : IO Unit := do
  IO.println <| ← Lean.searchPathRef.get

Running #eval main in the same file prints a populated search path

[./build/lib, ./build/lib, /home/adam/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/lib/lean, /home/adam/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/lib/lean]

And doing lake env lean --run Main.lean in a terminal does the same. However, lake exe test just prints an empty list [].
How would I go about modifying my main function so that lake exe test will print the correct search path?

[Mario Carneiro]

there is a function like initSearchPath you need to call

[Adam Topaz]

yes I know but that also takes some list to initialize, right?

[Mario Carneiro]

  initSearchPath (← findSysroot)

[Adam Topaz]

Oh that works.

[Adam Topaz]

Thanks! Could you explain a bit more about why this works, just for my understanding? docs4#Lean.initSearchPath has two parameters with the second one having an empty search path as the default.

[Mario Carneiro]

that's just add ons to the search path

[Mario Carneiro]

you don't have to supply anything there

[Adam Topaz]

Aha, I see. Ok, thanks again.

[Mario Carneiro]

I believe that function takes search data from LEAN_PATH environment variable and puts it in Lean.searchPathRef

[Adam Topaz]

docs4#Lean.addSearchPathFromEnv

[Adam Topaz]

so do I understand correctly that lake sets that LEAN_PATH env variable when it's called?

[Adam Topaz]

There's still something I don't understand. I now have the following Main.lean:

import Lean
import «Test»

open Lean

def main : IO Unit := do
  let contents ← IO.FS.readFile "Test.lean"
  let inputCtx := Parser.mkInputContext contents "<input>"
  let (hdr, _, msgs) := ← Parser.parseHeader inputCtx
  initSearchPath (← findSysroot)
  let (env, _) ← Elab.processHeader hdr {} msgs inputCtx
  IO.println s!"Found {env.constants.toList.length} constants."

and Test.lean just has import Lean.

Using lake exe test shows 0 constants, but #eval main (or lake env lean --run Main.lean) gives Found 166803 constants as expected. What am I doing wrong here? Does processHeader need some additional options?

[Mario Carneiro]

I haven't seen processHeader used for this, usually you use importModules to get the environment

[Adam Topaz]

I think leanink does something like this with processHeader

[Mario Carneiro]

oh yes it calls importModules

[Mario Carneiro]

you are ignoring the returned messages, and that function returns an empty env on errors. Try this:

  let (env, msgs) ← Elab.processHeader hdr {} msgs inputCtx
  for msg in msgs.msgs do
    IO.println (← msg.toString)
  IO.println s!"Found {env.constants.toList.length} constants."

[Mario Carneiro]

I'm getting

<input>:1:0: error: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

Found 0 constants.

[Adam Topaz]

Thanks. I’ll try it out when I get back to the computer

[Adam Topaz]

Okay, so printing out the messages does indeed give me exactly what Mario said above:

$ lake exe test
<input>:1:0: error: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

Found 0 constants.

But I still don't understand why this fails but the following works:

$ lake env lean --run Main.lean
Found 166803 constants.

[Mac Malone]

@Adam Topaz you need to add supportInterpreter := true as a configuration option to your lean_exe test. This will make Lean symbols (e.g., UInt64.ofNatCore) available to your executable.

[Adam Topaz]

Thanks @Mac that indeed worked on my "test" project.
I have now tried this in an actual project, where Test.lean is replaced by Mathlib.lean from mathlib4, and I'm getting another error as one of the messages when trying to process the header:

<input>:1:0: error: unknown package 'Init'

with 0 constants found again. Using lake env lean --run ... works though. Is there another configuration option that I'm missing?

Edit: Ignore this -- I had a different bug in my code. All is well now. Thanks Mario and Mac!

[Mac Malone]

Adam Topaz said:

I have now tried this in an actual project, where Test.lean is replaced by Mathlib.lean from mathlib4

What do you mean? Are importing Mathlib.lean in Test.lean or are you building a mathlib executable?