Kris Brown (Aug 06 2020 at 05:17):
I'm generating some files with Lean that I'd like to write relative to a $HOME directory, but it seems like the environment variables aren't showing up, at least with the way I've implemented it below:
import system.io import data.buffer open io.process.stdio def write_file (fname: string) (txt: string): io unit := do h <- io.mk_file_handle fname io.mode.write, io.fs.write h txt.to_char_buffer def run_command (c: string) (arg: list string): io string :=do res <- io.cmd $ io.process.spawn_args.mk c arg piped piped piped none , io.print res, -- for debugging pure res #eval run_command "echo" ["$HOME"] -- just literally prints "$HOME"
Furthermore, I'd like to use environment variables in the
leanpkg.path file, but that hasn't worked either. Are there workarounds for either of these?
Kris Brown (Aug 06 2020 at 05:21):
(running on Linux)
Yury G. Kudryashov (Aug 06 2020 at 05:51):
Yury G. Kudryashov (Aug 06 2020 at 05:52):
Env vars are expanded by shell, not
Yury G. Kudryashov (Aug 06 2020 at 05:53):
@Gabriel Ebner What should be done to add
io.setenv implemented by C
Kris Brown (Aug 06 2020 at 06:18):
Gabriel Ebner (Aug 06 2020 at 08:14):
io.setenv is a pretty bad idea with multi-threading, because
setenv is global. There is docs#io.env.get for
Gabriel Ebner (Aug 06 2020 at 08:15):
If you want to set environment variables for an external process, please use the
env field in the docs#io.process.spawn_args structure.
Last updated: May 08 2021 at 19:11 UTC