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

Equations

• IO.RealWorld = Unit

def EIO (ε : Type) : Type → Type

Equations

• EIO ε = EStateM ε IO.RealWorld

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• instOrElseEIO = { orElse := MonadExcept.orElse }

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

Equations

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

def BaseIO : Type → Type

An EIO monad that cannot throw exceptions.

Equations

• BaseIO = EIO Empty

instance instMonadBaseIO : Monad BaseIO

Equations

• instMonadBaseIO = inferInstanceAs (Monad (EIO Empty))

instance instMonadFinallyBaseIO : MonadFinally BaseIO

Equations

• instMonadFinallyBaseIO = inferInstanceAs (MonadFinally (EIO Empty))

@[inline]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[reducible, inline]

abbrev IO : Type → Type

Equations

• IO = EIO IO.Error

@[inline]

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

Equations

• act.toIO = liftM act

@[inline]

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

Equations

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

@[inline]

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

Equations

• act.toIO' = liftM act.toBaseIO

@[inline]

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

Equations

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

@[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 <action>] 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) (sync : optParam Bool false) : 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) (sync : optParam Bool false) : 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) (sync : optParam Bool false) : BaseIO (Task β)

Equations

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

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

Equations

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

@[inline]

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

EIO specialization of BaseIO.asTask.

Equations

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

@[inline]

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

EIO specialization of BaseIO.mapTask.

Equations

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

@[inline]

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

EIO specialization of BaseIO.bindTask.

Equations

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

@[inline]

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

EIO specialization of BaseIO.mapTasks.

Equations

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

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

Equations

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

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

Equations

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

@[extern lean_io_mono_ms_now]

opaque IO.monoMsNow : BaseIO Nat

Monotonically increasing time since an unspecified past point in milliseconds. 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

Equations

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

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

• act.asTask prio = EIO.asTask act prio

@[inline]

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

IO specialization of EIO.mapTask.

Equations

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

@[inline]

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

IO specialization of EIO.bindTask.

Equations

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

@[inline]

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

IO specialization of EIO.mapTasks.

Equations

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

@[extern lean_io_check_canceled]

opaque IO.checkCanceled : BaseIO Bool

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.

inductive IO.TaskState : Type

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

• waiting: IO.TaskState

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

• running: IO.TaskState

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

• finished: IO.TaskState

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

instance IO.instInhabitedTaskState : Inhabited IO.TaskState

Equations

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

instance IO.instReprTaskState : Repr IO.TaskState

Equations

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

instance IO.instDecidableEqTaskState : DecidableEq IO.TaskState

Equations

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

instance IO.instOrdTaskState : Ord IO.TaskState

Equations

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

instance IO.instLTTaskState : LT IO.TaskState

Equations

• IO.instLTTaskState = ltOfOrd

instance IO.instLETaskState : LE IO.TaskState

Equations

• IO.instLETaskState = leOfOrd

instance IO.instMinTaskState : Min IO.TaskState

Equations

• IO.instMinTaskState = minOfLe

instance IO.instMaxTaskState : Max IO.TaskState

Equations

• IO.instMaxTaskState = maxOfLe

def IO.TaskState.toString : IO.TaskState → String

Equations

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

instance IO.instToStringTaskState : ToString IO.TaskState

Equations

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

@[extern lean_io_get_task_state]

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

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

@[inline]

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

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

Equations

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

@[extern lean_io_wait]

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

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

@[extern lean_io_wait_any]

