Init.System.IO

IO.RealWorld definition

: Type

Full source

/--
A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
reordered.
-/
/- Like <https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld>.
   Makes sure we never reorder `IO` operations.

   TODO: mark opaque -/
def IO.RealWorld : Type := Unit

Real world token for IO monad sequencing

Informal description

The type `IO.RealWorld` represents a token used in the `IO` monad to ensure that input/output actions are executed in the correct order. It is implemented as the unit type, which has exactly one element.

EIO definition

(ε : Type) : Type → Type

Full source

/--
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`.
-/
/- TODO(Leo): mark it as an opaque definition. Reason: prevent
   functions defined in other modules from accessing `IO.RealWorld`.
   We don't want action such as
   ```
   def getWorld : IO (IO.RealWorld) := get
   ```
-/
def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld

IO monad with exceptions

Informal description

The monad `EIO ε α` represents a computation that can perform input/output operations and may throw exceptions of type `ε`, producing a result of type `α`. It is implemented as a stateful computation monad with exceptions (`EStateM`) where the state is a token (`IO.RealWorld`) used to sequence IO operations.

instMonadEIO instance

: Monad (EIO ε)

Full source

instance : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))

Monad Instance for Exception-Handling IO Monad

Informal description

The exception-handling IO monad `EIO ε` is a monad, meaning it supports the standard monadic operations `pure` and `bind` for sequencing computations with exceptions and input/output effects.

instMonadFinallyEIO instance

: MonadFinally (EIO ε)

Full source

instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))

`MonadFinally` Instance for Exception-Handling IO Monad

Informal description

The exception-handling IO monad `EIO ε` is equipped with a `MonadFinally` instance, allowing it to perform cleanup operations (like resource deallocation) regardless of whether the computation succeeds or fails with an exception of type `ε`.

instMonadExceptOfEIO instance

: MonadExceptOf ε (EIO ε)

Full source

instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))

Exception Handling in the EIO Monad

Informal description

The exception-handling IO monad `EIO ε` is equipped with a `MonadExceptOf ε` instance, meaning it can throw and catch exceptions of type `ε` while performing input/output operations.

instOrElseEIO instance

: OrElse (EIO ε α)

Full source

instance : OrElse (EIO ε α) := ⟨MonadExcept.orElse⟩

"Or Else" Operation for Exception-Handling IO Monad

Informal description

The exception-handling IO monad `EIO ε α` is equipped with an "or else" operation, which allows sequencing computations with a fallback option in case of exceptions.

instInhabitedEIO instance

[Inhabited ε] : Inhabited (EIO ε α)

Full source

instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))

Inhabited IO Monad with Exceptions

Informal description

For any types $\varepsilon$ and $\alpha$, if $\varepsilon$ is inhabited (has a default element), then the monad `EIO ε α` of input/output computations with exceptions is also inhabited.

BaseIO definition

Full source

/--
An `IO` monad that cannot throw exceptions.
-/
def BaseIO := EIO Empty

Exception-free IO monad

Informal description

The monad `BaseIO α` represents a computation that can perform input/output operations and cannot throw exceptions, producing a result of type `α`. It is implemented as a variant of the `EIO` monad where the exception type is `Empty`, meaning no exceptions can occur.

instMonadBaseIO instance

: Monad BaseIO

Full source

instance : Monad BaseIO := inferInstanceAs (Monad (EIO Empty))

Monad Instance for Exception-Free IO Monad

Informal description

The exception-free IO monad `BaseIO` is a monad, meaning it supports the standard monadic operations `pure` and `bind` for sequencing computations with input/output effects.

instMonadFinallyBaseIO instance

: MonadFinally BaseIO

Full source

instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (EIO Empty))

`MonadFinally` Instance for Exception-Free IO Monad

Informal description

The exception-free IO monad `BaseIO` is equipped with a `MonadFinally` instance, allowing it to perform cleanup operations (like resource deallocation) regardless of whether the computation succeeds or fails.

BaseIO.toEIO definition

(act : BaseIO α) : EIO ε α

Full source

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

This function is usually used implicitly via [automatic monadic
lifting](lean-manual://section/lifting-monads) rather being than called explicitly.
-/
@[always_inline, inline]
def BaseIO.toEIO (act : BaseIO α) : EIO ε α :=
  fun s => match act s with
  | EStateM.Result.okEStateM.Result.ok a s => EStateM.Result.ok a s

Lifting of exception-free IO to exception-capable IO

Informal description

The function lifts a `BaseIO` action (which cannot throw exceptions) to an `EIO` monad (which can throw exceptions of any type). Given a `BaseIO` computation `act`, it produces an `EIO` computation that behaves identically to `act` but in the context of an exception-capable monad. The implementation preserves the successful results and state transitions of the original computation.

instMonadLiftBaseIOEIO instance

: MonadLift BaseIO (EIO ε)

Full source

instance : MonadLift BaseIO (EIO ε) := ⟨BaseIO.toEIO⟩

Lifting BaseIO to EIO

Informal description

Every exception-free IO computation in `BaseIO` can be lifted to an exception-capable IO computation in `EIO ε` for any exception type `ε$.

EIO.toBaseIO definition

(act : EIO ε α) : BaseIO (Except ε α)

Full source

/--
Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `BaseIO`
action that returns an `Except` value.
-/
@[always_inline, inline]
def EIO.toBaseIO (act : EIO ε α) : BaseIO (Except ε α) :=
  fun s => match act s with
  | EStateM.Result.okEStateM.Result.ok a s     => EStateM.Result.ok (Except.ok a) s
  | EStateM.Result.errorEStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s

Conversion from exception-throwing IO to exception-free IO with Except result

Informal description

The function converts an `EIO ε α` computation (which may throw exceptions of type `ε`) into a `BaseIO (Except ε α)` computation (which is exception-free and returns an `Except` value representing either a successful result of type `α` or an error of type `ε`). Specifically: - If the `EIO` computation succeeds with result `a` and state `s`, it returns `Except.ok a` with state `s`. - If the `EIO` computation fails with exception `ex` and state `s`, it returns `Except.error ex` with state `s`.

EIO.catchExceptions definition

(act : EIO ε α) (h : ε → BaseIO α) : BaseIO α

Full source

/--
Handles any exception that might be thrown by an `EIO ε` action, transforming it into an
exception-free `BaseIO` action.
-/
@[always_inline, inline]
def EIO.catchExceptions (act : EIO ε α) (h : ε → BaseIO α) : BaseIO α :=
  fun s => match act s with
  | EStateM.Result.okEStateM.Result.ok a s     => EStateM.Result.ok a s
  | EStateM.Result.errorEStateM.Result.error ex s => h ex s

Exception handler for `EIO` computations

Informal description

Given an `EIO ε α` computation `act` that may throw an exception of type `ε`, and a handler function `h` that converts any exception into a `BaseIO α` computation, `EIO.catchExceptions` produces a `BaseIO α` computation that either returns the result of `act` if it succeeds, or applies `h` to the exception if one is thrown.

EIO.ofExcept definition

(e : Except ε α) : EIO ε α

Full source

/--
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.
-/
def EIO.ofExcept (e : Except ε α) : EIO ε α :=
  match e with
  | Except.ok a    => pure a
  | Except.error e => throw e

Lifting `Except` to `EIO`

Informal description

Given an `Except ε α` value `e`, the function `EIO.ofExcept` converts it into an `EIO ε α` computation as follows: - If `e` is `Except.ok a`, it returns the pure computation `pure a`. - If `e` is `Except.error e`, it throws the exception `e`. This function lifts an `Except` value into the `EIO` monad, preserving any exceptions.

IO abbrev

: Type → Type

Full source

/--
A monad that supports arbitrary side effects and throwing exceptions of type `IO.Error`.
-/
abbrev IO : Type → Type := EIO Error

Input/Output Monad with Exception Handling

Informal description

The `IO` monad represents computations that can perform arbitrary input/output operations and may throw exceptions of type `IO.Error`. It is defined as an abbreviation for `EIO IO.Error`, which is a monad combining stateful computations (with `IO.RealWorld` as the state token) and exception handling.

BaseIO.toIO definition

(act : BaseIO α) : IO α

Full source

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

