def IO.RealWorld : Type

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 EIO (ε : Type) : Type → Type

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

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

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

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

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

def BaseIO : Type → Type

An EIO monad that cannot throw exceptions.

instance instMonadBaseIO : Monad BaseIO

instance instMonadFinallyBaseIO : MonadFinally BaseIO

@[inline]

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

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

@[inline]

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

@[inline]

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

@[inline, reducible]

abbrev IO : Type → Type

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[extern lean_io_timeit]

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

@[extern lean_io_allocprof]

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

@[extern lean_io_initializing]

opaque IO.initializing : BaseIO Bool

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

The action initializing returns true iff it is invoked during initialization.

@[extern lean_io_as_task]

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

Run act in a separate Task. This is similar to Haskell's unsafeInterleaveIO, except that the Task is started eagerly as usual. Thus pure accesses to the Task do not influence the impure act computation. Unlike with pure tasks created by Task.spawn, tasks created by this function will be run even if the last reference to the task is dropped. The act should manually check for cancellation via IO.checkCanceled if it wants to react to that.

@[extern lean_io_map_task]

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

See BaseIO.asTask.

@[extern lean_io_bind_task]

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

See BaseIO.asTask.

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

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

Equations

• BaseIO.mapTasks.go f prio (t :: ts) x = BaseIO.bindTask t (fun a => BaseIO.mapTasks.go f prio ts (a :: x)) prio
• BaseIO.mapTasks.go f prio [] x = BaseIO.asTask (f (List.reverse x)) prio

@[inline]

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

EIO specialization of BaseIO.asTask.

@[inline]

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

EIO specialization of BaseIO.mapTask.

@[inline]

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

EIO specialization of BaseIO.bindTask.

@[inline]

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

EIO specialization of BaseIO.mapTasks.

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

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

@[extern lean_io_mono_ms_now]

opaque IO.monoMsNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time.

@[extern lean_io_mono_nanos_now]

opaque IO.monoNanosNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time.

@[extern lean_io_get_random_bytes]

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

Read bytes from a system entropy source. Not guaranteed to be cryptographically secure. If nBytes = 0, return immediately with an empty buffer.

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

@[inline]

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

IO specialization of EIO.asTask.

@[inline]

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

IO specialization of EIO.mapTask.

@[inline]

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

IO specialization of EIO.bindTask.

@[inline]

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

IO specialization of EIO.mapTasks.

@[extern lean_io_check_canceled]

opaque IO.checkCanceled : BaseIO Bool

Check if the task's cancellation flag has been set by calling IO.cancel or dropping the last reference to the task.

@[extern lean_io_cancel]

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

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

@[extern lean_io_has_finished]

opaque IO.hasFinished {α : Type u_1} : Task α → BaseIO Bool

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

@[extern lean_io_wait]

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

Wait for the task to finish, then return its result.

@[extern lean_io_wait_any]

opaque IO.waitAny {α : Type} (tasks : List (Task α)) (h : autoParam (List.length tasks > 0) _auto✝) : BaseIO α

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

@[extern lean_io_get_num_heartbeats]

opaque IO.getNumHeartbeats : BaseIO Nat

Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread.

inductive IO.FS.Mode : Type

• read: IO.FS.Mode

  File opened for reading. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

  • open flags: O_RDONLY
  • fdopen mode: r
• write: IO.FS.Mode

  File opened for writing. On open, truncate an existing file to zero length or create a new file. The stream is positioned at the beginning of the file.

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

  New file opened for writing. On open, create a new file with the stream positioned at the start. Errors if the file already exists.

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

  File opened for reading and writing. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

  • open flags: O_RDWR
  • fdopen mode: r+
• append: IO.FS.Mode

  File opened for writing. On open, create a new file if it does not exist. The stream is positioned at the end of the file.

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

The mode of a file handle (i.e., a set of open flags and an fdopen mode).

All modes do not translate line endings (i.e., O_BINARY on Windows) and are not inherited across process creation (i.e., O_NOINHERIT on Windows, O_CLOEXEC elsewhere).

References:

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

opaque IO.FS.Handle : Type

structure IO.FS.Stream : Type

• flush : IO Unit
• read : USize → IO ByteArray

  Read up to the given number of bytes from the stream. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

• write : ByteArray → IO Unit
• getLine : IO String

  Read text up to (including) the next line break from the stream. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

• putStr : String → IO Unit

A pure-Lean abstraction of POSIX streams. We use Streams for the standard streams stdin/stdout/stderr so we can capture output of #eval commands into memory.

instance IO.FS.instInhabitedStream : Inhabited IO.FS.Stream

@[extern lean_get_stdin]

opaque IO.getStdin : BaseIO IO.FS.Stream

@[extern lean_get_stdout]

opaque IO.getStdout : BaseIO IO.FS.Stream

@[extern lean_get_stderr]

opaque IO.getStderr : BaseIO IO.FS.Stream

@[extern lean_get_set_stdin]

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

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

@[extern lean_get_set_stdout]

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

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

@[extern lean_get_set_stderr]

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

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