opaque IO.waitAny {α : Type} (tasks : List (Task α)) (h : autoParam (tasks.length > 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.

@[extern lean_io_add_heartbeats]

opaque IO.addHeartbeats (count : UInt64) : BaseIO Unit

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

inductive IO.FS.Mode : Type

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

• 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

opaque IO.FS.Handle : Type

structure IO.FS.Stream : Type

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.

• 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
• isTty : BaseIO Bool

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

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

Equations

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

@[extern lean_get_stdin]

opaque IO.getStdin : BaseIO 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_lock]

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

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

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

@[extern lean_io_prim_handle_try_lock]

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

Tries to acquire an exclusive or shared lock on the handle. Will NOT block for the lock, but instead return false.

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

@[extern lean_io_prim_handle_unlock]

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

Releases any previously acquired lock on the handle. Will succeed even if no lock has been acquired.

@[extern lean_io_prim_handle_is_tty]

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

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

@[extern lean_io_prim_handle_flush]

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

@[extern lean_io_prim_handle_rewind]

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

Rewinds the read/write cursor to the beginning of the handle.

@[extern lean_io_prim_handle_truncate]

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

Truncates the handle to the read/write cursor.

Does not automatically flush. Usually this is fine because the read/write cursor includes buffered writes. However, the combination of buffered writes, then rewind, then truncate, then close may lead to a file with content. If unsure, flush before truncating.

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

Resolves a pathname to an absolute pathname with no '.', '..', or symbolic links.

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

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

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

Creates a temporary file in the most secure manner possible. 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. The function returns both a Handle to the already opened file as well as its FilePath.

Note that it is the caller's job to remove the file after use.

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

Equations

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

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

Like createTempFile but also takes care of removing the file after usage.

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• h.readBinToEnd = h.readBinToEndInto ByteArray.empty

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

Equations

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

def IO.FS.lines (fname : Lake.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 #[]

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

Equations

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

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

Equations

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

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

Equations

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

structure IO.FS.DirEntry : Type

• root : Lake.FilePath
• fileName : String

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

structure IO.FS.SystemTime : Type

• sec : Int
• nsec : UInt32

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• IO.FS.instLTSystemTime = ltOfOrd

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

Equations

• IO.FS.instLESystemTime = leOfOrd

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

Equations

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

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

Equations

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

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

Equations

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

def System.FilePath.walkDir (p : Lake.FilePath) (enter : optParam (Lake.FilePath → IO Bool) fun (x : Lake.FilePath) => 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.

Equations

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

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

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

Equations

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

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

Equations

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

def IO.withStdin {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : 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)))

def IO.withStdout {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [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)))

def IO.withStderr {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [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)))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def IO.appDir : IO Lake.FilePath

Equations

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

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

opaque IO.Process.getCurrentDir : IO Lake.FilePath

Returns the current working directory of the calling process.

@[extern lean_io_process_set_current_dir]

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

Sets the current working directory of the calling process.

@[extern lean_io_process_get_pid]

opaque IO.Process.getPID : BaseIO UInt32

Returns the process ID of the calling process.

inductive IO.Process.Stdio : Type

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

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

Equations

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

structure IO.Process.StdioConfig : Type

• 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 : cfg.stdin.toHandleType
• stdout : cfg.stdout.toHandleType
• stderr : cfg.stderr.toHandleType

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

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

@[extern lean_io_process_child_try_wait]

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

Check whether the child has exited yet. If it hasn't return none, otherwise its exit code.

@[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 (cfg.stdin.toHandleType × 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. The process does not inherit the standard input of the caller.

Equations

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

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.

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

Equations

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

structure IO.FileRight : Type

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

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

Equations

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

@[extern lean_chmod]

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

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

Equations

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

@[reducible, inline]

abbrev IO.Ref (α : Type) : Type

References

Equations

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

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

Equations

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

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

Equations

• IO.mkRef a = ST.mkRef a

structure IO.CancelToken : Type

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

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

• ref : IO.Ref Bool

def IO.CancelToken.new : BaseIO IO.CancelToken

Creates a new cancellation token.

Equations

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

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

Activates a cancellation token. Idempotent.

Equations

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

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

Checks whether the cancellation token has been activated.

Equations

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

@[export lean_stream_of_handle]

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

Equations

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

structure IO.FS.Stream.Buffer : Type

• data : ByteArray
• pos : Nat

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.

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.

Equations

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

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

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

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

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

Equations

• Lean.instEval = { eval := fun (a : Unit → α) (x : optParam Bool true) => IO.println (toString (a ())) }

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

Equations

• Lean.instEvalOfRepr = { eval := fun (a : Unit → α) (x : optParam Bool true) => IO.println (repr (a ())) }

instance Lean.instEvalUnit : Lean.Eval Unit

Equations

• Lean.instEvalUnit = { eval := fun (u : Unit → Unit) (hideUnit : optParam Bool true) => if hideUnit = true then pure () else IO.println (repr (u ())) }

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

Equations

• Lean.instEvalIO = { eval := fun (x : Unit → IO α) (x_1 : optParam Bool true) => do let a ← x () Lean.Eval.eval fun (x : Unit) => a }

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

Equations

• Lean.instEvalBaseIO = { eval := fun (x : Unit → BaseIO α) (x_1 : optParam Bool true) => do let a ← liftM (x ()) Lean.Eval.eval fun (x : Unit) => a }

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

Equations

• Lean.runEval a = IO.FS.withIsolatedStreams (liftM (EIO.toBaseIO (Lean.Eval.eval a false)))

def termPrintln!__ : Lean.ParserDescr

Equations

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