## Stream: lean4

### Topic: unknown package 'Init'

#### Jason Gross (Mar 19 2021 at 20:53):

def runLean (input : String) (opts : Lean.Options) (fileName : String) : IO (Lean.Environment × Lean.MessageLog) := open Lean in do
let inputCtx := Parser.mkInputContext input fileName
let s ← Elab.IO.processCommands inputCtx parserState (Elab.Command.mkState env messages opts)
pure (s.commandState.env, s.commandState.messages)


Currently I'm passing in Lean.Options.empty. Is there something I should be passing in instead so that I don't get error: unknown package 'Init'?

#### Sebastian Ullrich (Mar 19 2021 at 20:59):

Ah. You likely need to call initSearchPath first and give it the path to the stdlib (or do that from outside the process with LEAN_PATH). lean assumes the stdlib is located at ../lib/lean, which likely isn't true for your executable.

#### Jason Gross (Mar 19 2021 at 21:03):

How is it that that lean executable doesn't need me to put the standard library in LEAN_PATH? Also, how do I find where the stdlib is located?

#### Kevin Buzzard (Mar 19 2021 at 21:05):

If you're using elan then I guess it's finding a leanpkg.toml nearby . I guess I have a gazillion copies of Lean 3 and a few Lean 4's in ~/.elan/toolchains

#### Jason Gross (Mar 19 2021 at 21:07):

My leanpkg.toml is just

[package]
name = "Syntax"
version = "0.1"


so I don't see how that helps...

#### Kevin Buzzard (Mar 19 2021 at 21:08):

heh :-) Then probably it's using some default toolchain. Try elan show?

#### Jason Gross (Mar 19 2021 at 21:08):

\$ elan show
installed toolchains
--------------------

stable
leanprover-lean4-nightly (default)
leanprover-lean4-stable

active toolchain
----------------

leanprover-lean4-nightly (default)
Lean (version 4.0.0-nightly-2021-03-19, commit 1af02dcaca3c, Release)


#### Kevin Buzzard (Mar 19 2021 at 21:09):

then you're using the copy of Lean in ~/.elan/toolchains/leanprover-lean4-nightly I should think.

#### Jason Gross (Mar 19 2021 at 21:09):

So I guess the stdlib is in /home/jgross/.elan/toolchains/leanprover-lean4-nightly/lib/lean/

#### Kevin Buzzard (Mar 19 2021 at 21:10):

I'm no expert on Lean 4 but that was how it worked with Lean 3 and I guess elan didn't change much since then.

#### Jason Gross (Mar 19 2021 at 21:11):

And indeed LEAN_PATH=/home/jgross/.elan/toolchains/leanprover-lean4-nightly/lib/lean/:././build gets me further (thanks @Sebastian Ullrich and @Kevin Buzzard !) (though I'm still confused about how Lean is managing to figure this out automatically when I call the lean binary but not when I invoke it through the frontend), but now I'm getting error: could not find native implementation of external declaration 'Nat.div'

#### Zygimantas Straznickas (Mar 19 2021 at 22:10):

Are your running your code in the interpreter or as a compiled binary?

#### Sebastian Ullrich (Mar 19 2021 at 22:24):

Right, there is one more magic incantation necessary: you need to use leanpkg build bin LINK_OPTS=-rdynamic so that the interpreter can find native functions. We should probably gather all this information somewhere...

#### Zygimantas Straznickas (Mar 19 2021 at 22:25):

Does this effectively make the linker keep all the symbols from static libs?

Last updated: May 07 2021 at 13:21 UTC