runFrontend on a file with imports

Stream: lean4

[Arthur Paulino]

Hello! :wave:
I'm trying to run Lean.Elab.runFrontend on a file that has imports. It works fine if the file only imports builtin content like Init.Data etc. But when I try to run it on a file that imports content from another file in my project, it causes errors like

examples/Foo.lean:2:0: error: unknown package 'Yatima'
You might need to open '/home/arthur/dev/lean/yatima-lang' as a workspace in your editor
examples/Foo.lean:7:6: error: expected '=>'
examples/Foo.lean:11:6: error: expected '=>'
examples/Foo.lean:15:6: error: expected '=>'
examples/Foo.lean:32:0: error: invalid 'end', insufficient scopes

I'm already doing Lean.initSearchPath $ ← Lean.findSysroot before running the frontend btw. Help is very much appreciated :pray:

[Mac]

How are your running the file that is executing runFrontend? Are you building an executable and doing lake env foo?

[Mac]

LEAN_PATH needs to be augmented with the paths of third-party packages' olean directories in order for imports to work (which is what lake env does).

[Arthur Paulino]

Oh, let me try that!

[Arthur Paulino]

Oh wow that worked! Tyvm @Mac

[Arthur Paulino]

Btw, is there a way for me to set the environment from within my binary so the user doesn't have to use lake env?

[Mac]

If your goal is to support arbitrary third-party packages specified through Lake then, no, not really.

If you have a fixed set of additional modules you want to import, you can add their olean directories to search path via initSearchPath (← Lean.findSysroot) #[<more>, <olean>, <dirs>].

If really don't like using lake env, you can either import Lake itself use it methods to figure out the olean directories of the workspace, or you can invoke lake print-paths <imports> from within your binary to get the set of olean directories for the imports as JSON (see LeanPaths).

[Arthur Paulino]

You mean doing this

import Lake itself use it methods to figure out the olean directories of the workspace

To, then, do this:

initSearchPath (← Lean.findSysroot) #[<more>, <olean>, <dirs>]

Did I get it right?

[Mac]

No

[Mac]

Those were alternative options.

[Mac]

:laughter_tears:

[Arthur Paulino]

import Lake itself use it methods to figure out the olean directories of the workspace

What do I do with those directories?

[Mac]

That is, you can either already have a fixed set of directories you know about and do initSearchPath (← Lean.findSysroot) #[<more>, <olean>, <dirs>. OR, you can import Lake and ask it to figure things out itself. For example, doc-gen4 does approximately this:

let (leanInstall?, lakeInstall?) ← Lake.findInstall?
match Lake.Cli.mkLakeConfig {leanInstall?, lakeInstall?} with
| Except.ok config =>
  let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio
  let lean := config.leanInstall
  if lean.githash ≠ Lean.githash then
    IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
  let lake := config.lakeInstall
  let ctx ← Lake.mkBuildContext ws lean lake
  (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
  let mut sp : Lean.SearchPath := []
  sp ← addSearchPathFromEnv sp
  sp := lake.oleanDir :: lean.oleanDir :: sp
  sp := ws.oleanPath ++ sp
  searchPathRef.set sp
  -- ...
| Except.error err =>
  throw $ IO.userError err.toString

[Arthur Paulino]

Can't I import Lake to figure out the oleans directory and then pass it to initSearchPath (← Lean.findSysroot) #[<more>, <olean>, <dirs>?

[Mac]

Well, that is partly what the above code does. The problem is that initSearchPath does not work they way you want if you have more builtin modules you wish to add (as initSearchPath will prioritize user modules over builtin ones, which can cause bugs).

[Mac]

The above code also builds the imports but you can skip that step if desired.

[Arthur Paulino]

This happens when I import Lake:

error: ld.lld: error: undefined symbol: initialize_Lake
>>> referenced by Frontend.c
>>>               ./build/ir/Yatima/Compiler/Frontend.o:(initialize_Yatima_Compiler_Frontend)
clang: error: linker command failed with exit code 1 (use -v to see invocation)

[Arthur Paulino]

Solution: I had to add Lake as a dependency in my lakefile.lean. Thanks @Henrik Böving!