This function is usually used implicitly via [automatic monadic
lifting](lean-manual://section/lifting-monads) rather than being called explicitly.
-/
@[inline] def BaseIO.toIO (act : BaseIO α) : IO α :=
  act

Conversion from exception-free IO to standard IO

Informal description

The function converts a computation `act` in the exception-free IO monad `BaseIO α` into a computation in the standard IO monad `IO α`. Since `BaseIO` computations cannot throw exceptions, this conversion is straightforward and preserves the behavior of the original computation.

EIO.toIO definition

(f : ε → IO.Error) (act : EIO ε α) : IO α

Full source

/--
Converts an `EIO ε` action into an `IO` action by translating any exceptions that it throws into
`IO.Error`s using `f`.
-/
@[inline] def EIO.toIO (f : ε → IO.Error) (act : EIO ε α) : IO α :=
  act.adaptExcept f

Conversion from `EIO` to `IO` with exception translation

Informal description

Given a function $f : \varepsilon \to \text{IO.Error}$ and an action `act` in the `EIO \varepsilon` monad, the function `EIO.toIO` converts `act` into an `IO` action by translating any exceptions of type $\varepsilon$ thrown by `act` into `IO.Error` exceptions using $f$.

EIO.toIO' definition

(act : EIO ε α) : IO (Except ε α)

Full source

/--
Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `IO`
action that returns an `Except` value.
-/
@[inline] def EIO.toIO' (act : EIO ε α) : IO (Except ε α) :=
  act.toBaseIO

Conversion from exception-throwing IO to IO with Except result

Informal description

The function converts an `EIO ε α` computation (which may throw exceptions of type `ε`) into an `IO (Except ε α)` computation (which handles IO operations and returns either a successful result of type `α` or an error of type `ε`). Specifically: - If the `EIO` computation succeeds with result `a`, it returns `Except.ok a`. - If the `EIO` computation fails with exception `ex`, it returns `Except.error ex`.

IO.toEIO definition

(f : IO.Error → ε) (act : IO α) : EIO ε α

Full source

/--
Runs an `IO` action in some other `EIO` monad, using `f` to translate `IO` exceptions.
-/
@[inline] def IO.toEIO (f : IO.Error → ε) (act : IO α) : EIO ε α :=
  act.adaptExcept f

Conversion from IO to EIO with exception transformation

Informal description

Given a function $f : \text{IO.Error} \to \varepsilon$ and an input/output action $\text{act} : \text{IO} \alpha$, the function $\text{IO.toEIO}$ converts $\text{act}$ into an $\text{EIO} \varepsilon \alpha$ computation by transforming any $\text{IO.Error}$ exceptions using $f$.

unsafeBaseIO definition

(fn : BaseIO α) : α

Full source

/--
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](lean-manual://section/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.
-/
@[inline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
  match fn.run () with
  | EStateM.Result.okEStateM.Result.ok a _ => a

Unsafe execution of BaseIO computation

Informal description

The function `unsafeBaseIO` executes a `BaseIO α` computation in a pure context, returning a value of type `α`. This is an unsafe operation that bypasses the usual IO monad sequencing and should be used with extreme caution, as it can violate purity assumptions and lead to unpredictable behavior. The computation is run with an initial state of `()` (the unit value), and if successful, returns the result `a` while discarding the final state.

unsafeEIO definition

(fn : EIO ε α) : Except ε α

Full source

/--
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](lean-manual://section/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.
-/
@[inline] unsafe def unsafeEIO (fn : EIO ε α) : Except ε α :=
  unsafeBaseIO fn.toBaseIO

Unsafe execution of exception-throwing IO computation

Informal description

The function `unsafeEIO` executes an `EIO ε α` computation in a pure context, returning an `Except ε α` result. This is a dangerous operation that bypasses the usual IO monad sequencing and should be used with extreme caution, as it can violate purity assumptions and lead to unpredictable behavior. The computation is run by first converting it to a `BaseIO (Except ε α)` computation using `EIO.toBaseIO`, then executing it unsafely with `unsafeBaseIO`.

unsafeIO definition

(fn : IO α) : Except IO.Error α

Full source

@[inline, inherit_doc EIO] unsafe def unsafeIO (fn : IO α) : Except IO.Error α :=
  unsafeEIO fn

Unsafe execution of IO computation with error handling

Informal description

The function `unsafeIO` executes an `IO α` computation in a pure context, returning an `Except IO.Error α` result. This is an unsafe operation that bypasses the usual IO monad sequencing and should be used with caution, as it can violate purity assumptions. The computation may either succeed with a value of type `α` or fail with an `IO.Error` exception.

timeit opaque

(msg : @& String) (fn : IO α) : IO α

Full source

/--
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_timeit"] opaque timeit (msg : @& String) (fn : IO α) : IO α

Execution Timer for IO Actions

Informal description

The function `timeit` takes a message string `msg` and an input/output action `fn` of type `IO α`, and returns an `IO α` action that executes `fn` while printing the message `msg` and the time taken to the standard error output.

allocprof opaque

(msg : @& String) (fn : IO α) : IO α

Full source

@[extern "lean_io_allocprof"] opaque allocprof (msg : @& String) (fn : IO α) : IO α

Memory Allocation Profiling for IO Computations

Informal description

The function `allocprof` takes a string message `msg` and an input/output computation `fn` of type `IO α`, and returns a new input/output computation of type `IO α` that profiles memory allocation during the execution of `fn`.

IO.initializing opaque

: BaseIO Bool

Full source

/--
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_initializing"] opaque IO.initializing : BaseIO Bool

Check for Initialization Phase in BaseIO Monad

Informal description

The function `IO.initializing` returns a Boolean value `true` if and only if it is called during the initialization phase of the program (before the `main` function is executed). This function operates within the `BaseIO` monad, which represents exception-free input/output operations.

IO.ofExcept definition

[ToString ε] (e : Except ε α) : IO α

Full source

/--
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.
-/
def ofExcept [ToString ε] (e : Except ε α) : IO α :=
  match e with
  | Except.ok a    => pure a
  | Except.error e => throw (IO.userError (toString e))

Conversion from Except to IO with error handling

Informal description

Given a computation `e` of type `Except ε α` (which may either succeed with a value of type `α` or fail with an error of type `ε`), and a way to convert errors of type `ε` to strings (`ToString ε`), this function converts `e` into an `IO` computation. If `e` succeeds, the resulting `IO` computation returns the value. If `e` fails, the error is converted to a string and thrown as an `IO.Error`.

IO.lazyPure definition

(fn : Unit → α) : IO α

Full source

/--
Creates an IO action that will invoke `fn` if and when it is executed, returning the result.
-/
def lazyPure (fn : Unit → α) : IO α :=
  pure (fn ())

Lazy pure IO action from unit function

Informal description

The function `IO.lazyPure` takes a function `fn` from the unit type to a type `α` and returns an IO action that, when executed, will invoke `fn` with the unit value `()` and return the result.

IO.monoMsNow opaque

: BaseIO Nat

Full source

/--
Monotonically increasing time since an unspecified past point in milliseconds. There is no relation
to wall clock time.
-/
@[extern "lean_io_mono_ms_now"] opaque monoMsNow : BaseIO Nat

Monotonic Milliseconds Timer

Informal description

The function `IO.monoMsNow` returns the monotonically increasing time in milliseconds since an unspecified past point, as a natural number. This time measurement is unrelated to wall clock time.

IO.monoNanosNow opaque

: BaseIO Nat

Full source

/--
Monotonically increasing time since an unspecified past point in nanoseconds. There is no relation
to wall clock time.
-/
@[extern "lean_io_mono_nanos_now"] opaque monoNanosNow : BaseIO Nat

Monotonic Nanosecond Timer in BaseIO

Informal description

The function `IO.monoNanosNow` returns a monotonically increasing count of nanoseconds elapsed since an unspecified past point in time, as a computation in the `BaseIO` monad producing a natural number. This count is unrelated to wall clock time.

IO.getRandomBytes opaque

(nBytes : USize) : IO ByteArray

Full source

/--
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.
-/
@[extern "lean_io_get_random_bytes"] opaque getRandomBytes (nBytes : USize) : IO ByteArray

Read Bytes from System Entropy Source

Informal description

The function `IO.getRandomBytes` reads `nBytes` bytes from a system entropy source and returns them as a `ByteArray` in the `IO` monad. If `nBytes` is `0`, it returns an empty buffer immediately. Note that this function is not guaranteed to be cryptographically secure.

IO.sleep definition

(ms : UInt32) : BaseIO Unit

Full source

/--
Pauses execution for the specified number of milliseconds.
-/
def sleep (ms : UInt32) : BaseIO Unit :=
  -- TODO: add a proper primitive for IO.sleep
  fun s => dbgSleep ms fun _ => EStateM.Result.ok () s

Sleep function for pausing execution

Informal description

The function `IO.sleep` takes a time duration `ms` in milliseconds and returns a computation in the `BaseIO` monad that pauses execution for the specified duration before returning the unit value `()`.

IO.checkCanceled opaque

: BaseIO Bool

Full source

/--
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_check_canceled"] opaque checkCanceled : BaseIO Bool

Check Task Cancellation Status

Informal description

The function `IO.checkCanceled` checks whether the current task's cancellation flag has been set, either by calling `IO.cancel` or by dropping the last reference to the task. It returns a Boolean value indicating the cancellation status.

IO.cancel opaque

: @& Task α → BaseIO Unit

Full source

/--
Requests cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to
react to the cancellation.
-/
@[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit

Task Cancellation Request Function

Informal description

The function `IO.cancel` sends a cancellation request to a given task of type `Task α`. The task must explicitly check for cancellation by calling `IO.checkCanceled` to respond to the request. The function returns a computation in the `BaseIO` monad that produces no meaningful result (i.e., `Unit`).

IO.TaskState inductive

Full source

/-- The current state of a `Task` in the Lean runtime's task manager. -/
inductive 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.
  -/
  | waiting
  /--
  The `Task` is actively running on a thread or, in the case of a `Promise`, waiting for a call to
  `IO.Promise.resolve`.
  -/
  | running
  /--
  The `Task` has finished running and its result is available. Calling `Task.get` or `IO.wait` on
  the task will not block.
  -/
  | finished
  deriving Inhabited, Repr, DecidableEq, Ord

Task State

Informal description

The inductive type representing the possible states of a `Task` in the Lean runtime's task manager. This describes the various stages a task can be in during its execution lifecycle.

IO.instInhabitedTaskState instance

: Inhabited✝ (@IO.TaskState)

Full source

Inhabited, Repr, DecidableEq, Ord

Inhabitedness of Task States

Informal description

The type `IO.TaskState` is inhabited, meaning it has a designated default element.

IO.instReprTaskState instance

: Repr✝ (@IO.TaskState✝)

Full source

Repr, DecidableEq, Ord

String Representation for Task States

Informal description

The type `IO.TaskState` has a representation function that allows its values to be displayed as strings.

IO.instDecidableEqTaskState instance

: DecidableEq✝ IO.TaskState

Full source

DecidableEq, Ord

Decidable Equality for Task States

Informal description

The inductive type `IO.TaskState`, representing the possible states of a task in the Lean runtime's task manager, has decidable equality. That is, for any two task states $s_1$ and $s_2$, it is constructively decidable whether $s_1 = s_2$ holds.

IO.instOrdTaskState instance

: Ord✝ (@IO.TaskState✝)

Full source

Ord

Linear Order on Task States

Informal description

The inductive type `IO.TaskState` representing the possible states of a task in the Lean runtime's task manager is equipped with a canonical linear order structure.

IO.instLTTaskState instance

: LT TaskState

Full source

instance : LT TaskState := ltOfOrd

The "Less Than" Relation on Task States

Informal description

The inductive type `IO.TaskState` representing the possible states of a task in the Lean runtime's task manager is equipped with a canonical "less than" relation.

IO.instLETaskState instance

: LE TaskState

Full source

instance : LE TaskState := leOfOrd

The "Less Than or Equal To" Relation on Task States

Informal description

The inductive type `IO.TaskState` representing the possible states of a task in the Lean runtime's task manager is equipped with a canonical "less than or equal to" relation.

IO.instMinTaskState instance

: Min TaskState

Full source

instance : Min TaskState := minOfLe

Minimum Operation on Task States

Informal description

The inductive type `IO.TaskState` representing the possible states of a task in the Lean runtime's task manager is equipped with a canonical minimum operation.

IO.instMaxTaskState instance

: Max TaskState

Full source

instance : Max TaskState := maxOfLe

Maximum Operation on Task States

Informal description

The inductive type `IO.TaskState` representing the possible states of a task in the Lean runtime's task manager is equipped with a canonical maximum operation, where for any two task states $x$ and $y$, $\max(x, y)$ returns $y$ if $x \leq y$ and $x$ otherwise.

IO.TaskState.toString definition

: TaskState → String

Full source

/--
Converts a task state to a string.
-/
protected def TaskState.toString : TaskState → String
  | .waiting => "waiting"
  | .running => "running"
  | .finished => "finished"

String representation of task state

Informal description

The function converts a task state into a string representation, where: - "waiting" corresponds to a task that is waiting to be executed, - "running" corresponds to a task that is currently being executed, - "finished" corresponds to a task that has completed execution.

IO.instToStringTaskState instance

: ToString TaskState

Full source

instance : ToString TaskState := ⟨TaskState.toString⟩

String Representation of Task States

Informal description

The task state type `TaskState` has a canonical string representation.

IO.getTaskState opaque

: @& Task α → BaseIO TaskState

Full source

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

For tasks derived from `Promise`s, the states `waiting` and `running` should be considered
equivalent.
-/
@[extern "lean_io_get_task_state"] opaque getTaskState : @& Task α → BaseIO TaskState

Retrieve Task State in BaseIO Monad

Informal description

Given a task `t` of type `Task α`, the function `IO.getTaskState` returns the current state of `t` as a value of type `TaskState` in the `BaseIO` monad.

IO.hasFinished definition

(task : Task α) : BaseIO Bool

Full source

/--
Checks whether the task has finished execution, at which point calling `Task.get` will return
immediately.
-/
@[inline] def hasFinished (task : Task α) : BaseIO Bool := do
  return (← getTaskState task) matches .finished

Task completion check

Informal description

Given a task `task` of type `Task α`, the function `IO.hasFinished` checks whether the task has completed execution, returning `true` if it has finished and `false` otherwise, as a boolean value in the `BaseIO` monad.

IO.wait opaque

(t : Task α) : BaseIO α

Full source

/--
Waits for the task to finish, then returns its result.
-/
@[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
  return t.get

Wait for Task Completion in BaseIO Monad

Informal description

Given a task `t` of type `Task α`, the function `IO.wait` blocks until the task completes and returns its result of type `α` in the `BaseIO` monad.

IO.getNumHeartbeats opaque

: BaseIO Nat

Full source

/--
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_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat

Get Current Thread's Heartbeat Count

Informal description

The function `IO.getNumHeartbeats` returns the number of heartbeats (small memory allocations) that have occurred during the current thread's execution, as a natural number in the `BaseIO` monad.

IO.setNumHeartbeats opaque

(count : Nat) : BaseIO Unit

Full source

/--
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.
-/
@[extern "lean_io_set_heartbeats"] opaque setNumHeartbeats (count : Nat) : BaseIO Unit

Setting the Thread Heartbeat Counter in BaseIO

Informal description

The function `IO.setNumHeartbeats` sets the heartbeat counter of the current thread to the given natural number `count`. This operation is performed within the `BaseIO` monad and returns the unit value `()`, indicating that the operation is performed for its side effect rather than producing a meaningful result.

IO.addHeartbeats definition

(count : Nat) : BaseIO Unit

Full source

/--
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.
-/
def addHeartbeats (count : Nat) : BaseIO Unit := do
  let n ← getNumHeartbeats
  setNumHeartbeats (n + count)

Adjust thread heartbeat counter

Informal description

The function `IO.addHeartbeats` adjusts the heartbeat counter of the current thread by adding the given natural number `count` to the current count. Heartbeats are used to track small memory allocations and implement deterministic timeouts. The operation is performed within the `BaseIO` monad and returns the unit value `()`, indicating it is executed for its side effect.

IO.FS.Mode inductive

Full source

/--
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`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/open-wopen?view=msvc-170),
  [`_fdopen`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fdopen-wfdopen?view=msvc-170)
* Linux: [`open`](https://linux.die.net/man/2/open), [`fdopen`](https://linux.die.net/man/3/fdopen)
-/
inductive FS.Mode where
  /--
  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`
  -/
  | read
  /--
  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`
  -/
  | write
  /--
  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`
  -/
  | writeNew
  /--
  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+`
  -/
  | readWrite
  /--
  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`
  -/
  | append

File Opening Modes

Informal description

An inductive type representing the different modes in which a file can be opened: for reading, writing, creation and writing, or appending. At the operating system level, these modes correspond to specific flags and modes for file handles. Note that these modes do not translate line endings (e.g., `O_BINARY` on Windows) and are not inherited across process creation (e.g., `O_NOINHERIT` on Windows and `O_CLOEXEC` elsewhere).

IO.FS.Handle opaque

: Type

Full source

/--
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.
-/
opaque FS.Handle : Type := Unit

File Handle Type in Input/Output Operations

Informal description

A file handle is a reference to an opened file, representing the underlying operating system's file descriptor. It manages the read/write cursor position within the file and automatically closes the file when the last reference to the handle is dropped.

IO.FS.Stream structure

Full source

/--
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.Stream`s that can be
overridden, Lean code may capture and redirect input and output.
-/
structure FS.Stream where
  /--
  Flushes the stream's output buffers.
  -/
  flush   : IO Unit
  /--
  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.
  -/
  read    : USize → IO ByteArray
  /--
  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.
  -/
  write   : ByteArray → IO Unit
  /--
  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.
  -/
  getLine : IO String
  /--
  Writes the provided string to the stream.
  -/
  putStr  : String → IO Unit
  /-- Returns `true` if a stream refers to a Windows console or Unix terminal. -/
  isTty   : BaseIO Bool
  deriving Inhabited

POSIX Stream Abstraction

Informal description

A structure representing an abstraction of POSIX streams in Lean. These streams can either correspond to actual POSIX streams (like standard input/output) or be implemented purely within Lean. This abstraction allows Lean code to capture and redirect standard input, output, and error streams.

IO.FS.instInhabitedStream instance

: Inhabited✝ (@IO.FS.Stream)

Full source

Inhabited

Inhabited POSIX Stream Type

Informal description

The type `IO.FS.Stream` representing POSIX stream abstractions is inhabited, meaning it has a default element.

IO.getStdin opaque

: BaseIO FS.Stream

Full source

/--
Returns the current thread's standard input stream.

Use `IO.setStdin` to replace the current thread's standard input stream.
-/
@[extern "lean_get_stdin"] opaque getStdin  : BaseIO FS.Stream

Standard Input Stream Accessor

Informal description

The function `IO.getStdin` retrieves the standard input stream associated with the current thread in the Lean programming language. This stream can be used to read input data.

IO.getStdout opaque

: BaseIO FS.Stream

Full source

/--
Returns the current thread's standard output stream.

Use `IO.setStdout` to replace the current thread's standard output stream.
-/
@[extern "lean_get_stdout"] opaque getStdout : BaseIO FS.Stream

Get Standard Output Stream

Informal description

The function `IO.getStdout` returns the current thread's standard output stream as a `BaseIO FS.Stream` computation. This stream can be manipulated or redirected using functions like `IO.setStdout`.

IO.getStderr opaque

: BaseIO FS.Stream

Full source

/--
Returns the current thread's standard error stream.

Use `IO.setStderr` to replace the current thread's standard error stream.
-/
@[extern "lean_get_stderr"] opaque getStderr : BaseIO FS.Stream

Retrieve Current Thread's Standard Error Stream

Informal description

The function `IO.getStderr` retrieves the standard error stream of the current thread, returning it as an `FS.Stream` object within the `BaseIO` monad.

IO.setStdin opaque

: FS.Stream → BaseIO FS.Stream

Full source

/--
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_stdin"] opaque setStdin  : FS.Stream → BaseIO FS.Stream

Set standard input stream and return previous stream

Informal description

The function `IO.setStdin` takes a stream `s` of type `FS.Stream` and returns a `BaseIO` computation that replaces the current standard input stream with `s`, returning the previous standard input stream.

IO.setStdout opaque

: FS.Stream → BaseIO FS.Stream

Full source

/--
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_stdout"] opaque setStdout : FS.Stream → BaseIO FS.Stream

Set Standard Output Stream and Return Previous Stream

Informal description

The function `IO.setStdout` takes a stream `s` of type `FS.Stream` and replaces the current standard output stream of the thread with `s`, returning the previous standard output stream as a result in the `BaseIO` monad.

IO.setStderr opaque

: FS.Stream → BaseIO FS.Stream

Full source

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

Use `IO.getStderr` to get the current standard error stream.
-/
@[extern "lean_get_set_stderr"] opaque setStderr : FS.Stream → BaseIO FS.Stream

Set Standard Error Stream Function

Informal description

The function `IO.setStderr` takes a stream of type `FS.Stream` and replaces the current standard error stream with the given stream, returning the previous standard error stream in the `BaseIO` monad.

IO.iterate definition

(a : α) (f : α → IO (Sum α β)) : IO β

Full source

/--
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.
-/
@[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do
  let v ← f a
  match v with
  | Sum.inl a => iterate a f
  | Sum.inr b => pure b

Iteration of an IO action until completion

Informal description

The function `IO.iterate` repeatedly applies an `IO` action `f` starting with an initial state `a`. The action `f` returns either a new state in `Sum.inl` or a final result in `Sum.inr`. The iteration continues until `f` returns a final result, which is then returned by `IO.iterate`.

IO.FS.Handle.mk opaque

(fn : @& FilePath) (mode : FS.Mode) : IO Handle

Full source

/--
Opens the file at `fn` with the given `mode`.

An exception is thrown if the file cannot be opened.
-/
@[extern "lean_io_prim_handle_mk"] opaque mk (fn : @& FilePath) (mode : FS.Mode) : IO Handle

File handle creation operation

Informal description

The function `IO.FS.Handle.mk` takes a file path `fn` and a file opening mode `mode` as inputs, and returns an `IO Handle` computation that will open the specified file in the given mode when executed. If successful, it produces a file handle reference; if unsuccessful, it throws an exception.

IO.FS.Handle.unlock opaque

(h : @& Handle) : IO Unit

Full source

/--
Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired.
-/
@[extern "lean_io_prim_handle_unlock"] opaque unlock (h : @& Handle) : IO Unit

File Handle Unlock Operation

Informal description

Given a file handle `h`, the operation `unlock` releases any previously-acquired lock on `h`. The operation succeeds even if no lock was previously acquired.

IO.FS.Handle.isTty opaque

(h : @& Handle) : BaseIO Bool

Full source

/--
Returns `true` if a handle refers to a Windows console or a Unix terminal.
-/
@[extern "lean_io_prim_handle_is_tty"] opaque isTty (h : @& Handle) : BaseIO Bool

Check if File Handle is a Terminal

Informal description

Given a file handle `h`, the function `isTty` checks whether `h` refers to a Windows console or a Unix terminal, returning `true` if it does and `false` otherwise.

IO.FS.Handle.flush opaque

(h : @& Handle) : IO Unit

Full source

/--
Flushes the output buffer associated with the handle, writing any unwritten data to the associated
output device.
-/
@[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit

File Handle Flush Operation

Informal description

Given a file handle `h`, the operation `flush` ensures that any buffered data associated with `h` is written to the underlying output device, returning a value of type `Unit` upon completion.

IO.FS.Handle.rewind opaque

(h : @& Handle) : IO Unit

Full source

/--
Rewinds the read/write cursor to the beginning of the handle's file.
-/
@[extern "lean_io_prim_handle_rewind"] opaque rewind (h : @& Handle) : IO Unit

File Handle Rewind Operation

Informal description

Given a file handle `h`, the operation `rewind` resets the read/write cursor to the beginning of the file associated with `h`. This operation is performed within the `IO` monad and returns the unit value `()` upon completion.

IO.FS.Handle.truncate opaque

(h : @& Handle) : IO Unit

Full source

/--
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_truncate"] opaque truncate (h : @& Handle) : IO Unit

File Truncation Operation at Current Cursor Position

Informal description

The operation `truncate` on a file handle `h` reduces the file size to the current position of the read/write cursor. Note that this operation does not automatically flush any buffered output, so the file contents may not immediately reflect the change. To ensure consistency, it is recommended to call `flush` before truncating if there are pending buffered writes.

IO.FS.Handle.read opaque

(h : @& Handle) (bytes : USize) : IO ByteArray

Full source

/--
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_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray

File Handle Read Operation with EOF Detection

Informal description

Given a file handle $h$ and a number of bytes $n$ (represented as a `USize`), the function `read` performs an input/output operation that reads up to $n$ bytes from the file associated with $h$. The operation returns a byte array containing the read data. If the returned byte array is empty, it indicates that the end of the file has been reached (EOF). Note that encountering EOF does not close the handle, and subsequent reads may still return more data if available.

IO.FS.Handle.write opaque

(h : @& Handle) (buffer : @& ByteArray) : IO Unit

Full source

/--
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_write"] opaque write (h : @& Handle) (buffer : @& ByteArray) : IO Unit

File Handle Byte Array Write Operation

Informal description

Given a file handle `h` and a byte array `buffer`, the operation `write` writes the contents of `buffer` to the file associated with `h`. The operation returns a value of type `Unit`, indicating that it is performed for its side effect rather than for a meaningful return value. Note that writes may be buffered and not immediately reflected on disk until flushed.

IO.FS.Handle.getLine opaque

(h : @& Handle) : IO String

Full source

/--
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_get_line"] opaque getLine (h : @& Handle) : IO String

Read Line from File Handle

Informal description

Given a file handle `h`, the operation `getLine` reads a line of UTF-8-encoded text from the handle and returns it as a string. If the returned string is empty, it indicates that the end of the file has been reached. The handle remains open after this operation, and subsequent reads may return more data.

IO.FS.Handle.putStr opaque

(h : @& Handle) (s : @& String) : IO Unit

Full source

/--
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_prim_handle_put_str"] opaque putStr (h : @& Handle) (s : @& String) : IO Unit

File handle string writing operation

Informal description

The function `IO.FS.Handle.putStr` takes a file handle `h` and a string `s`, then writes the string `s` to the file associated with `h` using UTF-8 encoding. The operation returns a value of type `Unit`, indicating it's performed for its side effect rather than returning meaningful data.

IO.FS.realPath opaque

(fname : FilePath) : IO FilePath

Full source

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

This function coincides with the [POSIX `realpath`
function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/realpath.html).
-/
@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath

Canonical Path Resolution Function

Informal description

Given a file path `fname`, the function `realPath` resolves it to an absolute path that contains no relative components (`.` or `..`) or symbolic links, returning the canonicalized path in the `IO` monad.

IO.FS.removeFile opaque

(fname : @& FilePath) : IO Unit

Full source

/--
Removes (deletes) a file from the filesystem.

To remove a directory, use `IO.FS.removeDir` or `IO.FS.removeDirAll` instead.
-/
@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit

File Deletion Operation

Informal description

The function `removeFile` takes a file path `fname` and performs an I/O operation to delete the corresponding file from the filesystem. If the operation fails, it throws an exception.

IO.FS.removeDir opaque

: @& FilePath → IO Unit

Full source

/--
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_remove_dir"] opaque removeDir : @& FilePath → IO Unit

Directory Removal Operation

Informal description

The function `removeDir` takes a file path and performs an I/O operation to remove (delete) the directory at that path. The operation fails if the directory is not empty.

IO.FS.createDir opaque

: @& FilePath → IO Unit

Full source

/--
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_create_dir"] opaque createDir : @& FilePath → IO Unit

Directory Creation Operation

Informal description

The function `createDir` takes a file path and performs an I/O operation to create a directory at that path. The parent directory must exist prior to this operation. If the directory cannot be created, an exception is thrown.

IO.FS.rename opaque

(old new : @& FilePath) : IO Unit

Full source

/--
Moves a file or directory `old` to the new location `new`.

This function coincides with the [POSIX `rename`
function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html).
-/
@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit

File/Directory Rename Operation in IO Monad

Informal description

The function `IO.FS.rename` takes two file paths `old` and `new` as arguments and performs an operation in the `IO` monad that moves the file or directory located at `old` to the new location `new`. This operation coincides with the POSIX `rename` function, which atomically renames a file or directory if possible.

IO.FS.createTempFile opaque

: IO (Handle × FilePath)

Full source

/--
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_tempfile"] opaque createTempFile : IO (HandleHandle × FilePath)

Secure Temporary File Creation with Handle and Path

Informal description

The operation `createTempFile` creates a temporary file in the most secure manner possible, returning both a file handle to the opened file and its path. The file is created with no race conditions and is readable and writable only by the creating user ID (and executable by nobody on UNIX-style platforms). The caller is responsible for removing the file after use.

IO.FS.createTempDir opaque

: IO FilePath

Full source

/--
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_create_tempdir"] opaque createTempDir : IO FilePath

Secure Temporary Directory Creation in IO Monad

Informal description

The operation `IO.FS.createTempDir` creates a temporary directory in the most secure manner possible, ensuring there are no race conditions during its creation. The directory is readable and writable only by the creating user ID. The caller is responsible for removing the directory after use.

IO.getEnv opaque

(var : @& String) : BaseIO (Option String)

Full source

/--
Returns the value of the environment variable `var`, or `none` if it is not present in the
environment.
-/
@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)

Environment Variable Lookup Function

Informal description

Given a string `var` representing an environment variable name, the function returns an optional string value (`Option String`) in the `BaseIO` monad. The result is `some val` if the environment variable `var` exists with value `val`, and `none` if the variable is not present in the environment.

IO.appPath opaque

: IO FilePath

Full source

/--
Returns the file name of the currently-running executable.
-/
@[extern "lean_io_app_path"] opaque appPath : IO FilePath

Executable Path Retrieval

Informal description

The function `IO.appPath` returns the file path of the currently-running executable as an `IO` action.

IO.currentDir opaque

: IO FilePath

Full source

/--
Returns the current working directory of the executing process.
-/
@[extern "lean_io_current_dir"] opaque currentDir : IO FilePath

Current Working Directory Accessor

Informal description

The function `IO.currentDir` returns the current working directory of the executing process as a `FilePath` object within the `IO` monad.

IO.FS.withFile definition

(fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α

Full source

/--
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.
-/
@[inline]
def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α :=
  Handle.mkHandle.mk fn mode >>= f

File handle with automatic cleanup

Informal description

The function `IO.FS.withFile` opens a file specified by the path `fn` in the given `mode` and passes the resulting file handle to the function `f`. The file handle is automatically closed when the last reference to it is dropped. If references to the handle escape `f`, the file remains open even after `IO.FS.withFile` completes.

IO.FS.Handle.putStrLn definition

(h : Handle) (s : String) : IO Unit

Full source

/--
Writes the contents of the string to the handle, followed by a newline. Uses UTF-8.
-/
def Handle.putStrLn (h : Handle) (s : String) : IO Unit :=
  h.putStr (s.push '\n')

File handle string writing with newline

Informal description

The function writes the string `s` followed by a newline character to the file handle `h` using UTF-8 encoding. The operation returns a value of type `Unit`, indicating it's performed for its side effect rather than returning meaningful data.

IO.FS.Handle.readBinToEndInto definition

(h : Handle) (buf : ByteArray) : IO ByteArray

Full source

/--
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.
-/
partial def Handle.readBinToEndInto (h : Handle) (buf : ByteArray) : IO ByteArray := do
  let rec loop (acc : ByteArray) : IO ByteArray := do
    let buf ← h.read 1024
    if buf.isEmpty then
      return acc
    else
      loop (acc ++ buf)
  loop buf

Read binary file contents into buffer

Informal description

The function reads the entire remaining contents of the file handle `h` into a byte array, starting with the initial contents of `buf`. It repeatedly reads chunks of 1024 bytes from the handle until an empty chunk is encountered (indicating end-of-file), appending each chunk to the accumulator byte array. The final result is the concatenation of `buf` and all bytes read from the handle.

IO.FS.Handle.readBinToEnd definition

(h : Handle) : IO ByteArray

Full source

/--
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.
-/
partial def Handle.readBinToEnd (h : Handle) : IO ByteArray := do
  h.readBinToEndInto .empty

Read binary file contents to end

Informal description

The function reads the entire remaining binary contents of the file handle `h` and returns them as a byte array. It reads chunks of data from the file until reaching the end-of-file marker, accumulating all bytes read into a single byte array.

IO.FS.Handle.readToEnd definition

(h : Handle) : IO String

Full source

/--
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.
-/
def Handle.readToEnd (h : Handle) : IO String := do
  let data ← h.readBinToEnd
  match String.fromUTF8? data with
  | somesome s => return s
  | none => throw <| .userError s!"Tried to read from handle containing non UTF-8 data."

Read file contents as UTF-8 string

Informal description

The function reads the entire remaining contents of the file handle `h` as a UTF-8-encoded string. If the contents are not valid UTF-8, it throws an exception indicating the data is invalid.

IO.FS.lines definition

(fname : FilePath) : IO (Array String)

Full source

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

Newline markers are not included in the lines.
-/
partial def lines (fname : FilePath) : IO (Array String) := do
  let h ← Handle.mk fname Mode.read
  let rec read (lines : Array String) := do
    let line ← h.getLine
    if line.length == 0 then
      pure lines
    else if line.back == '\n' then
      let line := line.dropRight 1
      let line := if line.back == '\r' then line.dropRight 1 else line
      read <| lines.push line
    else
      pure <| lines.push line
  read #[]

Read file lines as string array

Informal description

Given a file path `fname`, the function reads the contents of the UTF-8-encoded text file and returns an array of strings, where each string represents a line from the file. Newline markers (`\n` and `\r\n`) are stripped from the end of each line. If a line ends without a newline marker, it is still included in the array.

IO.FS.writeBinFile definition

(fname : FilePath) (content : ByteArray) : IO Unit

Full source

/--
Write the provided bytes to a binary file at the specified path.
-/
def writeBinFile (fname : FilePath) (content : ByteArray) : IO Unit := do
  let h ← Handle.mk fname Mode.write
  h.write content

Binary file write operation

Informal description

The function takes a file path `fname` and a byte array `content` as inputs, and performs an input/output operation that writes the contents of `content` to the file specified by `fname` in binary mode. The operation returns a value of type `Unit`, indicating it is performed for its side effect rather than for a meaningful return value.

IO.FS.writeFile definition

(fname : FilePath) (content : String) : IO Unit

Full source

/--
Write contents of a string to a file at the specified path using UTF-8 encoding.
-/
def writeFile (fname : FilePath) (content : String) : IO Unit := do
  let h ← Handle.mk fname Mode.write
  h.putStr content

File writing operation with UTF-8 encoding

Informal description

The function takes a file path `fname` and a string `content`, then writes the contents of the string to the specified file using UTF-8 encoding. The operation returns a value of type `Unit`, indicating it's performed for its side effect rather than returning meaningful data.

IO.FS.Stream.putStrLn definition

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

Full source

/--
Writes the contents of the string to the stream, followed by a newline.
-/
def Stream.putStrLn (strm : FS.Stream) (s : String) : IO Unit :=
  strm.putStr (s.push '\n')

Write string with newline to stream

Informal description

The function writes the given string `s` followed by a newline character to the specified stream `strm`, returning a value of type `Unit` to indicate the operation is performed for its side effect.

IO.FS.DirEntry structure

Full source

/-- An entry in a directory on a filesystem. -/
structure DirEntry where
  /-- The directory in which the entry is found. -/
  root     : FilePath
  /-- The name of the entry. -/
  fileName : String
  deriving Repr

Filesystem Directory Entry

Informal description

A structure representing an entry in a filesystem directory, containing information about a file or subdirectory. Each entry has an associated path (accessible via the `path` field).

IO.FS.instReprDirEntry instance

: Repr✝ (@IO.FS.DirEntry✝)

Full source

Repr

Representation Instance for Filesystem Directory Entries

Informal description

The structure `IO.FS.DirEntry` representing a filesystem directory entry has a canonical representation instance.

IO.FS.DirEntry.path definition

(entry : DirEntry) : FilePath

Full source

/-- The path of the file indicated by the directory entry. -/
def DirEntry.path (entry : DirEntry) : FilePath :=
  entry.root / entry.fileName

File path of a directory entry

Informal description

Given a directory entry `entry`, the function returns the file path constructed by combining the root directory of the entry with its filename using the platform-specific path separator.

IO.FS.FileType inductive

Full source

/-- Types of files that may be found on a filesystem. -/
inductive FileType where
  /-- Directories don't have contents, but may contain other files. -/
  | dir
  /-- Ordinary files that have contents and are not directories. -/
  | file
  /-- Symbolic links that are pointers to other named files. -/
  | symlink
  /-- Files that are neither ordinary files, directories, or symbolic links. -/
  | other
  deriving Repr, BEq

File types on a filesystem

Informal description

An inductive type representing the different types of files that can be found on a filesystem, such as regular files, directories, symbolic links, etc.

IO.FS.instReprFileType instance

: Repr✝ (@IO.FS.FileType✝)

Full source

Repr, BEq

Representation Instance for File Types

Informal description

The type `IO.FS.FileType` has a canonical representation instance, allowing its values to be displayed in a human-readable format.

IO.FS.instBEqFileType instance

: BEq✝ (@IO.FS.FileType✝)

Full source

BEq

Boolean Equality for File Types

Informal description

The type `IO.FS.FileType` has a boolean equality relation `==` that can be used to compare file types.

IO.FS.SystemTime structure

Full source

/--
Low-level system time, tracked in whole seconds and additional nanoseconds.
-/
structure SystemTime where
  /-- The number of whole seconds. -/
  sec  : Int
  /-- The number of additional nanoseconds. -/
  nsec : UInt32
  deriving Repr, BEq, Ord, Inhabited

System Time

Informal description

The structure representing system time, consisting of whole seconds and additional nanoseconds.

IO.FS.instReprSystemTime instance

: Repr✝ (@IO.FS.SystemTime✝)

Full source

Repr, BEq, Ord, Inhabited

String Representation of System Time Structure

Informal description

The structure `IO.FS.SystemTime` representing system time (with seconds and nanoseconds components) has a canonical string representation.

IO.FS.instBEqSystemTime instance

: BEq✝ (@IO.FS.SystemTime✝)

Full source

BEq, Ord, Inhabited

Boolean Equality for System Time

Informal description

The system time structure `IO.FS.SystemTime` is equipped with a boolean-valued equality relation `==`.

IO.FS.instOrdSystemTime instance

: Ord✝ (@IO.FS.SystemTime✝)

Full source

Ord, Inhabited

Total Order on System Time

Informal description

The system time structure `IO.FS.SystemTime` is equipped with a canonical total order.

IO.FS.instInhabitedSystemTime instance

: Inhabited✝ (@IO.FS.SystemTime)

Full source

Inhabited

Inhabited System Time Structure

Informal description

The system time structure `IO.FS.SystemTime` is inhabited, with a default value.

IO.FS.instLTSystemTime instance

: LT SystemTime

Full source

instance : LT SystemTime := ltOfOrd

The < Relation on System Time

Informal description

The system time structure `IO.FS.SystemTime` is equipped with a canonical "less than" relation.

IO.FS.instLESystemTime instance

: LE SystemTime

Full source

instance : LE SystemTime := leOfOrd

The ≤ Relation on System Time

Informal description

The system time structure `IO.FS.SystemTime` is equipped with a canonical "less than or equal to" relation.

IO.FS.Metadata structure

Full source

/--
File metadata.

The metadata for a file can be accessed with `System.FilePath.metadata`.
-/
structure Metadata where
  --permissions : ...
  /-- File access time. -/
  accessed : SystemTime
  /-- File modification time. -/
  modified : SystemTime
  /-- The size of the file in bytes. -/
  byteSize : UInt64
  /--
  Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file.
  -/
  type     : FileType
  deriving Repr

File Metadata

Informal description

The structure representing file metadata, which contains information about a file such as its size, permissions, and timestamps. This metadata can be accessed using file system operations.

IO.FS.instReprMetadata instance

: Repr✝ (@IO.FS.Metadata✝)

Full source

Repr

Representation Instance for File Metadata

Informal description

The file metadata structure `IO.FS.Metadata` has a representation instance that allows it to be displayed in a human-readable format.

System.FilePath.readDir opaque

: @& FilePath → IO (Array IO.FS.DirEntry)

Full source

/--
Returns the contents of the indicated directory. Throws an exception if the file does not exist or
is not a directory.
-/
@[extern "lean_io_read_dir"]
opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry)

Directory Contents Reader

Informal description

Given a file path `p`, the function returns an array of directory entries (files and subdirectories) contained in the directory at path `p`. The operation may throw an exception if the path does not exist or is not a directory.

System.FilePath.metadata opaque

: @& FilePath → IO IO.FS.Metadata

Full source

/--
Returns metadata for the indicated file. Throws an exception if the file does not exist or the
metadata cannot be accessed.
-/
@[extern "lean_io_metadata"]
opaque metadata : @& FilePath → IO IO.FS.Metadata

File Metadata Accessor

Informal description

The function `FilePath.metadata` takes a file path and returns an `IO` action that, when executed, produces the metadata associated with the file at that path. If the file does not exist or the metadata cannot be accessed, an exception is thrown.

System.FilePath.isDir definition

(p : FilePath) : BaseIO Bool

Full source

/--
Checks whether the indicated path can be read and is a directory.
-/
def isDir (p : FilePath) : BaseIO Bool := do
  match (← p.metadata.toBaseIO) with
  | Except.ok m => return m.type == IO.FS.FileType.dir
  | Except.error _ => return false

Directory existence check

Informal description

Given a file path `p`, the function checks whether `p` exists and is a directory. It returns `true` if the path exists and its metadata indicates it is a directory, and `false` otherwise (including when the path does not exist or cannot be accessed).

System.FilePath.pathExists definition

(p : FilePath) : BaseIO Bool

Full source

/--
Checks whether the indicated path points to a file that exists.
-/
def pathExists (p : FilePath) : BaseIO Bool :=
  return (← p.metadata.toBaseIO).toBool

File existence check

Informal description

The function checks whether a file exists at the given path `p`, returning `true` if it exists and `false` otherwise. It does this by attempting to access the file's metadata and converting the result to a boolean value.

IO.FS.readBinFile definition

(fname : FilePath) : IO ByteArray

Full source

/--
Reads the entire contents of the binary file at the given path as an array of bytes.
-/
def readBinFile (fname : FilePath) : IO ByteArray := do
  -- Requires metadata so defined after metadata
  let mdata ← fname.metadata
  let size := mdata.byteSize.toUSize
  let handle ← IO.FS.Handle.mk fname .read
  let buf ←
    if size > 0 then
      handle.read mdata.byteSize.toUSize
    else
      pure <| ByteArray.emptyWithCapacity 0
  handle.readBinToEndInto buf

Binary file reader

Informal description

The function reads the entire contents of the binary file at the given path `fname` as a byte array. It first retrieves the file's metadata to determine its size, then opens the file in read mode. If the file has non-zero size, it reads the initial contents into a buffer of the appropriate size. Finally, it reads any remaining contents into the buffer until the end of the file is reached, returning the complete byte array.

IO.FS.readFile definition

(fname : FilePath) : IO String

Full source

/--
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.
-/
def readFile (fname : FilePath) : IO String := do
  let data ← readBinFile fname
  match String.fromUTF8? data with
  | somesome s => return s
  | none => throw <| .userError s!"Tried to read file '{fname}' containing non UTF-8 data."

UTF-8 file reader

Informal description

The function reads the entire contents of the UTF-8-encoded file at the given path `fname` as a string. If the file contains invalid UTF-8 data, it throws an exception with an error message indicating that the file contains non-UTF-8 data.

IO.withStdin definition

[Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Full source

/--
Runs an action with the specified stream `h` as standard input, restoring the original standard
input stream afterwards.
-/
def withStdin [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do
  let prev ← setStdin h
  try x finally discard <| setStdin prev

Temporarily set standard input stream

Informal description

Given a monad `m` that supports exception handling and lifting from `BaseIO`, a stream `h`, and a computation `x` in `m`, the function `IO.withStdin` temporarily sets `h` as the standard input stream while running `x`, then restores the original standard input stream afterward.

IO.withStdout definition

[Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Full source

/--
Runs an action with the specified stream `h` as standard output, restoring the original standard
output stream afterwards.
-/
def withStdout [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do
  let prev ← setStdout h
  try
    x
  finally
    discard <| setStdout prev

Temporarily redirect standard output

Informal description

The function `IO.withStdout` temporarily sets the standard output stream to `h`, runs the monadic action `x`, and then restores the original standard output stream. The action `x` is executed in a monad `m` that supports monadic lifting from `BaseIO` and has a `finally` block for cleanup.

IO.withStderr definition

[Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α

Full source

/--
Runs an action with the specified stream `h` as standard error, restoring the original standard
error stream afterwards.
-/
def withStderr [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do
  let prev ← setStderr h
  try x finally discard <| setStderr prev

Temporary standard error stream replacement

Informal description

The function `IO.withStderr` temporarily replaces the standard error stream with the specified stream `h`, runs the action `x`, and then restores the original standard error stream. The restoration happens even if the action `x` throws an exception.

IO.print definition

[ToString α] (s : α) : IO Unit

Full source

/--
Converts `s` to a string using its `ToString α` instance, and prints it to the current standard
output (as determined by `IO.getStdout`).
-/
def print [ToString α] (s : α) : IO Unit := do
  let out ← getStdout
  out.putStr <| toString s

Print to standard output

Informal description

The function `IO.print` converts the input `s` of type `α` to a string using its `ToString` instance and prints it to the standard output stream. This operation is performed within the `IO` monad, which handles input/output operations and potential exceptions.

IO.println definition

[ToString α] (s : α) : IO Unit

Full source

/--
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`).
-/
def println [ToString α] (s : α) : IO Unit :=
  print ((toString s).push '\n')

Print line to standard output

Informal description

The function converts an element `s` of type `α` to a string using its `ToString` instance, appends a newline character, and prints the resulting string to the standard output stream.

IO.eprint definition

[ToString α] (s : α) : IO Unit

Full source

/--
Converts `s` to a string using its `ToString α` instance, and prints it to the current standard
error (as determined by `IO.getStderr`).
-/
def eprint [ToString α] (s : α) : IO Unit := do
  let out ← getStderr
  out.putStr <| toString s

Print to standard error

Informal description

The function converts an element `s` of type `α` to a string using its `ToString` instance and prints it to the standard error stream.

IO.eprintln definition

[ToString α] (s : α) : IO Unit

Full source

/--
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`).
-/
def eprintln [ToString α] (s : α) : IO Unit :=
  eprint <| toString s |>.push '\n'

Print to standard error with newline

Informal description

The function converts an element `s` of type `α` to a string using its `ToString` instance and prints it with a trailing newline to the standard error stream.

IO.appDir definition

: IO FilePath

Full source

/--
Returns the directory that the current executable is located in.
-/
def appDir : IO FilePath := do
  let p ← appPath
  let some p ← pure p.parent
    | throw <| IO.userError s!"IO.appDir: unexpected filename '{p}'"
  FS.realPath p

Executable directory retrieval

Informal description

The function returns the directory containing the current executable as an `IO` action. It first retrieves the path of the executable using `appPath`, then gets its parent directory (failing with an error if the path has no parent), and finally resolves this path to its canonical form (removing any symbolic links or relative components).

IO.FS.createDirAll definition

(p : FilePath) : IO Unit

Full source

/--
Creates a directory at the specified path, creating all missing parents as directories.
-/
partial def createDirAll (p : FilePath) : IO Unit := do
  if ← p.isDir then
    return ()
  if let some parent := p.parent then
    createDirAll parent
  try
    createDir p
  catch
    | e =>
      if ← p.isDir then
        pure ()  -- I guess someone else was faster
      else
        throw e

Recursive directory creation

Informal description

The function creates a directory at the specified file path `p`, including all missing parent directories along the path. If the directory already exists, the function does nothing. If any parent directories are missing, they are created recursively before creating the target directory. If the directory creation fails for any reason other than the directory already existing, the exception is propagated.

IO.FS.removeDirAll definition

(p : FilePath) : IO Unit

Full source

/--
  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. -/
partial def removeDirAll (p : FilePath) : IO Unit := do
  for ent in (← p.readDir) do
    if (← ent.path.isDir : Bool) then
      removeDirAll ent.path
    else
      removeFile ent.path
  removeDir p

Recursive directory removal

Informal description

The function `IO.FS.removeDirAll` takes a file path `p` and performs an IO action that recursively deletes all files and subdirectories contained in `p`, then deletes `p` itself. The operation fails if any contained entry cannot be deleted or if new entries are created during execution.

IO.FS.withTempFile definition

[Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) : m α

Full source

/--
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.
-/
def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) :
    m α := do
  let (handle, path) ← createTempFile
  try
    f handle path
  finally
    removeFile path

Secure temporary file creation with automatic cleanup

Informal description

The function `withTempFile` creates a temporary file in the most secure manner possible, providing both a handle to the opened file and its path to the function `f`. After `f` completes execution (whether normally or via an exception), the temporary file is automatically deleted. The file is created with permissions ensuring it is readable and writable only by the creating user ID (and executable by nobody on UNIX-style platforms).

IO.FS.withTempDir definition

[Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) : m α

Full source

/--
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.
-/
def withTempDir [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) :
    m α := do
  let path ← createTempDir
  try
    f path
  finally
    removeDirAll path

Temporary directory with automatic cleanup

Informal description

The function `IO.FS.withTempDir` creates a temporary directory in the most secure manner possible, providing its path to a monadic action `f`. After the action completes (whether successfully or with an exception), the directory and all its contents are recursively deleted. The function operates within any monad `m` that supports lifting from `IO` and has a `MonadFinally` instance for cleanup.

IO.Process.getCurrentDir opaque

: IO FilePath

Full source

/-- Returns the current working directory of the calling process. -/
@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath

Get Current Working Directory

Informal description

The function returns the current working directory of the calling process as a file path.

IO.Process.setCurrentDir opaque

(path : @& FilePath) : IO Unit

Full source

/-- Sets the current working directory of the calling process. -/
@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit

Set Current Working Directory Operation

Informal description

The function `IO.Process.setCurrentDir` takes a file path `path` and performs an input/output operation that sets the current working directory of the calling process to `path`. The operation returns the unit value `()` upon success.

IO.Process.getPID opaque

: BaseIO UInt32

Full source

/-- Returns the process ID of the calling process. -/
@[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32

Get Current Process ID

Informal description

The function `IO.Process.getPID` returns the process ID (PID) of the calling process as an unsigned 32-bit integer, within the `BaseIO` monad context.

IO.Process.Stdio inductive

Full source

/--
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.
-/
inductive Stdio where
  /-- The stream should be attached to a pipe. -/
  | piped
  /-- The stream should be inherited from the parent process. -/
  | inherit
  /-- The stream should be empty. -/
  | null

Child process standard I/O configuration

Informal description

An inductive type representing the configuration options for standard input, output, and error handles of a child process. Each handle can be: - Piped (connected to a pipe for inter-process communication) - Inherited (shared with the parent process) - Null (disconnected) When a handle is piped, the parent process can use it to communicate with the child process.

IO.Process.Stdio.toHandleType definition

: Stdio → Type

Full source

/--
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.
-/
def Stdio.toHandleType : Stdio → Type
  | Stdio.piped   => FS.Handle
  | Stdio.inherit => Unit
  | Stdio.null    => Unit

Handle type for child process standard I/O configuration

Informal description

The function maps a standard I/O configuration for a child process to the corresponding handle type: - For `Stdio.piped`, it returns the type `IO.FS.Handle` (a file handle for inter-process communication) - For `Stdio.inherit` or `Stdio.null`, it returns the type `Unit` (indicating no communication is possible)

IO.Process.StdioConfig structure

Full source

/--
Configuration for the standard input, output, and error handles of a child process.
-/
structure StdioConfig where
  /-- Configuration for the process' stdin handle. -/
  stdin := Stdio.inherit
  /-- Configuration for the process' stdout handle. -/
  stdout := Stdio.inherit
  /-- Configuration for the process' stderr handle. -/
  stderr := Stdio.inherit

Standard I/O Configuration for Child Processes

Informal description

The structure `StdioConfig` represents the configuration for standard input, output, and error streams of a child process. It specifies how these standard I/O handles should be set up when spawning a new process.

IO.Process.SpawnArgs structure

extends StdioConfig

Full source

/--
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.
-/
structure SpawnArgs extends StdioConfig where
  /-- Command name. -/
  cmd : String
  /-- Arguments for the command. -/
  args : Array String := #[]
  /-- The child process's working directory. Inherited from the parent current process if `none`. -/
  cwd : Option FilePath := none
  /--
  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.
  -/
  env : Array (StringString × Option String) := #[]
  /--
  Starts the child process in a new session and process group using `setsid`. Currently a no-op on
  non-POSIX platforms.
  -/
  setsid : Bool := false

Child process spawning configuration

Informal description

A configuration structure for spawning a child process, extending the standard I/O configuration. This structure is used when starting a new process with `IO.Process.spawn`, and is also the basis for configurations where the child process should be run to completion with its output and/or error code captured (via `IO.Process.output` and `IO.Process.run`).

IO.Process.Child structure

(cfg : StdioConfig)

Full source

/--
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.Handle`s or `Unit`.
-/
-- TODO(Sebastian): constructor must be private
structure Child (cfg : StdioConfig) where
  /--
  The child process's standard input handle, if it was configured as `IO.Process.Stdio.piped`, or
  `()` otherwise.
  -/
  stdin  : cfg.stdin.toHandleType
  /--
  The child process's standard output handle, if it was configured as `IO.Process.Stdio.piped`, or
  `()` otherwise.
  -/
  stdout : cfg.stdout.toHandleType
  /--
  The child process's standard error handle, if it was configured as `IO.Process.Stdio.piped`, or
  `()` otherwise.
  -/
  stderr : cfg.stderr.toHandleType

Child process with standard I/O configuration

Informal description

A structure representing a child process spawned with a given standard I/O configuration `cfg`. The configuration determines how the child process's standard input, output, and error streams are handled.

IO.Process.spawn opaque

(args : SpawnArgs) : IO (Child args.toStdioConfig)

Full source

/--
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_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)

Child Process Spawning Operation

Informal description

The function `spawn` takes a process configuration `args` of type `SpawnArgs` and returns an `IO` computation that produces a child process handle with the specified standard I/O configuration (obtained via `args.toStdioConfig`). The child process runs concurrently with the parent process.

IO.Process.Child.wait opaque

{cfg : @& StdioConfig} : @& Child cfg → IO UInt32

Full source

/--
Blocks until the child process has exited and return its exit code.
-/
@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32

Blocking Wait for Child Process Termination

Informal description

Given a child process with standard I/O configuration `cfg`, the operation `wait` blocks until the child process terminates and returns its exit code as an unsigned 32-bit integer.

IO.Process.Child.tryWait opaque

{cfg : @& StdioConfig} : @& Child cfg → IO (Option UInt32)

Full source

/--
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_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg →
    IO (Option UInt32)

Non-blocking Check for Child Process Exit Status

Informal description

Given a child process with standard I/O configuration `cfg`, the function `tryWait` checks whether the process has exited. It returns `none` if the process is still running, or returns `some exitCode` where `exitCode` is a 32-bit unsigned integer representing the process's exit code if it has terminated.

IO.Process.Child.kill opaque

{cfg : @& StdioConfig} : @& Child cfg → IO Unit

Full source

/--
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_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit

Termination of Child Process via SIGTERM

Informal description

Given a child process with standard I/O configuration `cfg`, the `kill` operation sends a termination signal (`SIGTERM` or platform equivalent) to terminate the process. If the process was started with `setsid`, it terminates the entire process group instead.

IO.Process.Child.takeStdin opaque

{cfg : @& StdioConfig} : Child cfg → IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null })

