Zulip Chat Archive

Stream: general

Topic: access system environment variables

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):

Try printenv HOME

Yury G. Kudryashov (Aug 06 2020 at 05:52):

Env vars are expanded by shell, not echo

Yury G. Kudryashov (Aug 06 2020 at 05:53):

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

Kris Brown (Aug 06 2020 at 06:18):

ah great, printenv works!

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 getenv.

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: Aug 03 2023 at 10:10 UTC