spawn new process

Stream: general

[Moses Schönfinkel]

Would it be at all possible for a lean tactic to spawn a new process? For example call coqtop? If so, any recommendation as to what file to take a look at? (I don't suppose it's documented.)

[Gabriel Ebner]

leanpkg spawns external processes for almost everything: https://github.com/leanprover/lean/blob/d6d44a19947e2575b3fceed6d61167d258c661fb/leanpkg/leanpkg/main.lean
You can do the same in tactics by lifting the io monad to the tactic monad (don't remember the name of the function)

[Patrick Massot]

I guess there must be hints in that "Lean talks to mathematica" paper

[Moses Schönfinkel]

Thank you. I am giving you 10 out of 10 for today :P! :)

[Patrick Massot]

https://arxiv.org/abs/1712.09288

[Moses Schönfinkel]

Next thing you know we'll be querying google for proofs! ;)

[Sebastian Ullrich]

You can do the same in tactics by lifting the io monad to the tactic monad (don't remember the name of the function)

tactic.unsafe_run_io :) . The unsafe part should vanish soon by basing tactic on io.