def IO.RealWorld : Type

A representation of “the real world” that's used in IO monads to ensure that IO actions are not reordered.

Equations

• IO.RealWorld = Unit

def EIO (ε : Type) : Type → Type

A monad that can have side effects on the external world or throw exceptions of type ε.

BaseIO is a version of this monad that cannot throw exceptions. IO sets the exception type to IO.Error.

Equations

• EIO ε = EStateM ε IO.RealWorld

instance instMonadEIO {ε : Type} : Monad (EIO ε)

Equations

• instMonadEIO = inferInstanceAs (Monad (EStateM ε IO.RealWorld))

instance instMonadFinallyEIO {ε : Type} : MonadFinally (EIO ε)

Equations

• instMonadFinallyEIO = inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))

instance instMonadExceptOfEIO {ε : Type} : MonadExceptOf ε (EIO ε)

Equations

• instMonadExceptOfEIO = inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))

instance instOrElseEIO {ε α : Type} : OrElse (EIO ε α)

Equations

• instOrElseEIO = { orElse := MonadExcept.orElse }

instance instInhabitedEIO {ε α : Type} [Inhabited ε] : Inhabited (EIO ε α)

Equations

• instInhabitedEIO = inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))

def BaseIO : Type → Type

An IO monad that cannot throw exceptions.

Equations

• BaseIO = EIO Empty

instance instMonadBaseIO : Monad BaseIO

Equations

• instMonadBaseIO = inferInstanceAs (Monad (EIO Empty))

instance instMonadFinallyBaseIO : MonadFinally BaseIO

Equations

• instMonadFinallyBaseIO = inferInstanceAs (MonadFinally (EIO Empty))

@[inline]

def BaseIO.toEIO {α ε : Type} (act : BaseIO α) : EIO ε α

Runs a BaseIO action, which cannot throw an exception, in any other EIO monad.

This function is usually used implicitly via automatic monadic lifting rather being than called explicitly.

Equations

• act.toEIO s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok a s

instance instMonadLiftBaseIOEIO {ε : Type} : MonadLift BaseIO (EIO ε)

Equations

• instMonadLiftBaseIOEIO = { monadLift := fun {α : Type} => BaseIO.toEIO }

@[inline]

def EIO.toBaseIO {ε α : Type} (act : EIO ε α) : BaseIO (Except ε α)

Converts an EIO ε action that might throw an exception of type ε into an exception-free BaseIO action that returns an Except value.

Equations

• act.toBaseIO s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s | EStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s

@[inline]

def EIO.catchExceptions {ε α : Type} (act : EIO ε α) (h : ε → BaseIO α) : BaseIO α

Handles any exception that might be thrown by an EIO ε action, transforming it into an exception-free BaseIO action.

Equations

• act.catchExceptions h s = match act s with | EStateM.Result.ok a s => EStateM.Result.ok a s | EStateM.Result.error ex s => h ex s

def EIO.ofExcept {ε α : Type} (e : Except ε α) : EIO ε α

Converts an Except ε action into an EIO ε action.

If the Except ε action throws an exception, then the resulting EIO ε action throws the same exception. Otherwise, the value is returned.

Equations

• EIO.ofExcept (Except.ok a) = pure a
• EIO.ofExcept (Except.error e_2) = throw e_2

@[reducible, inline]

abbrev IO : Type → Type

A monad that supports arbitrary side effects and throwing exceptions of type IO.Error.

Equations

• IO = EIO IO.Error

@[inline]

def BaseIO.toIO {α : Type} (act : BaseIO α) : IO α

Runs a BaseIO action, which cannot throw an exception, as an IO action.

This function is usually used implicitly via automatic monadic lifting rather than being called explicitly.

Equations

• act.toIO = liftM act

@[inline]

def EIO.toIO {ε α : Type} (f : ε → IO.Error) (act : EIO ε α) : IO α

Converts an EIO ε action into an IO action by translating any exceptions that it throws into IO.Errors using f.

Equations

• EIO.toIO f act = EStateM.adaptExcept f act

@[inline]

def EIO.toIO' {ε α : Type} (act : EIO ε α) : IO (Except ε α)

Converts an EIO ε action that might throw an exception of type ε into an exception-free IO action that returns an Except value.

Equations

• act.toIO' = liftM act.toBaseIO

@[inline]

def IO.toEIO {ε α : Type} (f : Error → ε) (act : IO α) : EIO ε α

Runs an IO action in some other EIO monad, using f to translate IO exceptions.

Equations

• IO.toEIO f act = EStateM.adaptExcept f act

@[inline]

unsafe def unsafeBaseIO {α : Type} (fn : BaseIO α) : α

Executes arbitrary side effects in a pure context. This a dangerous operation that can easily undermine important assumptions about the meaning of Lean programs, and it should only be used with great care and a thorough understanding of compiler internals, and even then only to implement observationally pure operations.

This function is not a good way to convert a BaseIO α into an α. Instead, use do-notation.

Because the resulting value is treated as a side-effect-free term, the compiler may re-order, duplicate, or delete calls to this function. The side effect may even be hoisted into a constant, causing the side effect to occur at initialization time, even if it would otherwise never be called.

Equations

• unsafeBaseIO fn = match EStateM.run fn () with | EStateM.Result.ok a a_1 => a

@[inline]

unsafe def unsafeEIO {ε α : Type} (fn : EIO ε α) : Except ε α

Executes arbitrary side effects in a pure context, with exceptions indicated via Except. This a dangerous operation that can easily undermine important assumptions about the meaning of Lean programs, and it should only be used with great care and a thorough understanding of compiler internals, and even then only to implement observationally pure operations.

This function is not a good way to convert an EIO α or IO α into an α. Instead, use do-notation.

Because the resulting value is treated as a side-effect-free term, the compiler may re-order, duplicate, or delete calls to this function. The side effect may even be hoisted into a constant, causing the side effect to occur at initialization time, even if it would otherwise never be called.

Equations

• unsafeEIO fn = unsafeBaseIO fn.toBaseIO

@[inline]

unsafe def unsafeIO {α : Type} (fn : IO α) : Except IO.Error α

A monad that can have side effects on the external world or throw exceptions of type ε.

BaseIO is a version of this monad that cannot throw exceptions. IO sets the exception type to IO.Error.

Equations

• unsafeIO fn = unsafeEIO fn

@[extern lean_io_timeit]

opaque timeit {α : Type} (msg : String) (fn : IO α) : IO α

Times the execution of an IO action.

The provided message msg and the time take are printed to the current standard error as a side effect.

