Zulip Chat Archive

Stream: general

Topic: access system environment variables


view this post on Zulip 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?

view this post on Zulip Kris Brown (Aug 06 2020 at 05:21):

(running on Linux)

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 05:51):

Try printenv HOME

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 05:52):

Env vars are expanded by shell, not echo

view this post on Zulip 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?

view this post on Zulip Kris Brown (Aug 06 2020 at 06:18):

ah great, printenv works!

view this post on Zulip 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.

view this post on Zulip 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