Full source

/--
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.
-/
@[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg →
    IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null })

Extract and Nullify Standard Input Handle from Child Process

Informal description

Given a child process with standard I/O configuration `cfg`, the operation `takeStdin` extracts the standard input handle from the child process and returns a pair consisting of: 1. The handle of type `cfg.stdin.toHandleType` (which is either an `IO.FS.Handle` for piped input or `Unit` otherwise) 2. A modified child process where the standard input is set to `Stdio.null` This allows the handle to be closed independently while maintaining a reference to the child process.

IO.Process.Output structure

Full source

/--
The result of running a process to completion.
-/
structure Output where
  /-- The process's exit code. -/
  exitCode : UInt32
  /-- Everything that was written to the process's standard output. -/
  stdout   : String
  /-- Everything that was written to the process's standard error. -/
  stderr   : String

Process Execution Output

Informal description

The structure representing the output of a completed process execution, including its exit status and any produced output streams.

IO.Process.output definition

(args : SpawnArgs) : IO Output

Full source

/--
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.
-/
def output (args : SpawnArgs) : IO Output := do
  let child ← spawn { args with stdout := .piped, stderr := .piped, stdin := .null }
  let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
  let stderr ← child.stderr.readToEnd
  let exitCode ← child.wait
  let stdout ← IO.ofExcept stdout.get
  pure { exitCode := exitCode, stdout := stdout, stderr := stderr }

