mathlib documentation

core.​system.​io

core.​system.​io

constant io_core  :
Type → Type → Type

def io_rand_nat  :
std_gen × std_gen

Equations
@[instance]

@[instance]

@[instance]
def io_core_is_monad (e : Type) :

Equations
def io  :
Type → Type

Equations
def io.​iterate {e α : Type} :
α → (α → io_core e (option α))io_core e α

Equations
def io.​forever {e : Type} :

Equations
def io.​catch {e₁ e₂ α : Type} :
io_core e₁ α(e₁ → io_core e₂ α)io_core e₂ α

Equations
def io.​finally {α e : Type} :
io_core e αio_core e unitio_core e α

Equations
def io.​fail {α : Type} :
stringio α

Equations
def io.​print {α : Type u_1} [has_to_string α] :
α → io unit

Equations
def io.​print_ln {α : Type u_1} [has_to_string α] :
α → io unit

Equations
meta def io.​serialize  :

get the current working directory

Equations

set the current working directory

Equations

Equations

Equations

Equations
meta constant format.​print_using  :

meta def format.​print  :

meta def pp_using {α : Type} [has_to_format α] :
α → optionsio unit

meta def pp {α : Type} [has_to_format α] :
α → io unit

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.

IMPORTANT: this primitive can be used to implement unsafe_perform_io {α : Type} : io α → option α or unsafe_perform_io {α : Type} [inhabited α] : io α → α. This can be accomplished by executing the resulting tactic using an empty tactic_state (we have tactic_state.mk_empty). If unsafe_perform_io is defined, and 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.

meta constant io.​run_tactic {α : Type} :
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.