access system environment variables

Stream: general

[Kris Brown]

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]

(running on Linux)

[Yury G. Kudryashov]

Try printenv HOME

[Yury G. Kudryashov]

Env vars are expanded by shell, not echo

[Yury G. Kudryashov]

@Gabriel Ebner What should be done to add io.getenv/io.setenv implemented by C getenv/setenv?

[Kris Brown]

ah great, printenv works!

[Gabriel Ebner]

io.setenv is a pretty bad idea with multi-threading, because setenv is global. There is docs#io.env.get for getenv.

[Gabriel Ebner]

If you want to set environment variables for an external process, please use the env field in the docs#io.process.spawn_args structure.