@[specialize #[]]

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

@[extern lean_io_prim_handle_mk]

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

@[extern lean_io_prim_handle_flush]

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

@[extern lean_io_prim_handle_read]

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

Read up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

@[extern lean_io_prim_handle_write]

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

@[extern lean_io_prim_handle_get_line]

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

Read text up to (including) the next line break from the handle. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

@[extern lean_io_prim_handle_put_str]

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

@[extern lean_io_realpath]

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

@[extern lean_io_remove_file]

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

@[extern lean_io_remove_dir]

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

Remove given directory. Fails if not empty; see also IO.FS.removeDirAll.

@[extern lean_io_create_dir]

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

@[extern lean_io_rename]

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

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

This function coincides with the POSIX rename function, see there for more information.

@[extern lean_io_getenv]

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

@[extern lean_io_app_path]

opaque IO.appPath : IO Lake.FilePath

@[extern lean_io_current_dir]

opaque IO.currentDir : IO Lake.FilePath

@[inline]

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

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

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

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

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

partial def IO.FS.Handle.readToEnd.loop (h : IO.FS.Handle) (s : String) : IO String

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

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

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

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

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

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

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

structure IO.FS.DirEntry : Type

• root : Lake.FilePath
• fileName : String

instance IO.FS.instReprDirEntry : Repr IO.FS.DirEntry

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

inductive IO.FS.FileType : Type

• dir: IO.FS.FileType
• file: IO.FS.FileType
• symlink: IO.FS.FileType
• other: IO.FS.FileType

instance IO.FS.instReprFileType : Repr IO.FS.FileType

instance IO.FS.instBEqFileType : BEq IO.FS.FileType

structure IO.FS.SystemTime : Type

• sec : Int
• nsec : UInt32

instance IO.FS.instReprSystemTime : Repr IO.FS.SystemTime

instance IO.FS.instBEqSystemTime : BEq IO.FS.SystemTime

instance IO.FS.instOrdSystemTime : Ord IO.FS.SystemTime

instance IO.FS.instInhabitedSystemTime : Inhabited IO.FS.SystemTime

instance IO.FS.instLTSystemTime : LT IO.FS.SystemTime

instance IO.FS.instLESystemTime : LE IO.FS.SystemTime

structure IO.FS.Metadata : Type

• accessed : IO.FS.SystemTime
• modified : IO.FS.SystemTime
• byteSize : UInt64
• type : IO.FS.FileType

instance IO.FS.instReprMetadata : Repr IO.FS.Metadata

@[extern lean_io_read_dir]

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

@[extern lean_io_metadata]

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

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

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

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

Return all filesystem entries of a preorder traversal of all directories satisfying enter, starting at p. Symbolic links are visited as well by default.

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

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

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

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

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

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

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

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

def IO.appDir : IO Lake.FilePath

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

Create given path and all missing parents as directories.

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

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

@[extern lean_io_process_get_pid]

opaque IO.Process.getPID : BaseIO UInt32

Returns the process ID of the current process.

inductive IO.Process.Stdio : Type

• piped: IO.Process.Stdio
• inherit: IO.Process.Stdio
• null: IO.Process.Stdio

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

structure IO.Process.StdioConfig : Type

• stdin : IO.Process.Stdio

  Configuration for the process' stdin handle.

• stdout : IO.Process.Stdio

  Configuration for the process' stdout handle.

• stderr : IO.Process.Stdio

  Configuration for the process' stderr handle.

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

• stdin : IO.Process.Stdio
• stdout : IO.Process.Stdio
• stderr : IO.Process.Stdio
• cmd : String

  Command name.

• args : Array String

  Arguments for the process

• cwd : Option Lake.FilePath

  Working directory for the process. Inherit from current process if none.

• env : Array (String × Option String)

  Add or remove environment variables for the process.

• setsid : Bool

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

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

• stdin : IO.Process.Stdio.toHandleType cfg.stdin
• stdout : IO.Process.Stdio.toHandleType cfg.stdout
• stderr : IO.Process.Stdio.toHandleType cfg.stderr

@[extern lean_io_process_spawn]

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

@[extern lean_io_process_child_wait]

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

@[extern lean_io_process_child_kill]

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

Terminates the child process using the SIGTERM signal or a platform analogue. If the process was started using SpawnArgs.setsid, terminates the entire process group instead.

@[extern lean_io_process_child_take_stdin]

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

Extract the stdin field from a Child object, allowing them to be freed independently. This operation is necessary for closing the child process' stdin while still holding on to a process handle, e.g. for Child.wait. A file handle is closed when all references to it are dropped, which without this operation includes the Child object.

structure IO.Process.Output : Type

• exitCode : UInt32
• stdout : String
• stderr : String

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

Run process to completion and capture output.

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

Run process to completion and return stdout on success.

@[extern lean_io_exit]

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

structure IO.AccessRight : Type

• read : Bool
• write : Bool
• execution : Bool

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

structure IO.FileRight : Type

• user : IO.AccessRight
• group : IO.AccessRight
• other : IO.AccessRight

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

@[extern lean_chmod]

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

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

@[inline, reducible]

abbrev IO.Ref (α : Type) : Type

References

instance IO.instMonadLiftSTRealWorldBaseIO : MonadLift (ST IO.RealWorld) BaseIO

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

@[export lean_stream_of_handle]

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

structure IO.FS.Stream.Buffer : Type

• data : ByteArray
• pos : Nat

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

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

Run action with stdin emptied and stdout+stderr captured into a String.

class Lean.Eval (α : Type u) : Type u

• eval : (Unit → α) → optParam Bool true → IO Unit

Typeclass used for presenting the output of an #eval command.

instance Lean.instEval {α : Type u_1} [ToString α] : Lean.Eval α

instance Lean.instEval_1 {α : Type u_1} [Repr α] : Lean.Eval α

instance Lean.instEvalUnit : Lean.Eval Unit

instance Lean.instEvalIO {α : Type} [Lean.Eval α] : Lean.Eval (IO α)

instance Lean.instEvalBaseIO {α : Type} [Lean.Eval α] : Lean.Eval (BaseIO α)

def Lean.runEval {α : Type u_1} [Lean.Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit)

def termPrintln!__ : Lean.ParserDescr