Zulip Chat Archive

Stream: lean4

Topic: system interaction?


view this post on Zulip Jason Gross (Mar 19 2021 at 19:21):

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

view this post on Zulip Joe Hendrix (Mar 19 2021 at 19:25):

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.

view this post on Zulip Joe Hendrix (Mar 19 2021 at 19:28):

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.

view this post on Zulip Zygimantas Straznickas (Mar 19 2021 at 22:00):

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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 22:26):

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


Last updated: May 18 2021 at 23:14 UTC