Init.System.IO

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.

source

@[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.

source

@[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.

source

@[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.

source

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

BaseIO (Task β)

Equations

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

Instances For

source

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

Instances For

source

@[inline]

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

BaseIO (Task (Except ε α))

EIO specialization of BaseIO.asTask.

Equations

EIO.asTask act prio = BaseIO.asTask (EIO.toBaseIO act) prio

Instances For

source

@[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.

Equations

EIO.mapTask f t prio = BaseIO.mapTask (fun a => EIO.toBaseIO (f a)) t prio

Instances For

source

@[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.

Equations

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

Instances For

source

@[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.

Equations

EIO.mapTasks f tasks prio = BaseIO.mapTasks (fun as => EIO.toBaseIO (f as)) tasks prio

Instances For

source

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

IO α

Equations

IO.ofExcept e = match e with | Except.ok a => pure a | Except.error e => throw (IO.userError (toString e))

Instances For

source

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

IO α

Equations

IO.lazyPure fn = pure (fn ())

Instances For

source

@[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.

source

@[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.

source

@[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.

source

def IO.sleep (ms : UInt32) :

BaseIO Unit

Equations

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

Instances For

source

@[inline]

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

BaseIO (Task (Except IO.Error α))

IO specialization of EIO.asTask.

Equations

IO.asTask act prio = EIO.asTask act prio

Instances For

source

@[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.

Equations

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

Instances For

source

@[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.

Equations

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

Instances For

source

@[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.

Equations

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

Instances For

source

@[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.

source

@[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.

source

@[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.

source

@[extern lean_io_wait]

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

BaseIO α

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

source

@[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.

source

@[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.

source

inductive IO.FS.Mode :

Type

read: IO.FS.Mode
write: IO.FS.Mode
readWrite: IO.FS.Mode
append: IO.FS.Mode

Instances For

source

opaque IO.FS.Handle :

Type

source

structure IO.FS.Stream :

Type

flush : IO Unit
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.
read : USize → IO ByteArray
write : ByteArray → IO Unit
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.
getLine : IO String
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.

Instances For

source

instance IO.FS.instInhabitedStream :

Inhabited IO.FS.Stream

Equations

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

source

@[extern lean_get_stdin]

opaque IO.getStdin :

BaseIO IO.FS.Stream

source

@[extern lean_get_stdout]

opaque IO.getStdout :

BaseIO IO.FS.Stream

source

@[extern lean_get_stderr]

opaque IO.getStderr :

BaseIO IO.FS.Stream

source

@[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.

source

@[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.

source

@[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.

source

@[specialize #[]]

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

IO β

source

@[extern lean_io_prim_handle_mk]

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

IO IO.FS.Handle

source

@[extern lean_io_prim_handle_flush]

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

IO Unit

source

@[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.

source

@[extern lean_io_prim_handle_write]

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

IO Unit

source

@[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.

source

@[extern lean_io_prim_handle_put_str]

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

IO Unit

source

@[extern lean_io_realpath]

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

IO System.FilePath

source

@[extern lean_io_remove_file]

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

IO Unit

source

@[extern lean_io_remove_dir]

opaque IO.FS.removeDir :

System.FilePath → IO Unit

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

source

@[extern lean_io_create_dir]

opaque IO.FS.createDir :

System.FilePath → IO Unit

source

@[extern lean_io_getenv]

opaque IO.getEnv (var : String) :

BaseIO (Option String)

source

@[extern lean_io_app_path]

opaque IO.appPath :

IO System.FilePath

source

@[extern lean_io_current_dir]

opaque IO.currentDir :

IO System.FilePath

source

@[inline]

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

IO α

Equations

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

Instances For

source

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

IO Unit

Equations

IO.FS.Handle.putStrLn h s = IO.FS.Handle.putStr h (String.push s (Char.ofNat 10))

Instances For

source

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

IO ByteArray

Equations

IO.FS.Handle.readBinToEnd h = IO.FS.Handle.readBinToEnd.loop h ByteArray.empty

Instances For

source

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

IO ByteArray

source

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

IO String

Equations

IO.FS.Handle.readToEnd h = IO.FS.Handle.readToEnd.loop h ""

Instances For

source

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

IO String

source

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

IO ByteArray

Equations

IO.FS.readBinFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.Handle.readBinToEnd h

Instances For

source

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

IO String

Equations

IO.FS.readFile fname = do let h ← IO.FS.Handle.mk fname IO.FS.Mode.read IO.FS.Handle.readToEnd h

Instances For

source

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

IO (Array String)

Equations

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

Instances For

source

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

IO (Array String)

source

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

IO Unit

Equations

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

Instances For

source

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

IO Unit

Equations

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

Instances For

source

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

IO Unit

Equations

IO.FS.Stream.putStrLn strm s = IO.FS.Stream.putStr strm (String.push s (Char.ofNat 10))

Instances For

source

structure IO.FS.DirEntry :

Type

root : System.FilePath
fileName : String

Instances For

source

instance IO.FS.instReprDirEntry :

Repr IO.FS.DirEntry

Equations

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

source

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

System.FilePath

Equations

IO.FS.DirEntry.path entry = entry.root / { toString := entry.fileName }

Instances For

source

inductive IO.FS.FileType :

Type

Instances For

source

instance IO.FS.instReprFileType :

Repr IO.FS.FileType

Equations

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

source

instance IO.FS.instBEqFileType :

BEq IO.FS.FileType

Equations

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

source

structure IO.FS.SystemTime :

Type

sec : Int
nsec : UInt32

Instances For

source

instance IO.FS.instReprSystemTime :

Repr IO.FS.SystemTime

Equations

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

source

instance IO.FS.instBEqSystemTime :

BEq IO.FS.SystemTime

Equations

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

source

instance IO.FS.instOrdSystemTime :

Ord IO.FS.SystemTime

Equations

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

source

instance IO.FS.instInhabitedSystemTime :

Inhabited IO.FS.SystemTime

Equations

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

source

instance IO.FS.instLTSystemTime :

LT IO.FS.SystemTime

Equations

IO.FS.instLTSystemTime = ltOfOrd

source

instance IO.FS.instLESystemTime :

LE IO.FS.SystemTime

Equations

IO.FS.instLESystemTime = leOfOrd

source

structure IO.FS.Metadata :

Type

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

Instances For

source

instance IO.FS.instReprMetadata :

Repr IO.FS.Metadata

Equations

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

source

@[extern lean_io_read_dir]

opaque System.FilePath.readDir :

System.FilePath → IO (Array IO.FS.DirEntry)

source

@[extern lean_io_metadata]

opaque System.FilePath.metadata :

System.FilePath → IO IO.FS.Metadata

source

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

BaseIO Bool

Equations

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

Instances For

source

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

BaseIO Bool

Equations

System.FilePath.pathExists p = do let __do_lift ← EIO.toBaseIO (System.FilePath.metadata p) pure (Except.toBool __do_lift)

Instances For

source

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

IO (Array System.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.

Equations

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

Instances For

source

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

StateT (Array System.FilePath) IO Unit

source

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

m α

Equations

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

Instances For

source

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

m α

Equations

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

Instances For

source

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

m α

Equations

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

Instances For

source

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

IO Unit

Equations

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

Instances For

source

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

IO Unit

Equations

IO.println s = IO.print (String.push (toString s) (Char.ofNat 10))

Instances For

source

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

IO Unit

Equations

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

Instances For

source

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

IO Unit

Equations

IO.eprintln s = IO.eprint (String.push (toString s) (Char.ofNat 10))

Instances For

source

def IO.appDir :

IO System.FilePath

Equations

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

Instances For

source

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

IO Unit

Create given path and all missing parents as directories.

source

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

IO Unit

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

source

inductive IO.Process.Stdio :

Type

Instances For

source

def IO.Process.Stdio.toHandleType :

IO.Process.Stdio → Type

Equations

IO.Process.Stdio.toHandleType x = match x with | IO.Process.Stdio.piped => IO.FS.Handle | IO.Process.Stdio.inherit => Unit | IO.Process.Stdio.null => Unit

Instances For

source

structure IO.Process.StdioConfig :

Type

Configuration for the process' stdin handle.
stdin : IO.Process.Stdio
Configuration for the process' stdout handle.
stdout : IO.Process.Stdio
Configuration for the process' stderr handle.
stderr : IO.Process.Stdio

Instances For

source

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

Type

Command name.
cmd : String
Arguments for the process
args : Array String
Working directory for the process. Inherit from current process if none.
cwd : Option System.FilePath
Add or remove environment variables for the process.
env : Array (String × Option String)

Instances For

source

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

Instances For

source

@[extern lean_io_process_spawn]

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

IO (IO.Process.Child args.toStdioConfig)

source

@[extern lean_io_process_child_wait]

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

IO.Process.Child cfg → IO UInt32

source

@[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.

source

structure IO.Process.Output :

Type

exitCode : UInt32
stdout : String
stderr : String

Instances For

source

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

IO IO.Process.Output

Run process to completion and capture output.

Equations

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

Instances For

source

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

IO String

Run process to completion and return stdout on success.

Equations

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

Instances For

source

@[extern lean_io_exit]

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

UInt8 → IO α

source

structure IO.AccessRight :

Type

read : Bool
write : Bool
execution : Bool

Instances For

source

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

UInt32

Equations

IO.AccessRight.flags acc = let r := if acc.read = true then 4 else 0; let w := if acc.write = true then 2 else 0; let x := if acc.execution = true then 1 else 0; UInt32.lor r (UInt32.lor w x)