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 (header, parserState, messages) ← Parser.parseHeader inputCtx let (env, messages) ← Elab.processHeader header opts messages inputCtx 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 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
Jason Gross (Mar 19 2021 at 21:07):
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
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
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):
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