Runtime code loading

Stream: lean4

[Tasiro]

I'd like to load a function from another file/project/whatever and then use it. The problem is, I want to do that at runtime. I haven't found a way to do so in a "nice" way, such as in e. g. JS or C#. Is that possible?
The main approach I've found involves using the supportinterpreter flag and then using the lean frontend to create a new environment (for lack of a better word) into which the target code is loaded. Then I can create custom strings or syntax objects to feed the interpreter with my requests for the result of the function calls that I want. But that involves a lot of unnecessary syntax objects passing through the interpreter, or something stringly-typed (e. g. by passing the output as json). Alternatively I could take the code containing the target function, and then append my actual code using that function, and then interpret or compile that at runtime.
The interface for executing lean in C might allow just loading both parts into the same environment and then passing objects from one to the other, but I haven't looked at that yet, nor do I know if that would even be allowed. And a pure lean version would be preferable, of course.
Sorry if there is already an answer somewhere, because if so I didn't find it.

[Kim Morrison]

Are you looking for evalExpr?

[Tasiro]

Thank you, that indirectly calls evalConst, which helps. :smile:
evalConst lifts a value out of an environment, and evalExpr uses that by creating a new constant with evaluated expression, and then returning it without converting it to and from Expr on the way back. Is there a way to pass a value into the environment containing the function to be called without converting its arguments to Expr first? And is it necessary to create a new constant in that environment for every invokation?

[Tasiro]

... Or I can just directly take the function and call it outside. That works.