unknown package 'Init'

Stream: lean4

[Jason Gross]

(https://github.com/JasonGross/lean-tools/blob/f7582cbc0a94220ce2128681f3a87e0532b399be/LeanTools/FindBug.lean#L10-L25) I'm invoking lean via

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]

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]

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]

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]

My leanpkg.toml is just

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

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

[Kevin Buzzard]

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

[Jason Gross]

$ 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]

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

[Jason Gross]

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

[Kevin Buzzard]

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]

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]

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

[Sebastian Ullrich]

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]

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