@[extern lean_io_allocprof]

opaque allocprof {α : Type} (msg : String) (fn : IO α) : IO α

@[extern lean_io_initializing]

opaque IO.initializing : BaseIO Bool

Returns true if and only if it is invoked during initialization.

Programs can execute IO actions during an initialization phase that occurs before the main function is executed. The attribute @[init <action>] specifies which IO action is executed to set the value of an opaque constant.

@[extern lean_io_as_task]

opaque BaseIO.asTask {α : Type} (act : BaseIO α) (prio : Task.Priority := Task.Priority.default) : BaseIO (Task α)

Runs act in a separate Task, with priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Pure accesses to the Task do not influence the impure act.

Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

@[extern lean_io_map_task]

opaque BaseIO.mapTask {α : Type u_1} {β : Type} (f : α → BaseIO β) (t : Task α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task β)

Creates a new task that waits for t to complete and then runs the BaseIO action f on its result. This new task has priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

@[extern lean_io_bind_task]

opaque BaseIO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : α → BaseIO (Task β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task β)

Creates a new task that waits for t to complete, runs the IO action f on its result, and then continues as the resulting task. This new task has priority prio.

Running the resulting BaseIO action causes this new task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

def BaseIO.chainTask {α : Type u_1} (t : Task α) (f : α → BaseIO Unit) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO Unit

Creates a new task that waits for t to complete and then runs the IO action f on its result. This new task has priority prio.

This is a version of BaseIO.mapTask that ignores the result value.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• BaseIO.chainTask t f prio sync = discard (BaseIO.mapTask f t prio sync)

def BaseIO.mapTasks {α : Type u_1} {β : Type} (f : List α → BaseIO β) (tasks : List (Task α)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task β)

Creates a new task that waits for all the tasks in the list tasks to complete, and then runs the IO action f on their results. This new task has priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• BaseIO.mapTasks f tasks prio sync = BaseIO.mapTasks.go f prio sync tasks []

def BaseIO.mapTasks.go {α : Type u_1} {β : Type} (f : List α → BaseIO β) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : List (Task α) → List α → BaseIO (Task β)

Equations

• BaseIO.mapTasks.go f prio sync [] x✝ = if sync = true then do let __do_lift ← f x✝.reverse pure { get := __do_lift } else (f x✝.reverse).asTask prio
• BaseIO.mapTasks.go f prio sync [t] x✝ = BaseIO.mapTask (fun (a : α) => f (a :: x✝).reverse) t prio sync
• BaseIO.mapTasks.go f prio sync (t :: ts) x✝ = BaseIO.bindTask t (fun (a : α) => BaseIO.mapTasks.go f prio sync ts (a :: x✝)) prio sync

@[inline]

def EIO.asTask {ε α : Type} (act : EIO ε α) (prio : Task.Priority := Task.Priority.default) : BaseIO (Task (Except ε α))

Runs act in a separate Task, with priority prio. Because EIO ε actions may throw an exception of type ε, the result of the task is an Except ε α.

Running the resulting IO action causes the task to be started eagerly. Pure accesses to the Task do not influence the impure act.

Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• act.asTask prio = act.toBaseIO.asTask prio

@[inline]

def EIO.mapTask {α : Type u_1} {ε β : Type} (f : α → EIO ε β) (t : Task α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except ε β))

Creates a new task that waits for t to complete and then runs the IO action f on its result. This new task has priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped. Because EIO ε actions may throw an exception of type ε, the result of the task is an Except ε α.

Equations

• EIO.mapTask f t prio sync = BaseIO.mapTask (fun (a : α) => (f a).toBaseIO) t prio sync

@[inline]

def EIO.bindTask {α : Type u_1} {ε β : Type} (t : Task α) (f : α → EIO ε (Task (Except ε β))) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except ε β))

Creates a new task that waits for t to complete, runs the EIO ε action f on its result, and then continues as the resulting task. This new task has priority prio.

Running the resulting BaseIO action causes this new task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped. Because EIO ε actions may throw an exception of type ε, the result of the task is an Except ε α.

Equations

• EIO.bindTask t f prio sync = BaseIO.bindTask t (fun (a : α) => (f a).catchExceptions fun (e : ε) => pure { get := Except.error e }) prio sync

def EIO.chainTask {α : Type u_1} {ε : Type} (t : Task α) (f : α → EIO ε Unit) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : EIO ε Unit

Creates a new task that waits for t to complete and then runs the EIO ε action f on its result. This new task has priority prio.

This is a version of EIO.mapTask that ignores the result value.

Running the resulting EIO ε action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• EIO.chainTask t f prio sync = discard (liftM (EIO.mapTask f t prio sync))

@[inline]

def EIO.mapTasks {α : Type u_1} {ε β : Type} (f : List α → EIO ε β) (tasks : List (Task α)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except ε β))

Creates a new task that waits for all the tasks in the list tasks to complete, and then runs the EIO ε action f on their results. This new task has priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• EIO.mapTasks f tasks prio sync = BaseIO.mapTasks (fun (as : List α) => (f as).toBaseIO) tasks prio sync

def IO.ofExcept {ε : Type u_1} {α : Type} [ToString ε] (e : Except ε α) : IO α

Converts an Except ε action into an IO action.

If the Except ε action throws an exception, then the exception type's ToString instance is used to convert it into an IO.Error, which is thrown. Otherwise, the value is returned.

Equations

• IO.ofExcept (Except.ok a) = pure a
• IO.ofExcept (Except.error e_2) = throw (IO.userError (toString e_2))

def IO.lazyPure {α : Type} (fn : Unit → α) : IO α

Creates an IO action that will invoke fn if and when it is executed, returning the result.

Equations

• IO.lazyPure fn = pure (fn ())

@[extern lean_io_mono_ms_now]

opaque IO.monoMsNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in milliseconds. There is no relation to wall clock time.

@[extern lean_io_mono_nanos_now]

opaque IO.monoNanosNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in nanoseconds. There is no relation to wall clock time.

@[extern lean_io_get_random_bytes]

opaque IO.getRandomBytes (nBytes : USize) : IO ByteArray

Reads bytes from a system entropy source. It is not guaranteed to be cryptographically secure.

If nBytes is 0, returns immediately with an empty buffer.

def IO.sleep (ms : UInt32) : BaseIO Unit

Pauses execution for the specified number of milliseconds.

Equations

• IO.sleep ms s = dbgSleep ms fun (x : Unit) => EStateM.Result.ok () s

@[inline]