Capture process output and exit code

Informal description

The function `IO.Process.output` takes a process configuration `args` of type `SpawnArgs` and returns an `IO` computation that produces an `Output` structure containing the exit code, standard output, and standard error of the completed child process. The child process is spawned with its standard input set to null and its standard output and error streams piped for capture. The function blocks until the process completes, reading both output streams and collecting the exit code.

IO.Process.run definition

(args : SpawnArgs) : IO String

Full source

/--
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.
-/
def run (args : SpawnArgs) : IO String := do
  let out ← output args
  if out.exitCode != 0 then
    throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
  pure out.stdout

Run process and capture output or throw on failure

Informal description

The function `IO.Process.run` takes a process configuration `args` of type `SpawnArgs` and returns an `IO` computation that produces the standard output of the completed child process as a string. If the child process terminates with a non-zero exit code, an exception is thrown with an error message indicating the process name and exit code. Otherwise, the standard output is returned.

IO.Process.exit opaque

: UInt8 → IO α

Full source

/--
Terminates the current process with the provided exit code. `0` indicates success, all other values
indicate failure.
-/
@[extern "lean_io_exit"] opaque exit : UInt8 → IO α

Process Termination with Exit Code

Informal description

The function `IO.Process.exit` terminates the current process with the specified exit code, where `0` indicates success and any other value indicates failure. The function takes an unsigned 8-bit integer as input and returns an `IO` computation that produces a value of any type `α` (though the process terminates before any value is actually produced).

