Documentation

Init.System.IO

Like . Makes sure we never reorder IO operations.

TODO: mark opaque

Equations
Instances For
    def EIO (ε : Type) :
    Equations
    Instances For
      instance instMonadEIO {ε : Type} :
      Monad (EIO ε)
      Equations
      Equations
      instance instMonadExceptOfEIO {ε : Type} :
      Equations
      instance instOrElseEIO {ε : Type} {α : Type} :
      OrElse (EIO ε α)
      Equations
      • instOrElseEIO = { orElse := MonadExcept.orElse }
      instance instInhabitedEIO {ε : Type} {α : Type} [Inhabited ε] :
      Inhabited (EIO ε α)
      Equations
      def BaseIO :

      An EIO monad that cannot throw exceptions.

      Equations
      Instances For
        @[inline]
        def BaseIO.toEIO {α : Type} {ε : Type} (act : BaseIO α) :
        EIO ε α
        Equations
        Instances For
          Equations
          • instMonadLiftBaseIOEIO = { monadLift := fun {α : Type} => BaseIO.toEIO }
          @[inline]
          def EIO.toBaseIO {ε : Type} {α : Type} (act : EIO ε α) :
          BaseIO (Except ε α)
          Equations
          Instances For
            @[inline]
            def EIO.catchExceptions {ε : Type} {α : Type} (act : EIO ε α) (h : εBaseIO α) :
            Equations
            Instances For
              @[inline, reducible]
              abbrev IO :
              Equations
              Instances For
                @[inline]
                def BaseIO.toIO {α : Type} (act : BaseIO α) :
                IO α
                Equations
                Instances For
                  @[inline]
                  def EIO.toIO {ε : Type} {α : Type} (f : εIO.Error) (act : EIO ε α) :
                  IO α
                  Equations
                  Instances For
                    @[inline]
                    def EIO.toIO' {ε : Type} {α : Type} (act : EIO ε α) :
                    IO (Except ε α)
                    Equations
                    Instances For
                      @[inline]
                      def IO.toEIO {ε : Type} {α : Type} (f : IO.Errorε) (act : IO α) :
                      EIO ε α
                      Equations
                      Instances For
                        @[inline]
                        unsafe def unsafeBaseIO {α : Type} (fn : BaseIO α) :
                        α
                        Equations
                        Instances For
                          @[inline]
                          unsafe def unsafeEIO {ε : Type} {α : Type} (fn : EIO ε α) :
                          Except ε α
                          Equations
                          Instances For
                            @[inline]
                            unsafe def unsafeIO {α : Type} (fn : IO α) :
                            Equations
                            Instances For
                              @[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]

                              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]

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

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

                              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) :
                              Equations
                              Instances For
                                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
                                Instances For
                                  @[inline]
                                  def EIO.asTask {ε : Type} {α : Type} (act : EIO ε α) (prio : optParam Task.Priority Task.Priority.default) :
                                  BaseIO (Task (Except ε α))

                                  EIO specialization of BaseIO.asTask.

                                  Equations
                                  Instances For
                                    @[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
                                    Instances For
                                      @[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
                                      Instances For
                                        @[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
                                        Instances For
                                          def IO.ofExcept {ε : Type u_1} {α : Type} [ToString ε] (e : Except ε α) :
                                          IO α
                                          Equations
                                          Instances For
                                            def IO.lazyPure {α : Type} (fn : Unitα) :
                                            IO α
                                            Equations
                                            Instances For
                                              @[extern lean_io_mono_ms_now]

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

                                              @[extern lean_io_mono_nanos_now]

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

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

                                              Equations
                                              Instances For
                                                @[inline]

                                                IO specialization of EIO.asTask.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def IO.mapTask {α : Type u_1} {β : Type} (f : αIO β) (t : Task α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                  IO specialization of EIO.mapTask.

                                                  Equations
                                                  Instances For
                                                    @[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) :

                                                    IO specialization of EIO.bindTask.

                                                    Equations
                                                    Instances For
                                                      @[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) :

                                                      IO specialization of EIO.mapTasks.

                                                      Equations
                                                      Instances For
                                                        @[extern lean_io_check_canceled]

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

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

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

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

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

                                                        @[extern lean_io_get_num_heartbeats]

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

                                                        inductive IO.FS.Mode :

                                                        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:

                                                        • 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
                                                        Instances For
                                                          structure IO.FS.Stream :

                                                          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 : USizeIO 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 : ByteArrayIO 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 : StringIO Unit
                                                          Instances For
                                                            Equations
                                                            • IO.FS.instInhabitedStream = { default := { flush := default, read := default, write := default, getLine := default, putStr := default } }
                                                            @[extern lean_get_stdin]
                                                            @[extern lean_get_stdout]
                                                            @[extern lean_get_stderr]
                                                            @[extern lean_get_set_stdin]

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

                                                            @[extern lean_get_set_stdout]

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

                                                            @[extern lean_get_set_stderr]

                                                            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]
                                                            @[extern lean_io_prim_handle_lock]
                                                            opaque IO.FS.Handle.lock (h : IO.FS.Handle) (exclusive : optParam Bool true) :

                                                            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]

                                                            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]

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

                                                            @[extern lean_io_prim_handle_flush]
                                                            @[extern lean_io_prim_handle_rewind]

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

                                                            @[extern lean_io_prim_handle_truncate]

                                                            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]

                                                            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]
                                                            @[extern lean_io_prim_handle_get_line]

                                                            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]
                                                            @[extern lean_io_realpath]
                                                            @[extern lean_io_remove_file]
                                                            @[extern lean_io_remove_dir]

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

                                                            @[extern lean_io_create_dir]
                                                            @[extern lean_io_rename]

                                                            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) :
                                                            @[extern lean_io_app_path]
                                                            @[extern lean_io_current_dir]
                                                            @[inline]
                                                            def IO.FS.withFile {α : Type} (fn : Lake.FilePath) (mode : IO.FS.Mode) (f : IO.FS.HandleIO α) :
                                                            IO α
                                                            Equations
                                                            Instances For
                                                              Equations
                                                              Instances For
                                                                def IO.FS.writeBinFile (fname : Lake.FilePath) (content : ByteArray) :
                                                                Equations
                                                                Instances For
                                                                  def IO.FS.writeFile (fname : Lake.FilePath) (content : String) :
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    Instances For
                                                                      structure IO.FS.DirEntry :
                                                                      Instances For
                                                                        Equations
                                                                        Instances For
                                                                          Instances For
                                                                            Equations
                                                                            structure IO.FS.Metadata :
                                                                            Instances For
                                                                              @[extern lean_io_read_dir]
                                                                              @[extern lean_io_metadata]
                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                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
                                                                                Instances For
                                                                                  def IO.withStdin {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                  m α
                                                                                  Equations
                                                                                  Instances For
                                                                                    def IO.withStdout {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                    m α
                                                                                    Equations
                                                                                    Instances For
                                                                                      def IO.withStderr {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                      m α
                                                                                      Equations
                                                                                      Instances For
                                                                                        def IO.print {α : Type u_1} [ToString α] (s : α) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          def IO.println {α : Type u_1} [ToString α] (s : α) :
                                                                                          Equations
                                                                                          Instances For
                                                                                            def IO.eprint {α : Type u_1} [ToString α] (s : α) :
                                                                                            Equations
                                                                                            Instances For
                                                                                              def IO.eprintln {α : Type u_1} [ToString α] (s : α) :
                                                                                              Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For

                                                                                                  Create given path and all missing parents as directories.

                                                                                                  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]

                                                                                                  Returns the process ID of the current process.

                                                                                                  Instances For
                                                                                                    Instances For
                                                                                                      Instances For
                                                                                                        @[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]
                                                                                                        @[extern lean_io_process_child_kill]

                                                                                                        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 cfgIO (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.

                                                                                                        Instances For

                                                                                                          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.
                                                                                                          Instances For

                                                                                                            Run process to completion and return stdout on success.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              @[extern lean_io_exit]
                                                                                                              opaque IO.Process.exit {α : Type} :
                                                                                                              UInt8IO α
                                                                                                              structure IO.AccessRight :
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  structure IO.FileRight :
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      @[extern lean_chmod]
                                                                                                                      opaque IO.Prim.setAccessRights (filename : Lake.FilePath) (mode : UInt32) :
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[inline, reducible]
                                                                                                                        abbrev IO.Ref (α : Type) :

                                                                                                                        References

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def IO.mkRef {α : Type} (a : α) :
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[export lean_stream_of_handle]
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  def IO.FS.withIsolatedStreams {m : TypeType 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.
                                                                                                                                  Instances For
                                                                                                                                    class Lean.Eval (α : Type u) :

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

                                                                                                                                    Instances
                                                                                                                                      instance Lean.instEval {α : Type u_1} [ToString α] :
                                                                                                                                      Equations
                                                                                                                                      instance Lean.instEval_1 {α : Type u_1} [Repr α] :
                                                                                                                                      Equations
                                                                                                                                      Equations
                                                                                                                                      instance Lean.instEvalIO {α : Type} [Lean.Eval α] :
                                                                                                                                      Equations
                                                                                                                                      Equations
                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For