def IO.asTask {α : Type} (act : IO α) (prio : Task.Priority := Task.Priority.default) : BaseIO (Task (Except Error α))

Runs act in a separate Task, with priority prio. Because IO actions may throw an exception of type IO.Error, the result of the task is an Except IO.Error α.

Running the resulting BaseIO action causes the task to be started eagerly. Pure accesses to the Task do not influence the impure act. Because IO actions may throw an exception of type IO.Error, the result of the task is an Except IO.Error α.

Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• act.asTask prio = EIO.asTask act prio

@[inline]

def IO.mapTask {α : Type u_1} {β : Type} (f : α → IO β) (t : Task α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except Error β))

Creates a new task that waits for t to complete and then runs the IO action f on its result. This new task has priority prio.

Running the resulting BaseIO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped. Because IO actions may throw an exception of type IO.Error, the result of the task is an Except IO.Error α.

Equations

• IO.mapTask f t prio sync = EIO.mapTask f t prio sync

@[inline]

def IO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : α → IO (Task (Except Error β))) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except Error β))

Creates a new task that waits for t to complete, runs the IO action f on its result, and then continues as the resulting task. This new task has priority prio.

Running the resulting BaseIO action causes this new task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped. Because IO actions may throw an exception of type IO.Error, the result of the task is an Except IO.Error α.

Equations

• IO.bindTask t f prio sync = EIO.bindTask t f prio sync

def IO.chainTask {α : Type u_1} (t : Task α) (f : α → IO Unit) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : IO Unit

Creates a new task that waits for t to complete and then runs the IO action f on its result. This new task has priority prio.

This is a version of IO.mapTask that ignores the result value.

Running the resulting IO action causes the task to be started eagerly. Unlike pure tasks created by Task.spawn, tasks created by this function will run even if the last reference to the task is dropped. The act should explicitly check for cancellation via IO.checkCanceled if it should be terminated or otherwise react to the last reference being dropped.

Equations

• IO.chainTask t f prio sync = EIO.chainTask t f prio sync

@[inline]

def IO.mapTasks {α : Type u_1} {β : Type} (f : List α → IO β) (tasks : List (Task α)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except Error β))

IO specialization of EIO.mapTasks.

Equations

• IO.mapTasks f tasks prio sync = EIO.mapTasks f tasks prio sync

@[extern lean_io_check_canceled]

opaque IO.checkCanceled : BaseIO Bool

Checks whether the current task's cancellation flag has been set by calling IO.cancel or by dropping the last reference to the task.

@[extern lean_io_cancel]

opaque IO.cancel {α : Type u_1} : Task α → BaseIO Unit

Requests cooperative cancellation of the task. The task must explicitly call IO.checkCanceled to react to the cancellation.

inductive IO.TaskState : Type

The current state of a Task in the Lean runtime's task manager.

• waiting : TaskState

  The Task is waiting to be run.

  It can be waiting for dependencies to complete or sitting in the task manager queue waiting for a thread to run on.

• running : TaskState

  The Task is actively running on a thread or, in the case of a Promise, waiting for a call to IO.Promise.resolve.

• finished : TaskState

  The Task has finished running and its result is available. Calling Task.get or IO.wait on the task will not block.

instance IO.instInhabitedTaskState : Inhabited TaskState

Equations

• IO.instInhabitedTaskState = { default := IO.TaskState.waiting }

instance IO.instReprTaskState : Repr TaskState

Equations

• IO.instReprTaskState = { reprPrec := IO.reprTaskState✝ }

instance IO.instDecidableEqTaskState : DecidableEq TaskState

Equations

• IO.instDecidableEqTaskState x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance IO.instOrdTaskState : Ord TaskState

Equations

• IO.instOrdTaskState = { compare := IO.ordTaskState✝ }

instance IO.instLTTaskState : LT TaskState

Equations

• IO.instLTTaskState = ltOfOrd

instance IO.instLETaskState : LE TaskState

Equations

• IO.instLETaskState = leOfOrd

instance IO.instMinTaskState : Min TaskState

Equations

• IO.instMinTaskState = minOfLe

instance IO.instMaxTaskState : Max TaskState

Equations

• IO.instMaxTaskState = maxOfLe

def IO.TaskState.toString : TaskState → String

Converts a task state to a string.

Equations

• IO.TaskState.waiting.toString = "waiting"
• IO.TaskState.running.toString = "running"
• IO.TaskState.finished.toString = "finished"

instance IO.instToStringTaskState : ToString TaskState

Equations

• IO.instToStringTaskState = { toString := IO.TaskState.toString }

@[extern lean_io_get_task_state]

opaque IO.getTaskState {α : Type u_1} : Task α → BaseIO TaskState

Returns the current state of a task in the Lean runtime's task manager.

For tasks derived from Promises, the states waiting and running should be considered equivalent.

@[inline]

def IO.hasFinished {α : Type u_1} (task : Task α) : BaseIO Bool

Checks whether the task has finished execution, at which point calling Task.get will return immediately.

Equations

• IO.hasFinished task = do let __do_lift ← IO.getTaskState task pure (match __do_lift with | IO.TaskState.finished => true | x => false)

@[extern lean_io_wait]

opaque IO.wait {α : Type} (t : Task α) : BaseIO α

Waits for the task to finish, then returns its result.

@[extern lean_io_wait_any]

