system interaction?

Stream: lean4

[Jason Gross]

Is there a way to set environment variables and/or change the current directory?

[Joe Hendrix]

I don't know of a way for this or the argv[0] question, but the IO functionality is very minimal. It's pretty easy to write C functions that can be invoked by Lean. I'll defer to others on whether now is a good time to add PRs to expand Lean's system API.

[Joe Hendrix]

I guess I should say it's fairly "straightforward" for writing C to be callable from Lean to be precise. I've often messed up reference counts.

[Zygimantas Straznickas]

Is there a way to set environment variables and/or change the current directory?

Don't think so, most of what exists is in https://github.com/leanprover/lean4/blob/master/src/Init/System/IO.lean#L322

[Sebastian Ullrich]

You can set environment variables and the cwd when spawning new processes. Doing so in a running process is problematic with multithreading.