Init.System.IO

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 []

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) _fun_discr = BaseIO.bindTask t (fun a => BaseIO.mapTasks.go f prio ts (a :: _fun_discr)) prio
BaseIO.mapTasks.go f prio [] _fun_discr = BaseIO.asTask (f (List.reverse _fun_discr)) prio

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

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

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

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

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))

source

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

IO α

Equations

IO.lazyPure fn = pure (fn ())

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) :

IO Unit

Equations

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

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

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

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

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

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} :

List (Task α) → IO α

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

source

opaque IO.FS.Handle:

Type

source

structure IO.FS.Stream:

Type

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

source

instance IO.FS.instInhabitedStream:

Inhabited IO.FS.Stream

Equations

IO.FS.instInhabitedStream = { default := { isEof := 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.mkPrim (fn : System.FilePath) (mode : String) :

IO IO.FS.Handle

source

def IO.FS.Handle.mk (fn : System.FilePath) (Mode : IO.FS.Mode) (bin : optParam Bool true) :

IO IO.FS.Handle

Equations

IO.FS.Handle.mk fn Mode bin = IO.FS.Handle.mkPrim fn (IO.FS.Handle.fopenFlags Mode bin)

source

@[extern lean_io_prim_handle_is_eof]

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

BaseIO Bool

Returns whether the end of the file has been reached while reading a file. h.isEof returns true /after/ the first attempt at reading past the end of h. Once h.isEof is true, reading h will always return an empty array.

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

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

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 true >>= f

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))

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

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 ""

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 true IO.FS.Handle.readBinToEnd h

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 false IO.FS.Handle.readToEnd h

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 false IO.FS.lines.read h #[]

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 true IO.FS.Handle.write h content

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 false IO.FS.Handle.putStr h content

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))

source

structure IO.FS.DirEntry:

Type

root : System.FilePath
fileName : String

source

instance IO.FS.instReprDirEntry:

Repr IO.FS.DirEntry

Equations

IO.FS.instReprDirEntry = { reprPrec := [anonymous] }

source

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

System.FilePath

Equations

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

source

inductive IO.FS.FileType:

Type

source

instance IO.FS.instReprFileType:

Repr IO.FS.FileType

Equations

IO.FS.instReprFileType = { reprPrec := [anonymous] }

source

instance IO.FS.instBEqFileType:

BEq IO.FS.FileType

Equations

IO.FS.instBEqFileType = { beq := [anonymous] }

source

structure IO.FS.SystemTime:

Type

sec : Int
nsec : UInt32

source

instance IO.FS.instReprSystemTime:

Repr IO.FS.SystemTime

Equations

IO.FS.instReprSystemTime = { reprPrec := [anonymous] }

source

instance IO.FS.instBEqSystemTime:

BEq IO.FS.SystemTime

Equations

IO.FS.instBEqSystemTime = { beq := [anonymous] }

source

instance IO.FS.instOrdSystemTime:

Ord IO.FS.SystemTime

Equations

IO.FS.instOrdSystemTime = { compare := [anonymous] }

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

source

instance IO.FS.instReprMetadata:

Repr IO.FS.Metadata

Equations

IO.FS.instReprMetadata = { reprPrec := [anonymous] }

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

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

source

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

BaseIO Bool

Equations

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

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) #[]

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)))

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)))

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)))

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)

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))

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)

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))

source

def IO.appDir:

IO System.FilePath

Equations

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

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

source

def IO.Process.Stdio.toHandleType:

IO.Process.Stdio → Type

Equations

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

source

structure IO.Process.StdioConfig:

Type

source

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

Type

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

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

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.

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.

source

@[extern lean_io_exit]

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

UInt8 → IO α

source

structure IO.AccessRight:

Type

read : Bool
write : Bool
execution : Bool

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)

source

structure IO.FileRight:

Type

source

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

UInt32

Equations

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

source

@[extern lean_chmod]

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

IO Unit

source

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

IO Unit

Equations

IO.setAccessRights filename mode = IO.Prim.setAccessRights filename (IO.FileRight.flags mode)

source

@[inline]

abbrev IO.Ref (α : Type) :

Type

Equations

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

source

instance IO.instMonadLiftSTRealWorldBaseIO:

MonadLift (ST IO.RealWorld) BaseIO

Equations

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

source

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

BaseIO (IO.Ref α)

Equations

IO.mkRef a = ST.mkRef a

source

@[export lean_stream_of_handle]

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

IO.FS.Stream

Equations

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

source

structure IO.FS.Stream.Buffer:

Type

data : ByteArray
pos : Nat

source

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

IO.FS.Stream

Equations

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

source

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

m (String × α)

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

Equations