opaque IO.waitAny {α : Type} (tasks : List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α

Waits until any of the tasks in the list has finished, then return its result.

@[extern lean_io_get_num_heartbeats]

opaque IO.getNumHeartbeats : BaseIO Nat

Returns the number of heartbeats that have occurred during the current thread's execution. The heartbeat count is the number of “small” memory allocations performed in a thread.

Heartbeats used to implement timeouts that are more deterministic across different hardware.

@[extern lean_io_set_heartbeats]

opaque IO.setNumHeartbeats (count : Nat) : BaseIO Unit

Sets the heartbeat counter of the current thread to the given amount. This can be used to avoid counting heartbeats of code whose execution time is non-deterministic.

def IO.addHeartbeats (count : Nat) : BaseIO Unit

Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give allocation-avoiding code additional “weight” and is also used to adjust the counter after resuming from a snapshot.

Heartbeats are a means of implementing “deterministic” timeouts. The heartbeat counter is the number of “small” memory allocations performed on the current execution thread.

Equations

• IO.addHeartbeats count = do let n ← IO.getNumHeartbeats IO.setNumHeartbeats (n + count)

inductive IO.FS.Mode : Type

Whether a file should be opened for reading, writing, creation and writing, or appending.

A the operating system level, this translates to the mode of a file handle (i.e., a set of open flags and an fdopen mode).

None of the modes represented by this datatype translate line endings (i.e. O_BINARY on Windows). Furthermore, they are not inherited across process creation (i.e. O_NOINHERIT on Windows and O_CLOEXEC elsewhere).

Operating System Specifics:

• Windows: _open, _fdopen
• Linux: open, fdopen

• read : Mode

  The file should be opened for reading.

  The read/write cursor is positioned at the beginning of the file. It is an error if the file does not exist.

  • open flags: O_RDONLY
  • fdopen mode: r
• write : Mode

  The file should be opened for writing.

  If the file already exists, it is truncated to zero length. Otherwise, a new file is created. The read/write cursor is positioned at the beginning of the file.

  • open flags: O_WRONLY | O_CREAT | O_TRUNC
  • fdopen mode: w
• writeNew : Mode

  A new file should be created for writing.

  It is an error if the file already exists. A new file is created, with the read/write cursor positioned at the start.

  • open flags: O_WRONLY | O_CREAT | O_TRUNC | O_EXCL
  • fdopen mode: w
• readWrite : Mode

  The file should be opened for both reading and writing.

  It is an error if the file does not already exist. The read/write cursor is positioned at the start of the file.

  • open flags: O_RDWR
  • fdopen mode: r+
• append : Mode

  The file should be opened for writing.

  If the file does not already exist, it is created. If the file already exists, it is opened, and the read/write cursor is positioned at the end of the file.

  • open flags: O_WRONLY | O_CREAT | O_APPEND
  • fdopen mode: a

opaque IO.FS.Handle : Type

A reference to an opened file.

File handles wrap the underlying operating system's file descriptors. There is no explicit operation to close a file: when the last reference to a file handle is dropped, the file is closed automatically.

Handles have an associated read/write cursor that determines the where reads and writes occur in the file.

structure IO.FS.Stream : Type

A pure-Lean abstraction of POSIX streams. These streams may represent an underlying POSIX stream or be implemented by Lean code.

Because standard input, standard output, and standard error are all IO.FS.Streams that can be overridden, Lean code may capture and redirect input and output.

• flush : IO Unit

  Flushes the stream's output buffers.

• read : USize → IO ByteArray

  Reads up to the given number of bytes from the stream.

  If the returned array is empty, an end-of-file marker (EOF) has been reached. An EOF does not actually close a stream, so further reads may block and return more data.

• write : ByteArray → IO Unit

  Writes the provided bytes to the stream.

  If the stream represents a physical output device such as a file on disk, then the results may be buffered. Call FS.Stream.flush to synchronize their contents.

• getLine : IO String

  Reads text up to and including the next newline from the stream.

  If the returned string is empty, an end-of-file marker (EOF) has been reached. An EOF does not actually close a stream, so further reads may block and return more data.

• putStr : String → IO Unit

  Writes the provided string to the stream.

• isTty : BaseIO Bool

  Returns true if a stream refers to a Windows console or Unix terminal.

instance IO.FS.instInhabitedStream : Inhabited Stream

Equations

• IO.FS.instInhabitedStream = { default := { flush := default, read := default, write := default, getLine := default, putStr := default, isTty := default } }

@[extern lean_get_stdin]

opaque IO.getStdin : BaseIO FS.Stream

Returns the current thread's standard input stream.

Use IO.setStdin to replace the current thread's standard input stream.

@[extern lean_get_stdout]

opaque IO.getStdout : BaseIO FS.Stream

Returns the current thread's standard output stream.

Use IO.setStdout to replace the current thread's standard output stream.

@[extern lean_get_stderr]

opaque IO.getStderr : BaseIO FS.Stream

Returns the current thread's standard error stream.

Use IO.setStderr to replace the current thread's standard error stream.

@[extern lean_get_set_stdin]

opaque IO.setStdin : FS.Stream → BaseIO FS.Stream

Replaces the standard input stream of the current thread and returns its previous value.

Use IO.getStdin to get the current standard input stream.

@[extern lean_get_set_stdout]

opaque IO.setStdout : FS.Stream → BaseIO FS.Stream

Replaces the standard output stream of the current thread and returns its previous value.

Use IO.getStdout to get the current standard output stream.

@[extern lean_get_set_stderr]

opaque IO.setStderr : FS.Stream → BaseIO FS.Stream

Replaces the standard error stream of the current thread and returns its previous value.

Use IO.getStderr to get the current standard error stream.

@[specialize #[]]

partial def IO.iterate {α β : Type} (a : α) (f : α → IO (α ⊕ β)) : IO β

Iterates an IO action. Starting with an initial state, the action is applied repeatedly until it returns a final value in Sum.inr. Each time it returns Sum.inl, the returned value is treated as a new sate.

@[extern lean_io_prim_handle_mk]

opaque IO.FS.Handle.mk (fn : System.FilePath) (mode : Mode) : IO Handle

Opens the file at fn with the given mode.

An exception is thrown if the file cannot be opened.

@[extern lean_io_prim_handle_lock]

opaque IO.FS.Handle.lock (h : Handle) (exclusive : Bool := true) : IO Unit

Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary.

Acquiring a exclusive lock while already possessing a shared lock will not reliably succeed: it works on Unix-like systems but not on Windows.

@[extern lean_io_prim_handle_try_lock]

opaque IO.FS.Handle.tryLock (h : Handle) (exclusive : Bool := true) : IO Bool

Tries to acquire an exclusive or shared lock on the handle and returns true if successful. Will not block if the lock cannot be acquired, but instead returns false.

Acquiring a exclusive lock while already possessing a shared lock will not reliably succeed: it works on Unix-like systems but not on Windows.

@[extern lean_io_prim_handle_unlock]

opaque IO.FS.Handle.unlock (h : Handle) : IO Unit

Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired.

@[extern lean_io_prim_handle_is_tty]

opaque IO.FS.Handle.isTty (h : Handle) : BaseIO Bool

Returns true if a handle refers to a Windows console or a Unix terminal.

@[extern lean_io_prim_handle_flush]

opaque IO.FS.Handle.flush (h : Handle) : IO Unit

Flushes the output buffer associated with the handle, writing any unwritten data to the associated output device.

@[extern lean_io_prim_handle_rewind]

opaque IO.FS.Handle.rewind (h : Handle) : IO Unit

Rewinds the read/write cursor to the beginning of the handle's file.

@[extern lean_io_prim_handle_truncate]

opaque IO.FS.Handle.truncate (h : Handle) : IO Unit

Truncates the handle to its read/write cursor.

This operation does not automatically flush output buffers, so the contents of the output device may not reflect the change immediately. This does not usually lead to problems because the read/write cursor includes buffered writes. However, buffered writes followed by IO.FS.Handle.rewind, then IO.FS.Handle.truncate, and then closing the file may lead to a non-empty file. If unsure, call IO.FS.Handle.flush before truncating.

@[extern lean_io_prim_handle_read]

opaque IO.FS.Handle.read (h : Handle) (bytes : USize) : IO ByteArray

Reads up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.

@[extern lean_io_prim_handle_write]

opaque IO.FS.Handle.write (h : Handle) (buffer : ByteArray) : IO Unit

Writes the provided bytes to the the handle.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use IO.FS.Handle.flush to write changes to buffers to the associated device.

@[extern lean_io_prim_handle_get_line]

opaque IO.FS.Handle.getLine (h : Handle) : IO String

Reads UTF-8-encoded text up to and including the next line break from the handle. If the returned string is empty, an end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.

@[extern lean_io_prim_handle_put_str]

opaque IO.FS.Handle.putStr (h : Handle) (s : String) : IO Unit

Writes the provided string to the file handle using the UTF-8 encoding.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use IO.FS.Handle.flush to write changes to buffers to the associated device.

@[extern lean_io_realpath]

opaque IO.FS.realPath (fname : System.FilePath) : IO System.FilePath

Resolves a path to an absolute path that contains no '.', '..', or symbolic links.

This function coincides with the POSIX realpath function.

@[extern lean_io_remove_file]

opaque IO.FS.removeFile (fname : System.FilePath) : IO Unit

Removes (deletes) a file from the filesystem.

To remove a directory, use IO.FS.removeDir or IO.FS.removeDirAll instead.

@[extern lean_io_remove_dir]

opaque IO.FS.removeDir : System.FilePath → IO Unit

Removes (deletes) a directory.

Removing a directory fails if the directory is not empty. Use IO.FS.removeDirAll to remove directories along with their contents.

@[extern lean_io_create_dir]

opaque IO.FS.createDir : System.FilePath → IO Unit

Creates a directory at the specified path. The parent directory must already exist.

Throws an exception if the directory cannot be created.

@[extern lean_io_rename]

opaque IO.FS.rename (old new : System.FilePath) : IO Unit

Moves a file or directory old to the new location new.

This function coincides with the POSIX rename function.

@[extern lean_io_create_tempfile]

opaque IO.FS.createTempFile : IO (Handle × System.FilePath)

Creates a temporary file in the most secure manner possible, returning both a Handle to the already-opened file and its path.

There are no race conditions in the file’s creation. The file is readable and writable only by the creating user ID. Additionally on UNIX style platforms the file is executable by nobody.

It is the caller's job to remove the file after use. Use withTempFile to ensure that the temporary file is removed.

@[extern lean_io_create_tempdir]

opaque IO.FS.createTempDir : IO System.FilePath

Creates a temporary directory in the most secure manner possible, returning the new directory's path. There are no race conditions in the directory’s creation. The directory is readable and writable only by the creating user ID.

It is the caller's job to remove the directory after use. Use withTempDir to ensure that the temporary directory is removed.

@[extern lean_io_getenv]

opaque IO.getEnv (var : String) : BaseIO (Option String)

Returns the value of the environment variable var, or none if it is not present in the environment.

@[extern lean_io_app_path]

opaque IO.appPath : IO System.FilePath

Returns the file name of the currently-running executable.

@[extern lean_io_current_dir]

opaque IO.currentDir : IO System.FilePath

Returns the current working directory of the executing process.

@[inline]

def IO.FS.withFile {α : Type} (fn : System.FilePath) (mode : Mode) (f : Handle → IO α) : IO α

Opens the file fn with the specified mode and passes the resulting file handle to f.

The file handle is closed when the last reference to it is dropped. If references escape f, then the file remains open even after IO.FS.withFile has finished.

Equations

• IO.FS.withFile fn mode f = IO.FS.Handle.mk fn mode >>= f

def IO.FS.Handle.putStrLn (h : Handle) (s : String) : IO Unit

Writes the contents of the string to the handle, followed by a newline. Uses UTF-8.

Equations

• h.putStrLn s = h.putStr (s.push '\n')

def IO.FS.Handle.readBinToEndInto (h : Handle) (buf : ByteArray) : IO ByteArray

Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from the handle may block and/or return data.

Equations

• h.readBinToEndInto buf = IO.FS.Handle.readBinToEndInto.loop h buf

partial def IO.FS.Handle.readBinToEndInto.loop (h : Handle) (acc : ByteArray) : IO ByteArray

def IO.FS.Handle.readBinToEnd (h : Handle) : IO ByteArray

Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from the handle may block and/or return data.

Equations

• h.readBinToEnd = h.readBinToEndInto ByteArray.empty

def IO.FS.Handle.readToEnd (h : Handle) : IO String

Reads the entire remaining contents of the file handle as a UTF-8-encoded string. An exception is thrown if the contents are not valid UTF-8.

The underlying file is not automatically closed, and subsequent reads from the handle may block and/or return data.

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.lines (fname : System.FilePath) : IO (Array String)

Returns the contents of a UTF-8-encoded text file as an array of lines.

Newline markers are not included in the lines.

Equations

• IO.FS.lines fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.lines.read h #[]

partial def IO.FS.lines.read (h : Handle) (lines : Array String) : IO (Array String)

def IO.FS.writeBinFile (fname : System.FilePath) (content : ByteArray) : IO Unit

Write the provided bytes to a binary file at the specified path.

Equations

• IO.FS.writeBinFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write h.write content

def IO.FS.writeFile (fname : System.FilePath) (content : String) : IO Unit

Write contents of a string to a file at the specified path using UTF-8 encoding.

Equations

• IO.FS.writeFile fname content = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.write h.putStr content

def IO.FS.Stream.putStrLn (strm : Stream) (s : String) : IO Unit

Writes the contents of the string to the stream, followed by a newline.

Equations

• strm.putStrLn s = strm.putStr (s.push '\n')

structure IO.FS.DirEntry : Type

An entry in a directory on a filesystem.

• root : System.FilePath

  The directory in which the entry is found.

• fileName : String

  The name of the entry.

instance IO.FS.instReprDirEntry : Repr DirEntry

Equations

• IO.FS.instReprDirEntry = { reprPrec := IO.FS.reprDirEntry✝ }

def IO.FS.DirEntry.path (entry : DirEntry) : System.FilePath

The path of the file indicated by the directory entry.

Equations

• entry.path = entry.root / { toString := entry.fileName }

inductive IO.FS.FileType : Type

Types of files that may be found on a filesystem.

• dir : FileType

  Directories don't have contents, but may contain other files.

• file : FileType

  Ordinary files that have contents and are not directories.

• symlink : FileType

  Symbolic links that are pointers to other named files.

• other : FileType

  Files that are neither ordinary files, directories, or symbolic links.

instance IO.FS.instReprFileType : Repr FileType

Equations

• IO.FS.instReprFileType = { reprPrec := IO.FS.reprFileType✝ }

instance IO.FS.instBEqFileType : BEq FileType

Equations

• IO.FS.instBEqFileType = { beq := IO.FS.beqFileType✝ }

structure IO.FS.SystemTime : Type

Low-level system time, tracked in whole seconds and additional nanoseconds.

• sec : Int

  The number of whole seconds.

• nsec : UInt32

  The number of additional nanoseconds.

instance IO.FS.instReprSystemTime : Repr SystemTime

Equations

• IO.FS.instReprSystemTime = { reprPrec := IO.FS.reprSystemTime✝ }

instance IO.FS.instBEqSystemTime : BEq SystemTime

Equations

• IO.FS.instBEqSystemTime = { beq := IO.FS.beqSystemTime✝ }

instance IO.FS.instOrdSystemTime : Ord SystemTime

Equations

• IO.FS.instOrdSystemTime = { compare := IO.FS.ordSystemTime✝ }

instance IO.FS.instInhabitedSystemTime : Inhabited SystemTime

Equations

• IO.FS.instInhabitedSystemTime = { default := { sec := default, nsec := default } }

instance IO.FS.instLTSystemTime : LT SystemTime

Equations

• IO.FS.instLTSystemTime = ltOfOrd

instance IO.FS.instLESystemTime : LE SystemTime

Equations

• IO.FS.instLESystemTime = leOfOrd

structure IO.FS.Metadata : Type

File metadata.

The metadata for a file can be accessed with System.FilePath.metadata.

• accessed : SystemTime

  File access time.

• modified : SystemTime

  File modification time.

• byteSize : UInt64

  The size of the file in bytes.

• type : FileType

  Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file.

instance IO.FS.instReprMetadata : Repr Metadata

Equations

• IO.FS.instReprMetadata = { reprPrec := IO.FS.reprMetadata✝ }

@[extern lean_io_read_dir]

opaque System.FilePath.readDir : FilePath → IO (Array IO.FS.DirEntry)

Returns the contents of the indicated directory. Throws an exception if the file does not exist or is not a directory.

@[extern lean_io_metadata]

opaque System.FilePath.metadata : FilePath → IO IO.FS.Metadata

Returns metadata for the indicated file. Throws an exception if the file does not exist or the metadata cannot be accessed.

def System.FilePath.isDir (p : FilePath) : BaseIO Bool

Checks whether the indicated path can be read and is a directory.

Equations

• p.isDir = do let __do_lift ← EIO.toBaseIO p.metadata match __do_lift with | Except.ok m => pure (m.type == IO.FS.FileType.dir) | Except.error a => pure false

def System.FilePath.pathExists (p : FilePath) : BaseIO Bool

Checks whether the indicated path points to a file that exists.

Equations

• p.pathExists = do let __do_lift ← EIO.toBaseIO p.metadata pure __do_lift.toBool

def System.FilePath.walkDir (p : FilePath) (enter : FilePath → IO Bool := fun (x : FilePath) => pure true) : IO (Array FilePath)

Traverses a filesystem starting at the path p and exploring directories that satisfy enter, returning the paths visited.

The traversal is a preorder traversal, in which parent directories occur prior to any of their children. Symbolic links are followed.

Equations

• p.walkDir enter = Prod.snd <$> (System.FilePath.walkDir.go enter p).run #[]

partial def System.FilePath.walkDir.go (enter : FilePath → IO Bool := fun (x : FilePath) => pure true) (p : FilePath) : StateT (Array FilePath) IO Unit

def IO.FS.readBinFile (fname : System.FilePath) : IO ByteArray

Reads the entire contents of the binary file at the given path as an array of bytes.

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.readFile (fname : System.FilePath) : IO String

Reads the entire contents of the UTF-8-encoded file at the given path as a String.

An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to exceptions that may always be thrown as a result of failing to read files.

Equations

• One or more equations did not get rendered due to their size.

def IO.withStdin {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Runs an action with the specified stream h as standard input, restoring the original standard input stream afterwards.

Equations

• IO.withStdin h x = do let prev ← liftM (IO.setStdin h) tryFinally x (discard (liftM (IO.setStdin prev)))

def IO.withStdout {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Runs an action with the specified stream h as standard output, restoring the original standard output stream afterwards.

Equations

• IO.withStdout h x = do let prev ← liftM (IO.setStdout h) tryFinally x (discard (liftM (IO.setStdout prev)))

def IO.withStderr {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Runs an action with the specified stream h as standard error, restoring the original standard error stream afterwards.

Equations

• IO.withStderr h x = do let prev ← liftM (IO.setStderr h) tryFinally x (discard (liftM (IO.setStderr prev)))

def IO.print {α : Type u_1} [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it to the current standard output (as determined by IO.getStdout).

Equations

• IO.print s = do let out ← liftM IO.getStdout out.putStr (toString s)

def IO.println {α : Type u_1} [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it with a trailing newline to the current standard output (as determined by IO.getStdout).

Equations

• IO.println s = IO.print ((toString s).push '\n')

def IO.eprint {α : Type u_1} [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it to the current standard error (as determined by IO.getStderr).

Equations

• IO.eprint s = do let out ← liftM IO.getStderr out.putStr (toString s)

def IO.eprintln {α : Type u_1} [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it with a trailing newline to the current standard error (as determined by IO.getStderr).

Equations

• IO.eprintln s = IO.eprint ((toString s).push '\n')

def IO.appDir : IO System.FilePath

Returns the directory that the current executable is located in.

Equations

• One or more equations did not get rendered due to their size.

partial def IO.FS.createDirAll (p : System.FilePath) : IO Unit

Creates a directory at the specified path, creating all missing parents as directories.

partial def IO.FS.removeDirAll (p : System.FilePath) : IO Unit

Fully remove given directory by deleting all contained files and directories in an unspecified order. Fails if any contained entry cannot be deleted or was newly created during execution.

def IO.FS.withTempFile {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → System.FilePath → m α) : m α

Creates a temporary file in the most secure manner possible and calls f with both a Handle to the already-opened file and its path. Afterwards, the temporary file is deleted.

There are no race conditions in the file’s creation. The file is readable and writable only by the creating user ID. Additionally on UNIX style platforms the file is executable by nobody.

Use IO.FS.createTempFile to avoid the automatic deletion of the temporary file.

Equations

• IO.FS.withTempFile f = do let __discr ← liftM IO.FS.createTempFile match __discr with | (handle, path) => tryFinally (f handle path) (liftM (IO.FS.removeFile path))

def IO.FS.withTempDir {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : System.FilePath → m α) : m α

Creates a temporary directory in the most secure manner possible, providing a its path to an IO action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how or when they were created.

There are no race conditions in the directory’s creation. The directory is readable and writable only by the creating user ID. Use IO.FS.createTempDir to avoid the automatic deletion of the directory's contents.

Equations

• IO.FS.withTempDir f = do let path ← liftM IO.FS.createTempDir tryFinally (f path) (liftM (IO.FS.removeDirAll path))

@[extern lean_io_process_get_current_dir]

opaque IO.Process.getCurrentDir : IO System.FilePath

Returns the current working directory of the calling process.

@[extern lean_io_process_set_current_dir]

opaque IO.Process.setCurrentDir (path : System.FilePath) : IO Unit

Sets the current working directory of the calling process.

@[extern lean_io_process_get_pid]

opaque IO.Process.getPID : BaseIO UInt32

Returns the process ID of the calling process.

inductive IO.Process.Stdio : Type

Whether the standard input, output, and error handles of a child process should be attached to pipes, inherited from the parent, or null.

If the stream is a pipe, then the parent process can use it to communicate with the child.

• piped : Stdio

  The stream should be attached to a pipe.

• inherit : Stdio

  The stream should be inherited from the parent process.

• null : Stdio

  The stream should be empty.

def IO.Process.Stdio.toHandleType : Stdio → Type

The type of handles that can be used to communicate with a child process on its standard input, output, or error streams.

For IO.Process.Stdio.piped, this type is IO.FS.Handle. Otherwise, it is Unit, because no communication is possible.

Equations

• IO.Process.Stdio.piped.toHandleType = IO.FS.Handle
• IO.Process.Stdio.inherit.toHandleType = Unit
• IO.Process.Stdio.null.toHandleType = Unit

structure IO.Process.StdioConfig : Type

Configuration for the standard input, output, and error handles of a child process.

• stdin : Stdio

  Configuration for the process' stdin handle.

• stdout : Stdio

  Configuration for the process' stdout handle.

• stderr : Stdio

  Configuration for the process' stderr handle.

structure IO.Process.SpawnArgsextends IO.Process.StdioConfig : Type

Configuration for a child process to be spawned.

Use IO.Process.spawn to start the child process. IO.Process.output and IO.Process.run can be used when the child process should be run to completion, with its output and/or error code captured.

• stdin : Stdio
• stdout : Stdio
• stderr : Stdio
• cmd : String

  Command name.

• args : Array String

  Arguments for the command.

• cwd : Option System.FilePath

  The child process's working directory. Inherited from the parent current process if none.

• env : Array (String × Option String)

  Add or remove environment variables for the child process.

  The child process inherits the parent's environment, as modified by env. Keys in the array are the names of environment variables. A none, causes the entry to be removed from the environment, and some sets the variable to the new value, adding it if necessary. Variables are processed from left to right.

• setsid : Bool

  Starts the child process in a new session and process group using setsid. Currently a no-op on non-POSIX platforms.

structure IO.Process.Child (cfg : StdioConfig) : Type

A child process that was spawned with configuration cfg.

The configuration determines whether the child process's standard input, standard output, and standard error are IO.FS.Handles or Unit.

• stdin : cfg.stdin.toHandleType

  The child process's standard input handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

• stdout : cfg.stdout.toHandleType

  The child process's standard output handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

• stderr : cfg.stderr.toHandleType

  The child process's standard error handle, if it was configured as IO.Process.Stdio.piped, or () otherwise.

@[extern lean_io_process_spawn]

opaque IO.Process.spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)

Starts a child process with the provided configuration. The child process is spawned using operating system primitives, and it can be written in any language.

The child process runs in parallel with the parent.

If the child process's standard input is a pipe, use IO.Process.Child.takeStdin to make it possible to close the child's standard input before the process terminates, which provides the child with an end-of-file marker.

@[extern lean_io_process_child_wait]

opaque IO.Process.Child.wait {cfg : StdioConfig} : Child cfg → IO UInt32

Blocks until the child process has exited and return its exit code.

@[extern lean_io_process_child_try_wait]

opaque IO.Process.Child.tryWait {cfg : StdioConfig} : Child cfg → IO (Option UInt32)

Checks whether the child has exited. Returns none if the process has not exited, or its exit code if it has.

@[extern lean_io_process_child_kill]

opaque IO.Process.Child.kill {cfg : StdioConfig} : Child cfg → IO Unit

Terminates the child process using the SIGTERM signal or a platform analogue.

If the process was started using SpawnArgs.setsid, terminates the entire process group instead.

@[extern lean_io_process_child_take_stdin]

opaque IO.Process.Child.takeStdin {cfg : StdioConfig} : Child cfg → IO (cfg.stdin.toHandleType × Child { stdin := Stdio.null, stdout := cfg.stdout, stderr := cfg.stderr })

Extracts the stdin field from a Child object, allowing the handle to be closed while maintaining a reference to the child process.

File handles are closed when the last reference to them is dropped. Closing the child's standard input causes an end-of-file marker. Because the Child object has a reference to the standard input, this operation is necessary in order to close the stream while the process is running (e.g. to extract its exit code after calling Child.wait). Many processes do not terminate until their standard input is exhausted.

structure IO.Process.Output : Type

The result of running a process to completion.

• exitCode : UInt32

  The process's exit code.

• stdout : String

  Everything that was written to the process's standard output.

• stderr : String

  Everything that was written to the process's standard error.

def IO.Process.output (args : SpawnArgs) : IO Output

Runs a process to completion and captures its output and exit code. The child process is run with a null standard input, and the current process blocks until it has run to completion.

The specifications of standard input, output, and error handles in args are ignored.

Equations

• One or more equations did not get rendered due to their size.

def IO.Process.run (args : SpawnArgs) : IO String

Runs a process to completion, blocking until it terminates. If the child process terminates successfully with exit code 0, its standard output is returned. An exception is thrown if it terminates with any other exit code.

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_io_exit]

opaque IO.Process.exit {α : Type} : UInt8 → IO α

Terminates the current process with the provided exit code. 0 indicates success, all other values indicate failure.

@[extern lean_io_get_tid]

opaque IO.getTID : BaseIO UInt64

Returns the thread ID of the calling thread.

structure IO.AccessRight : Type

POSIX-style file permissions.

The FileRight structure describes these permissions for a file's owner, members of it's designated group, and all others.

• read : Bool

  The file can be read.

• write : Bool

  The file can be written to.

• execution : Bool

  The file can be executed.

def IO.AccessRight.flags (acc : AccessRight) : UInt32

Converts individual POSIX-style file permissions to their conventional three-bit representation.

This is the bitwise or of the following:

• If the file can be read, 0x4, otherwise 0.
• If the file can be written, 0x2, otherwise 0.
• If the file can be executed, 0x1, otherwise 0.

Examples:

• {read := true : AccessRight}.flags = 4
• {read := true, write := true : AccessRight}.flags = 6
• {read := true, execution := true : AccessRight}.flags = 5

Equations

• acc.flags = (if acc.read = true then 4 else 0).lor ((if acc.write = true then 2 else 0).lor (if acc.execution = true then 1 else 0))

structure IO.FileRight : Type

POSIX-style file permissions that describe access rights for a file's owner, members of its assigned group, and all others.

• user : AccessRight

  The owner's permissions to access the file.

• group : AccessRight

  The assigned group's permissions to access the file.

• other : AccessRight

  The permissions that all others have to access the file.

def IO.FileRight.flags (acc : FileRight) : UInt32

Converts POSIX-style file permissions to their numeric representation, with three bits each for the owner's permissions, the group's permissions, and others' permissions.

Equations

• acc.flags = (acc.user.flags.shiftLeft 6).lor ((acc.group.flags.shiftLeft 3).lor acc.other.flags)

@[extern lean_chmod]

opaque IO.Prim.setAccessRights (filename : System.FilePath) (mode : UInt32) : IO Unit

def IO.setAccessRights (filename : System.FilePath) (mode : FileRight) : IO Unit

Sets the POSIX-style permissions for a file.

Equations

• IO.setAccessRights filename mode = IO.Prim.setAccessRights filename mode.flags

@[reducible, inline]

abbrev IO.Ref (α : Type) : Type

Mutable reference cells that contain values of type α. These cells can read from and mutated in the IO monad.

Equations

• IO.Ref α = ST.Ref IO.RealWorld α

instance IO.instMonadLiftSTRealWorldBaseIO : MonadLift (ST RealWorld) BaseIO

Equations

• IO.instMonadLiftSTRealWorldBaseIO = { monadLift := fun {α : Type} => id }

def IO.mkRef {α : Type} (a : α) : BaseIO (Ref α)

Creates a new mutable reference cell that contains a.

Equations

• IO.mkRef a = ST.mkRef a

structure IO.CancelToken : Type

Mutable cell that can be passed around for purposes of cooperative task cancellation: request cancellation with CancelToken.set and check for it with CancelToken.isSet.

This is a more flexible alternative to Task.cancel as the token can be shared between multiple tasks.

• ref : IO.Ref Bool

instance IO.instNonemptyCancelToken : Nonempty CancelToken

def IO.CancelToken.new : BaseIO CancelToken

Creates a new cancellation token.

Equations

• IO.CancelToken.new = IO.CancelToken.mk <$> IO.mkRef false

def IO.CancelToken.set (tk : CancelToken) : BaseIO Unit

Activates a cancellation token. Idempotent.

Equations

• tk.set = ST.Ref.set (IO.CancelToken.ref✝ tk) true

def IO.CancelToken.isSet (tk : CancelToken) : BaseIO Bool

Checks whether the cancellation token has been activated.

Equations

• tk.isSet = ST.Ref.get (IO.CancelToken.ref✝ tk)

@[export lean_stream_of_handle]

def IO.FS.Stream.ofHandle (h : Handle) : Stream

Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding file handle operation.

Equations

• IO.FS.Stream.ofHandle h = { flush := h.flush, read := h.read, write := h.write, getLine := h.getLine, putStr := h.putStr, isTty := h.isTty }

structure IO.FS.Stream.Buffer : Type

A byte buffer that can simulate a file in memory.

Use IO.FS.Stream.ofBuffer to create a stream from a buffer.

• data : ByteArray

  The contents of the buffer.

• pos : Nat

  The read/write cursor's position in the buffer.

def IO.FS.Stream.ofBuffer (r : Ref Buffer) : Stream

Creates a stream from a mutable reference to a buffer.

The resulting stream simulates a file, mutating the contents of the reference in response to writes and reading from it in response to reads. These streams can be used with IO.withStdin, IO.setStdin, and the corresponding operators for standard output and standard error to redirect input and output.

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.withIsolatedStreams {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α) (isolateStderr : Bool := true) : m (String × α)

Runs an action with stdin emptied and stdout and stderr captured into a String. If isolateStderr is false, only stdout is captured.

Equations

• One or more equations did not get rendered due to their size.

def termPrintln!__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_runtime_mark_multi_threaded]

def Runtime.markMultiThreaded {α : Type} (a : α) : BaseIO α

Marks given value and its object graph closure as multi-threaded if currently marked single-threaded. This will make reference counter updates atomic and thus more costly. It can still be useful to do eagerly when the value will be shared between threads later anyway and there is available time budget to mark it now.

Equations

• Runtime.markMultiThreaded a = pure a

@[extern lean_runtime_mark_persistent]

unsafe def Runtime.markPersistent {α : Type} (a : α) : BaseIO α

Marks given value and its object graph closure as persistent. This will remove reference counter updates but prevent the closure from being deallocated until the end of the process! It can still be useful to do eagerly when the value will be marked persistent later anyway and there is available time budget to mark it now or it would be unnecessarily marked multi-threaded in between.

This function is only safe to use on objects (in the full closure) which are not used concurrently or which are already persistent.

Equations

• Runtime.markPersistent a = pure a

@[extern lean_runtime_forget]

def Runtime.forget {α : Sort u_1} (a : α) : BaseIO Unit

Discards the passed owned reference. This leads to a any any object reachable from it never being freed. This can be a useful optimization for eliding deallocation time of big object graphs that are kept alive close to the end of the process anyway (in which case calling Runtime.markPersistent would be similarly costly to deallocation). It is still considered a safe operation as it cannot lead to undefined behavior.

Equations

• Runtime.forget a = pure PUnit.unit