determine operating system

Stream: lean4

[Jeremy Avigad]

Can I somehow make a system call from within Lean that will tell me whether it is running on Linux, Windows, OS/X, or OS/X ARM?

[Damiano Testa]

There are

• docs#System.Platform.isWindows,
• docs#System.Platform.isOSX,
• docs#System.Platform.isEmscripten.

I neverjust used them and I do not know what Emscripten, but they look promising!

[Damiano Testa]

And there is also

#eval System.Platform.target --  `x86_64-unknown-linux-gnu`, on my computer

[Jeremy Avigad]

Thanks! This is really helpful.

[Damiano Testa]

I do not know why you need them, but I knew about those functions since, when messing with paths, there is already support in IO.FS for dealing with path separators, extensions and such.

[Mario Carneiro]

Damiano Testa said:

I neverjust used them and I do not know what Emscripten, but they look promising!

emscripten is the WASM compiler. But compiling lean to wasm, for running lean client-side on the web, is (unfortunately) no longer really supported and is at "experimental" support level at this point.

[Mario Carneiro]

@Jeremy Avigad Here's the code (extracted from cache) for differentiating the 5 different OS/arch combinations Lean officially supports:

#eval show IO String from do
  if System.Platform.isWindows then
    pure "x86 Windows"
  else
    let arch ← (·.stdout.trim) <$> IO.Process.output { cmd := "uname", args := #["-m"] }
    match arch with
    | "arm64" => if System.Platform.isOSX then pure "ARM OSX" else pure "ARM Linux"
    | "x86_64" => if System.Platform.isOSX then pure "x86 OSX" else pure "x86 Linux"
    | _ => throw <| IO.userError s!"unsupported architecture {arch}"

[Jeremy Avigad]

Thanks to both of you!

@Damiano Testa, I am co-teaching a course with a Lean repository in which students are required to do an exercise with an SMT solver. They create a problem file in Lean, send it to Z3, and then read back and decode the solution. The easiest way to let students call Z3 is to put a copy of each binary in the repository and automatically call the appropriate one. Ultimately it would be nice to have a better solution where e.g. the lakefile requires a "lean-z3" project and e.g. lake exe cache get fetches the right one. But in the meanwhile, this solution does the job.

[Damiano Testa]

Jeremy, that's a cool project: thanks for the details!

Mario, thanks for the explanation about emscripten!