Obtaining environment from another lean folder

Stream: lean4

[Adam Topaz]

I'm trying to figure out how to obtain the environment of a lean file which is located in a separate lean folder.
For now I would be happy with just the env I would get from the imports (i.e. without running the actual commands in the file).
To test this out I made two lean project as follows:

1. lake new test math
2. lake new test mwe

the file test/Test.lean just contained

import Mathlib.Data.Nat.Basic

and I built test with lake build, as usual.

The other folder has a file mwe/Main.lean with the following code:

import Lean

def file := "../test/Test.lean"

open Lean System Elab

def main : IO Unit := do
  let contents ← IO.FS.readFile file
  let ctx := Parser.mkInputContext contents file
  let ⟨hdr, stt, msgs⟩ ← Parser.parseHeader ctx
  Lean.initSearchPath (← Lean.findSysroot)
    ["../test/build/lib", "../test/lake-packages/mathlib/build/lib"]
  let (env, messages) ← processHeader hdr {} msgs ctx
    match env.find? `Nat.two_lt_of_ne with
    | none => IO.println "fail"
    | some _ => IO.println "ok"

But I can't seem to get it to work (i.e. main prints "fail"). What am I missing? I thought it had something to do with the search path, hence the two lines trying to set it up.

[Mac Malone]

@Adam Topaz Mathlib also has dependencies which you are not including in the search path, so that may be making the import fail.

[Mac Malone]

Instead of manually supplying the search path yourself I would suggest just using the default (i.e., Lean.initSearchPath (← Lean.findSysroot)) and using Lake to filling the details. That is, run lake env lean --run ../mwe/Main.lean from test to have it properly configure the environment with test's search paths.

[Adam Topaz]

Thanks @Mac that was indeed the issue.
This works:

import Lean

def file := "../test/Test.lean"

open Lean System Elab

def main : IO Unit := do
  let contents ← IO.FS.readFile file
  let ctx := Parser.mkInputContext contents file
  let ⟨hdr, stt, msgs⟩ ← Parser.parseHeader ctx
  Lean.initSearchPath (← Lean.findSysroot)
    [ "../test/build/lib"
    , "../test/lake-packages/mathlib/build/lib"
    , "../test/lake-packages/Qq/build/lib"
    , "../test/lake-packages/aesop/build/lib"
    , "../test/lake-packages/std/build/lib"
    ]
  let (env, messages) ← processHeader hdr {} msgs ctx
    match env.find? `Nat.two_lt_of_ne with
    | none => IO.println "fail"
    | some _ => IO.println "ok"

I got the search path locations using lake print-paths ... in the test folder.

[Adam Topaz]

Is there some option to make lake print-paths give back absolute paths as opposed to relative ones?

[Mac Malone]

Adam Topaz said:

Is there some option to make lake print-paths give back absolute paths as opposed to relative ones?

No. But you can covert them through some intermediary step (e.g. readlink -m on the command line or IO.FS.realpath in Lean).

[Adam Topaz]

Yes, of course. I was hoping there was some secret shortcut :)

[Mac Malone]

Sadly, no. Lake always uses relative paths itself so it doesn't have any absolute paths to provide you with. :wink: