initSrcSearchPath

Stream: lean4

[Kim Morrison]

If I run:

import Lean.Util.Paths

open Lean

def main : IO Unit := do
  _ ← (← initSrcSearchPath).findM? fun p => do IO.println p; pure false

#eval main

in a project, it prints something like:

././.lake/packages/batteries/./.
././.lake/packages/Qq/./.
././.lake/packages/aesop/./.
././.lake/packages/aesop/./.
././.lake/packages/proofwidgets/./.
././.lake/packages/proofwidgets/./.
././.lake/packages/Cli/./.
././.lake/packages/importGraph/./.
././.lake/packages/mathlib/./.
././.lake/packages/mathlib/./.
././.lake/packages/mathlib/./.
././.lake/packages/mathlib/./.
././.lake/packages/mathlib/./.
././.lake/packages/mathlib/./.
./././.
/Users/scott/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/src/lean/lake
/Users/scott/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/../src/lean/lake
/Users/scott/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/../src/lean

However when I lake build, it just prints

/Users/scott/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/../src/lean/lake
/Users/scott/.elan/toolchains/leanprover--lean4---v4.8.0-rc2/bin/../src/lean

This is causing polyrith (which relies on this mechanism) to fail under lake build in any projects downstream of Mathlib.

[Kim Morrison]

What is the correct way to locate the Mathlib/scripts/ folder in the Mathlib sources, in a downstream project, in a way that works in both VSCode and under lake build?

[Kim Morrison]

(Pinging @Heather Macbeth, who needs a fix for this for her polyrith tutorial.)

[Kim Morrison]

The underlying difference here is that the LEAN_SRC_PATH environment variable is set when we run in VS Code, but not set during lake build.

[Kim Morrison]

@Mac Malone?

[Eric Wieser]

Does using lake env lake build work?

[Mac Malone]

When Lean is run from lake build, Lake only sets the the minimum environment needed for Lean to build properly., while the server getts the full Lake environment. However, doing otherwise would be a relatively trivial fix.

[Mac Malone]

Eric's lake env lake build is also a stop-gap fix.

[Kim Morrison]

I couldn't get lake env lake build to work.

[Kim Morrison]

Ah!! It did work, but only after lake clean, because it replayed the result from without lake env.

[Kim Morrison]

@Mac Malone can we have a proper fix for this? Currently lake build won't work on any project downstream of mathlib that uses polyrith.

I've created lean#4296 to track this.

[Kim Morrison]

I've also created lean#4297 to discuss whether Lean-specific enviroment variables should be included in deciding whether to rebuild. I suspect the answer is no here, but I'm not sure.

[Eric Wieser]

In theory it's possible for code to depend on non-lean specific environment variables too, at build time

[George Pîrlea]

Looking at lean#4296, I have the same use-case as polyrith (we have a library that invokes a Python script) and the same problem (lake build fails for users of our library, but lake env lake build succeeds).

[Sebastian Ullrich]

And have you evaluated using include_str for this purpose?

[George Pîrlea]

I'm willing to try, but I don't understand how it would work for my use case (invoking at runtime a Python script that ships together with my Lean library).

Is the idea that I would include_str the script, and then at runtime when I need to run the script, save it to a file (whose path I know), then execute the Python interpreter on that file? That seems cumbersome.

[Sebastian Ullrich]

That's not necessary, you can just pass the script as stdin to python

[Sebastian Ullrich]

Just to evaluate other options, what seems to be done in Rust libraries for simple file packaging is to compile the path to the file into the binary at build time, which would be easily achieved in Lean via meta programming. You just can't move the binary afterwards without rebuilding, so it shouldn't be cached in the cloud either.

[George Pîrlea]

I see, that's very helpful. Thank you!

I think the easiest solution for me would be to compile the path into the binary. Does Lean already have a macro to get the path of the current file (similar to file! in Rust)?

[George Pîrlea]

import Lean

/-- The directory of the file being currently compiled. -/
syntax (name := currentDirectory) "currentDirectory!" : term

open Lean Elab Elab.Term in
@[term_elab currentDirectory] def elabCurrentFilePath : TermElab
  | `(currentDirectory!), _ => do
    let ctx ← readThe Lean.Core.Context
    let srcPath := System.FilePath.mk ctx.fileName
    let some srcDir := srcPath.parent
      | throwError "cannot compute parent directory of '{srcPath}'"
    return mkStrLit s!"{srcDir}"
  | _, _ => throwUnsupportedSyntax

Here's an implementation of what I needed, for future reference in case anyone comes across this thread later.

[Kim Morrison]

(I've been meaning to try using include_str for polyrith for long time, but still haven't. If anyone wants to try!! :-)

[Thomas Zhu]

@Kim Morrison In #17626 I refactored Polyrith to remove the dependency on the Python script, and I used include_str for the script sent to the SageMath server. I wasn't aware of this issue here, so I don't know if my PR accidentally affected this issue.

[Kim Morrison]

No no, #17626 is perfect, and I'd missed it. Thank you!

[Sebastian Ullrich]

This solution is still a bit dangerous, especially when globally cached, because a change to the script does not actually rebuild anything, no? Likely there should be a comment in the script file to touch some magic hash in the corresponding .lean file to ensure that. In fact include_str should probably contain that hash, check it at build time, and offer a code action to refresh it.

[Eric Wieser]

Isn't the right mechanism here to tell lake that the Lean file depends on the data file?

[Sebastian Ullrich]

For sure, but it should still be an annotation inside the file so the annotation and file path cannot go out of sync. So that will require feature work in both Lean and Lake.