Metaprogramming: Importing modules

Stream: lean4

[Adrian Marti]

I am experimenting with using the Lean package in order to produce my own .olean files. I am running into an issue when importing modules. One can reproduce the problem in a new nix flake lean package, where the only source file contains the following code:

import Lean

open Lean

def main (args: List String) : IO Unit := do
  searchPathRef.set ["/nix/store/xn6b2h5izwi786gs5995fn0fcs7yif06-lean-stage1/lib/lean"]

  let env <- importModules [{module := `Init}] Options.empty

-- #eval main []

Interestingly, the editor runs #eval main [] fine, and it even works if I omit running searchPathRef.set, as the search path seems to be set correctly by default. But if I run the executable component of the package with nix run .#executable, I get the following output:

uncaught exception: could not find native implementation of external declaration 'Nat.div'

If I omit the seachPathRef.set ... line, it does not fine the Init module at all when running nix run .#executable, the searchPathRef seems to be the empty list and thus we get the error:

uncaught exception: unknown package 'Init'

Am I missing something? Do I need to manually point to the native implementations of Init? Although it seemed to me that those implementations were already in the .a files in /nix/store/xn6b2h5izwi786gs5995fn0fcs7yif06-lean-stage1/lib/lean.

I am not even interested in using those native implementations, since I only want to create .olean files.

[Sebastian Ullrich]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20package.20'Init'/near/231097911. You should be able to do this in Nix by passing leancFlags = ["-rdynamic"]; to buildLeanPackage.

[Adrian Marti]

Note that setting LEAN_PATH="/nix/store/xn6b2h5izwi786gs5995fn0fcs7yif06-lean-stage1/lib/lean" and running initSearchPath instead of searchPathRef.set... produces exactly the same result:

uncaught exception: could not find native implementation of external declaration 'Nat.div'

[Sebastian Ullrich]

Now, the reason importing can trigger the interpreter in the first place is that the [init] attribute runs code on import to initialize e.g. some IO.Ref objects. This might not be strictly necessary depending on your use case, but currently it cannot be turned off.

[Adrian Marti]

Sebastian Ullrich said:

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/unknown.20package.20'Init'/near/231097911. You should be able to do this in Nix by passing leancFlags = ["-rdynamic"]; to buildLeanPackage.

Okay, thank you, I will try that

[Adrian Marti]

Okay, my code now works if I package it with leanpkg, thanks to the stream you referenced. So that is already big progress and I wouldn't mind changing to using leanpkg instead of nix. But for the record, passing leancFlags = ["-rdynamic"]; to buildLeanPackage did not make a difference and it still outputs the same uncaught exception: could not find native implementation of external declaration 'Nat.div' error.

[Sebastian Ullrich]

Oh I see, we don't use them for linking. I added a new parameter linkFlags for that.

[Adrian Marti]

Thanks! Everything works now!