mathlib documentation

core / system.io

def io_rand_nat  :
std_gen × std_gen
Equations
@[instance]
@[instance]
@[protected, instance]
def io_core_is_monad (e : Type) :
Equations
@[reducible]
def io (α : Type) :
Type
Equations
def io.iterate {e α : Type} (a : α) (f : α → io_core e (option α)) :
io_core e α
Equations
def io.forever {e : Type} (a : io_core e unit) :
Equations
def io.catch {e₁ e₂ α : Type} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) :
io_core e₂ α
Equations
def io.finally {α e : Type} (a : io_core e α) (cleanup : io_core e unit) :
io_core e α
Equations
@[protected]
def io.fail {α : Type} (s : string) :
io α
Equations
def io.print {α : Type u_1} [has_to_string α] (s : α) :
Equations
def io.print_ln {α : Type u_1} [has_to_string α] (s : α) :
Equations
meta def io.serialize  :
def io.env.get (env_var : string) :
Equations

get the current working directory

Equations
def io.env.set_cwd (cwd : string) :

set the current working directory

Equations
Equations
def io.fs.mkdir (path : string) (recursive : bool := bool.ff) :
Equations
def io.rand (lo : := std_range.fst) (hi : := std_range.snd) :
Equations
meta constant format.print_using  :
meta def format.print (fmt : format) :
meta def pp_using {α : Type} [has_to_format α] (a : α) (o : options) :
meta def pp {α : Type} [has_to_format α] (a : α) :

Run the external process specified by args.

The process will run to completion with its output captured by a pipe, and read into string which is then returned.

Equations
meta constant tactic.unsafe_run_io {α : Type} :
io αtactic α

This is the "back door" into the io monad, allowing IO computation to be performed during tactic execution. For this to be safe, the IO computation should be ideally free of side effects and independent of its environment. This primitive is used to invoke external tools (e.g., SAT and SMT solvers) from a tactic.

meta constant io.run_tactic {α : Type} (a : tactic α) :
io α

Execute the given tactic with a tactic_state object that contains:

  • The current environment in the virtual machine.
  • The current set of options in the virtual machine.
  • Empty metavariable and local contexts.
  • One single goal of the form true. This action is mainly useful for writing tactics that inspect the environment.
meta constant io.unsafe_perform_io {α : Type} (a : io α) :

Similarly to tactic.unsafe_run_io, this gives an unsafe backdoor to run io inside a pure function.

If unsafe_perform_io is used to perform side-effects, users need to take the following precautions:

  • Use @[noinline] attribute in any function to invokes tactic.unsafe_perform_io. Reason: if the call is inlined, the IO may be performed more than once.

  • Set set_option compiler.cse false before any function that invokes tactic.unsafe_perform_io. This option disables common subexpression elimination. Common subexpression elimination might combine two side effects that were meant to be separate.

TODO[Leo]: add [noinline] attribute and option compiler.cse.