mathlib3 documentation

core / system.io

The following constants have a builtin implementation

source
constant io_core  :
Type → Type → Type
Instances for io_core
source
def io_rand_nat  :
std_gen → ℕ → ℕ → ℕ × std_gen

Auxiliary definition used in the builtin implementation of monad_io_random_impl

Equations
source
@[instance]
constant monad_io_impl  :
monad_io io_core
source
@[instance]
constant monad_io_terminal_impl  :
monad_io_terminal io_core
source
@[instance]
constant monad_io_net_system_impl  :
monad_io_net_system io_core
source
@[instance]
constant monad_io_file_system_impl  :
monad_io_file_system io_core
source
@[instance]
meta constant monad_io_serial_impl  :
monad_io_serial io_core
source
@[instance]
constant monad_io_environment_impl  :
monad_io_environment io_core
source
@[instance]
constant monad_io_process_impl  :
monad_io_process io_core
source
@[instance]
constant monad_io_random_impl  :
monad_io_random io_core
source
@[protected, instance]
def io_core_is_monad (e : Type) :
monad (io_core e)
Equations
source
@[protected, instance]
def io_core_is_monad_fail  :
monad_fail (io_core io.error)
Equations
source
@[protected, instance]
def io_core_is_alternative  :
alternative (io_core io.error)
Equations
source
@[reducible]
def io (α : Type) :
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.).

source
def io.iterate {e α : Type} (a : α) (f : α → io_core e (option α)) :
io_core e α
Equations
source
def io.forever {e : Type} (a : io_core e unit) :
io_core e unit
Equations
source
def io.catch {e₁ e₂ α : Type} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) :
io_core e₂ α
Equations
source
def io.finally {α e : Type} (a : io_core e α) (cleanup : io_core e unit) :
io_core e α
Equations
source
@[protected]
def io.fail {α : Type} (s : string) :
io α
Equations
source
def io.put_str  :
string → io unit
Equations
source
def io.put_str_ln (s : string) :
io unit
Equations
source
def io.get_line  :
io string
Equations
source
def io.cmdline_args  :
io (list string)
Equations
source
def io.print {α : Type u_1} [has_to_string α] (s : α) :
io unit
Equations
source
def io.print_ln {α : Type u_1} [has_to_string α] (s : α) :
io unit
Equations
source
def io.handle  :
Type
Equations
source
def io.mk_file_handle (s : string) (m : io.mode) (bin : bool := bool.ff) :
io io.handle
Equations
source
def io.stdin  :
io io.handle
Equations
source
def io.stderr  :
io io.handle
Equations
source
def io.stdout  :
io io.handle
Equations
source
meta def io.serialize  :
io.handle → expr → io unit
source
meta def io.deserialize  :
io.handle → io expr
source
def io.env.get (env_var : string) :
io (option string)
Equations
source
def io.env.get_cwd  :
io string

get the current working directory

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

set the current working directory

Equations
source
def io.net.socket  :
Type
Equations
source
def io.net.listen  :
string → ℕ → io io.net.socket
Equations
source
def io.net.accept  :
io.net.socket → io io.net.socket
Equations
source
def io.net.connect  :
string → io io.net.socket
Equations
source
def io.net.recv  :
io.net.socket → ℕ → io char_buffer
Equations
source
def io.net.send  :
io.net.socket → char_buffer → io unit
Equations
source
def io.net.close  :
io.net.socket → io unit
Equations
source
def io.fs.is_eof  :
io.handle → io bool
Equations
source
def io.fs.flush  :
io.handle → io unit
Equations
source
def io.fs.close  :
io.handle → io unit
Equations
source
def io.fs.read  :
io.handle → ℕ → io char_buffer
Equations
source
def io.fs.write  :
io.handle → char_buffer → io unit
Equations
source
def io.fs.get_char (h : io.handle) :
io char
Equations
source
def io.fs.get_line  :
io.handle → io char_buffer
Equations
source
def io.fs.put_char (h : io.handle) (c : char) :
io unit
Equations
source
def io.fs.put_str (h : io.handle) (s : string) :
io unit
Equations
source
def io.fs.put_str_ln (h : io.handle) (s : string) :
io unit
Equations
source
def io.fs.read_to_end (h : io.handle) :
io char_buffer
Equations
source
def io.fs.read_file (s : string) (bin : bool := bool.ff) :
io char_buffer
Equations
source
def io.fs.file_exists  :
string → io bool
Equations
source
def io.fs.dir_exists  :
string → io bool
Equations
source
def io.fs.remove  :
string → io unit
Equations
source
def io.fs.rename  :
string → string → io unit
Equations
source
def io.fs.mkdir (path : string) (recursive : bool := bool.ff) :
io bool
Equations
source
def io.fs.rmdir  :
string → io bool
Equations
source
def io.proc.child  :
Type
Equations
source
def io.proc.child.stdin  :
io.proc.child → io.handle
Equations
source
def io.proc.child.stdout  :
io.proc.child → io.handle
Equations
source
def io.proc.child.stderr  :
io.proc.child → io.handle
Equations
source
def io.proc.spawn (p : io.process.spawn_args) :
io io.proc.child
Equations
source
def io.proc.wait (c : io.proc.child) :
io ℕ
Equations
source
def io.proc.sleep (n : ℕ) :
io unit
Equations
source
def io.set_rand_gen  :
std_gen → io unit
Equations
source
def io.rand (lo : ℕ := std_range.fst) (hi : ℕ := std_range.snd) :
io ℕ
Equations
source
meta constant format.print_using  :
format → options → io unit
source
meta def format.print (fmt : format) :
io unit
source
meta def pp_using {α : Type} [has_to_format α] (a : α) (o : options) :
io unit
source
meta def pp {α : Type} [has_to_format α] (a : α) :
io unit
source
def io.cmd (args : io.process.spawn_args) :
io string

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
source
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.

source
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.
source
meta constant io.unsafe_perform_io {α : Type} (a : io α) :
except io.error α

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.