how to set environment variable

Stream: lean4

[Asei Inoue]

How to set environment variable in Lean?

[Aaron Liu]

What do you mean by environment variable?

[Asei Inoue]

environment variable in OS, such as LEAN_ABORT_ON_PANIC

[Aaron Liu]

after a quick search I found docs#Std.Internal.IO.Async.System.setEnvVar

[Aaron Liu]

and also docs#Std.Internal.UV.System.osSetenv

[Aaron Liu]

they're both Internal so I'm not sure if it's meant to be used directly

[Kenny Lau]

there's stuff to run a command right

[Aaron Liu]

yeah

[Aaron Liu]

docs#IO.Process.run

[Markus Himmel]

For a variable like LEAN_ABORT_ON_PANIC, you usually set them when invoking the Lean program, not while the Lean program is running. For example, on the command line you can write LEAN_ABORT_ON_PANIC=1 lake exe myprogram.

[Markus Himmel]

But yes, running Std.Internal.IO.Async.System.setEnvVar "LEAN_ABORT_ON_PANIC" "1" does also work (we're going to stabilize this API soon and move it out of the Internal namespace, so no harm in using it except that the name will change without deprecation sometime soon). I would not recommend doing this though, modifying the behavior of your program like that while it is running is asking for trouble.

[Asei Inoue]

Thank you.

but why this code outputs "hello"?
(fail to abort?)

import Std

open Std Internal IO Async

#eval System.setEnvVar "LEAN_ABORT_ON_PANIC" "1"

-- "hello" appears
#eval show IO Unit from do
  let a : Nat := panic! "panic message"
  IO.println a

  IO.println "hello"

[Markus Himmel]

It doesn't for me. In VS Code it crashes the server and when runnning lake build it prints the backtrace and then lake reports "Lean exited with code 134".

[Asei Inoue]

I'm on Windows. It depends on OS?

[Markus Himmel]

Ah, yes, from a quick search it looks like it is known that due to the way that we set and access the environment variables, this update is not picked up on on Windows. We could fix this on the Lean side, but it is probably low priority because like I said you should set this environment variable before running your progam.

[Asei Inoue]

"set environment variable before running you program" works well in Windows, too.

11325@gtune MINGW64 ~/lean-by-example (main)
$ export LEAN_ABORT_ON_PANIC=1

11325@gtune MINGW64 ~/lean-by-example (main)
$ lean --run LeanByExample/Syntax/Panic/Abort.lean
panic message

[Asei Inoue]

my problem is resolved. Thanks!

[Asei Inoue]

oh... in windows, lean --run does not consider this environment variable?

11325@gtune MINGW64 ~/lean-by-example (main)
$ export LEAN_ABORT_ON_PANIC=0

11325@gtune MINGW64 ~/lean-by-example (main)
$ lean --run LeanByExample/Syntax/Panic/Abort.lean
panic message

[Asei Inoue]

the content of LeanByExample/Syntax/Panic/Abort.lean is here:

import Std

open Std Internal IO Async

def main : IO Unit := do
  let a : Nat := panic "panic message"
  IO.println a

  IO.println "hello"

[Markus Himmel]

For LEAN_ABORT_ON_PANIC we only check if the variable has any value at all and interpret this as "should abort" (yes, this is inconsistent with LEAN_BACKTRACE). Try unset LEAN_ABORT_ON_PANIC.