Calculating Floating Point Array with External Executable

Stream: Is there code for X?

[Paul Wintz]

Within Lean, I would like to call an external tool (such as a C++ executable or library) to calculate an array of floating-point values, then use the resulting values to complete a proof. In particular, I want to take a given polynomial and use an external tool to try to construct a sum-of-squares representation of the polynomial---or show that it cannot be done.

Has anybody done this sort of thing before? I saw the page Foreign Function Interface in the manual, which says the interface for calling external libraries is unstable. Are there any alternatives?

[Paul Wintz]

I found this paper from 2017 that does something similar to what I want, except using Mathematica instead of a C++ program.

[Eric Wieser]

"Unstable" here means "the API might change in future versions of Lean" not "the API is unreliable"

[Eric Wieser]

If you don't like the sound of that, having Lean call your program as a subprocess is an option

[Paul Wintz]

How do you call a program as a subprocess? I haven't come across that in the documentation.

[Eric Wieser]

docs#IO.Process.run is one way

[Paul Wintz]

That looks like what I need. Thanks!

[Paul Wintz]

@Eric Wieser, are there any examples that use IO.Process.run that I could see?

[Paul Wintz]

Here is what I have tried for running a process without using any returned values. It doesn't seem to actually execute the given command, though (the file ~/mytestfilefromlean.txt is not created).

def args : IO.Process.SpawnArgs where
  cmd := "touch"
  args : Array String := #["~/mytestfilefromlean.txt"]

#check IO.Process.run args

Using #check was just a shot in the dark. What is the right way to execute the process call?

[Paul Wintz]

My inevitable follow questions will be how to access the output from the process (presumably as a String?)

[Eric Wieser]

Does #eval work?

[Paul Wintz]

When I replace #check with #eval, I get an error that says,

no such file or directory (error code: 2)

I thought maybe this has something to do with not finding my home directory using the ~ alias, but the changing the cmd to "echo" produces the same error:

def args : IO.Process.SpawnArgs where
  cmd := "echo"
  args : Array String := #["Hello, world"]

#eval IO.Process.run args

[Eric Wieser]

I'm not sure that echo is a real command, isn't it just a shell built-in?

[Alex J. Best]

Echo is a real command for me (ubuntu) and the above code produces "Hello, world\n"

[Paul Wintz]

Got it: the problem probably is that I'm on Windows and echo is not available (I typically use Git-Bash so I forget that Windows commands are different). The following code works:

def args : IO.Process.SpawnArgs where
  cmd := "python"
  args : Array String := #["--version"]

#eval IO.Process.run args