IO.getTID opaque

: BaseIO UInt64

Full source

/-- Returns the thread ID of the calling thread. -/
@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64

Thread ID retrieval in exception-free I/O context

Informal description

The function `IO.getTID` returns the thread ID of the calling thread as an unsigned 64-bit integer, within the `BaseIO` monad which performs I/O operations without throwing exceptions.

IO.AccessRight structure

Full source

/--
POSIX-style file permissions.

The `FileRight` structure describes these permissions for a file's owner, members of it's designated
group, and all others.
-/
structure AccessRight where
  /-- The file can be read. -/
  read : Bool := false
  /-- The file can be written to. -/
  write : Bool := false
  /-- The file can be executed. -/
  execution : Bool := false

File Access Permissions

Informal description

The structure `AccessRight` represents POSIX-style file access permissions, describing the read, write, and execute permissions for a file's owner, group members, and others.

IO.AccessRight.flags definition

(acc : AccessRight) : UInt32

Full source

/--
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`
-/
def AccessRight.flags (acc : AccessRight) : UInt32 :=
  let r : UInt32 := if acc.read      then 0x4 else 0
  let w : UInt32 := if acc.write     then 0x2 else 0
  let x : UInt32 := if acc.execution then 0x1 else 0
  r.lor <| w.lor x

3-bit representation of file access permissions

Informal description

Given a file access permission `acc` of type `AccessRight`, the function computes a 3-bit unsigned integer representation where: - The read permission (if true) contributes `0x4` (binary 100) - The write permission (if true) contributes `0x2` (binary 010) - The execute permission (if true) contributes `0x1` (binary 001) The final value is obtained by performing a bitwise OR operation on these contributions. For example: - `{read := true}` produces `4` (binary 100) - `{read := true, write := true}` produces `6` (binary 110) - `{read := true, execution := true}` produces `5` (binary 101)

IO.FileRight structure

Full source

/--
POSIX-style file permissions that describe access rights for a file's owner, members of its
assigned group, and all others.
-/
structure FileRight where
  /-- The owner's permissions to access the file. -/
  user  : AccessRight := {}
  /-- The assigned group's permissions to access the file. -/
  group : AccessRight := {}
  /-- The permissions that all others have to access the file. -/
  other : AccessRight := {}

POSIX file permissions

Informal description

The structure representing POSIX-style file permissions, which specify access rights for three categories of users: the file's owner, members of the file's group, and all other users.

IO.FileRight.flags definition

(acc : FileRight) : UInt32

Full source

/--
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.
-/
def FileRight.flags (acc : FileRight) : UInt32 :=
  let u : UInt32 := acc.user.flags.shiftLeft 6
  let g : UInt32 := acc.group.flags.shiftLeft 3
  let o : UInt32 := acc.other.flags
  u.lor <| g.lor o

Numeric representation of POSIX file permissions

Informal description

Given a POSIX-style file permission structure `acc`, the function computes its numeric representation as a 32-bit unsigned integer. The permissions for the owner, group, and others are encoded in three separate 3-bit segments (bits 6-8 for owner, bits 3-5 for group, and bits 0-2 for others). The final value is obtained by combining these segments using bitwise OR operations.

IO.Prim.setAccessRights opaque

(filename : @& FilePath) (mode : UInt32) : IO Unit

Full source

@[extern "lean_chmod"] opaque Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit

File Permission Setting Primitive Operation

Informal description

The primitive operation `setAccessRights` takes a file path `filename` and a 32-bit unsigned integer `mode` representing file permissions, and performs an input/output action that sets the access rights of the specified file to the given mode. The operation returns no meaningful value (denoted by `Unit`).

IO.setAccessRights definition

(filename : FilePath) (mode : FileRight) : IO Unit

Full source

/--
Sets the POSIX-style permissions for a file.
-/
def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit :=
  Prim.setAccessRights filename mode.flags

Set file permissions

Informal description

The function `IO.setAccessRights` takes a file path `filename` and a POSIX-style file permission structure `mode`, and performs an input/output action that sets the access rights of the specified file to the given permissions. The operation returns no meaningful value (denoted by `Unit`).

IO.Ref abbrev

(α : Type)

Full source

/--
Mutable reference cells that contain values of type `α`. These cells can read from and mutated in
the `IO` monad.
-/
abbrev Ref (α : Type) := ST.Ref IO.RealWorld α

IO Mutable Reference Cell

Informal description

A mutable reference cell containing a value of type $\alpha$, which can be read from and modified within the `IO` monad.

IO.instMonadLiftSTRealWorldBaseIO instance

: MonadLift (ST IO.RealWorld) BaseIO

Full source

instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩

Lifting from State-Only IO to Exception-Free IO

Informal description

There is a canonical way to lift computations from the state-only restricted IO monad `ST IO.RealWorld` to the exception-free IO monad `BaseIO`.

IO.mkRef definition

(a : α) : BaseIO (IO.Ref α)

Full source

/--
Creates a new mutable reference cell that contains `a`.
-/
def mkRef (a : α) : BaseIO (IO.Ref α) :=
  ST.mkRef a

Create mutable reference in `BaseIO` monad

Informal description

The function creates a new mutable reference cell in the `BaseIO` monad, initialized with the value `a` of type `α`. The reference cell can be used to store and modify mutable state within the `BaseIO` monad.

IO.CancelToken structure

Full source

/--
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.
-/
structure CancelToken where
  private ref : IO.Ref Bool
deriving Nonempty

Cooperative task cancellation token

Informal description

A mutable cell used for cooperative task cancellation, allowing cancellation requests to be signaled with `CancelToken.set` and checked with `CancelToken.isSet`. This provides a more flexible alternative to `Task.cancel` as the token can be shared among multiple tasks.

IO.instNonemptyCancelToken instance

: Nonempty✝ (@IO.CancelToken✝)

Full source

Nonempty

Nonemptiness of IO Cancellation Tokens

Informal description

The type `IO.CancelToken` is nonempty, meaning there exists at least one cancellation token for cooperative task cancellation.

IO.CancelToken.new definition

: BaseIO CancelToken

Full source

/-- Creates a new cancellation token. -/
def new : BaseIO CancelToken :=
  CancelToken.mkCancelToken.mk <$> IO.mkRef false

Create new cancellation token

Informal description

The function creates a new cancellation token in the exception-free IO monad `BaseIO`, initialized to the "not cancelled" state.

IO.CancelToken.set definition

(tk : CancelToken) : BaseIO Unit

Full source

/-- Activates a cancellation token. Idempotent. -/
def set (tk : CancelToken) : BaseIO Unit :=
  tk.ref.set true

Setting a cancellation token

Informal description

The function `IO.CancelToken.set` takes a cancellation token `tk` and sets it to the "cancelled" state, returning the unit value `()`. This operation is performed in the exception-free IO monad `BaseIO`.

IO.CancelToken.isSet definition

(tk : CancelToken) : BaseIO Bool

Full source

/-- Checks whether the cancellation token has been activated. -/
def isSet (tk : CancelToken) : BaseIO Bool :=
  tk.ref.get

Check cancellation token status

Informal description

Given a cancellation token `tk`, the function checks whether the token has been activated, returning a boolean value in the exception-free IO monad.

IO.FS.Stream.ofHandle definition

(h : Handle) : Stream

Full source

/--
Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding
file handle operation.
-/
@[export lean_stream_of_handle]
def ofHandle (h : Handle) : Stream where
  flush   := Handle.flush h
  read    := Handle.read h
  write   := Handle.write h
  getLine := Handle.getLine h
  putStr  := Handle.putStr h
  isTty   := Handle.isTty h

Stream construction from file handle

Informal description

Given a file handle `h`, the function `IO.FS.Stream.ofHandle` constructs a stream that delegates its operations to the corresponding file handle operations. Specifically: - Flushing the stream flushes the file handle - Reading from the stream reads from the file handle - Writing to the stream writes to the file handle - Getting a line from the stream reads a line from the file handle - Writing a string to the stream writes the string to the file handle - Checking if the stream is a terminal checks if the file handle is a terminal

IO.FS.Stream.Buffer structure

Full source

/--
A byte buffer that can simulate a file in memory.

Use `IO.FS.Stream.ofBuffer` to create a stream from a buffer.
-/
structure Buffer where
  /-- The contents of the buffer. -/
  data : ByteArray := ByteArray.empty
  /-- The read/write cursor's position in the buffer. -/
  pos  : Nat := 0

In-memory byte buffer

Informal description

A structure representing an in-memory byte buffer that can simulate a file, allowing operations similar to file I/O streams. It can be converted to a stream using `IO.FS.Stream.ofBuffer`.

IO.FS.Stream.ofBuffer definition

(r : Ref Buffer) : Stream

Full source

/--
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.
-/
def ofBuffer (r : Ref Buffer) : Stream where
  flush   := pure ()
  read    := fun n => r.modifyGet fun b =>
    let data := b.data.extract b.pos (b.pos + n.toNat)
    (data, { b with pos := b.pos + data.size })
  write   := fun data => r.modify fun b =>
    -- set `exact` to `false` so that repeatedly writing to the stream does not impose quadratic run time
    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
  getLine := do
    let buf ← r.modifyGet fun b =>
      let pos := match b.data.findIdx? (start := b.pos) fun u => u == 0 || u = '\n'.toNat.toUInt8 with
        -- include '\n', but not '\0'
        | some pos => if b.data.get! pos == 0 then pos else pos + 1
        | none     => b.data.size
      (b.data.extract b.pos pos, { b with pos := pos })
    match String.fromUTF8? buf with
    | somesome str => pure str
    | none => throw (.userError "invalid UTF-8")
  putStr  := fun s => r.modify fun b =>
    let data := s.toUTF8
    { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
  isTty   := pure false

Stream from mutable buffer reference

Informal description

Given a mutable reference `r` to a buffer, this function creates a stream that simulates file operations by reading from and writing to the buffer. The stream supports the following operations: - **Flushing**: Does nothing (always succeeds) - **Reading**: Reads up to `n` bytes from the current position in the buffer, advancing the position - **Writing**: Appends data to the buffer at the current position, advancing the position - **Getting a line**: Reads until a newline or null character is found - **Writing a string**: Converts the string to UTF-8 and appends it to the buffer - **Terminal check**: Always returns false (not a terminal) The stream maintains the buffer's position and updates it after each operation.

termPrintln!__ definition

: Lean.ParserDescr✝

Full source

syntaxsyntax "println! " (interpolatedStr(term) <|> term) : term

Println macro syntax

Informal description

The `println!` macro is a syntax construct for printing output, which takes either an interpolated string or a term as input and evaluates to a term in the Lean language.

Runtime.markMultiThreaded definition

(a : α) : BaseIO α

Full source

/--
  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. -/
@[extern "lean_runtime_mark_multi_threaded"]
def Runtime.markMultiThreaded (a : α) : BaseIO α := return a

Mark value as multi-threaded

Informal description

The function `Runtime.markMultiThreaded` takes a value `a` of type `α` and marks it and its object graph closure as multi-threaded if they are currently marked as single-threaded. This operation ensures that reference counter updates become atomic, which makes them more costly but is useful when the value will be shared between threads later. The function returns the original value `a` in the `BaseIO` monad, representing an exception-free IO computation.

Runtime.markPersistent definition

(a : α) : BaseIO α

Full source

/--
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.
-/
@[extern "lean_runtime_mark_persistent"]
unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a

Mark value as persistent

Informal description

The function marks a given value and its entire object graph closure as persistent, preventing reference counter updates and deallocation until the process ends. This is safe only for objects not used concurrently or already persistent.

Runtime.forget definition

(a : α) : BaseIO Unit

Full source

/--
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.
-/
@[extern "lean_runtime_forget"]
def Runtime.forget (a : α) : BaseIO Unit := return

Discard owned reference without freeing

Informal description

The function `Runtime.forget` takes an owned reference `a` and discards it, preventing the garbage collector from freeing `a` and any objects reachable from it. This operation is safe but can be used as an optimization to avoid deallocation costs for large object graphs that would remain alive until the end of the process. The function returns the unit value `()` in the `BaseIO` monad.