mathlib3 documentation

core / system.io

The following constants have a builtin implementation

Auxiliary definition used in the builtin implementation of monad_io_random_impl

Equations
@[instance]
@[instance]
@[protected, instance]
def io_core_is_monad (e : Type) :
Equations
@[reducible]
def io (α : Type) :
Equations

Remark: the following definitions can be generalized and defined for any (m : Type -> Type -> Type) that implements the required type classes. However, the generalized versions are very inconvenient to use, (example: #eval io.put_str "hello world" does not work because we don't have enough information to infer m.).

def io.iterate {e α : Type} (a : α) (f : α io_core e (option α)) :
io_core e α
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
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 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.