Documentation

Init.System.IOError

source
inductive IO.Error :
Type

Exceptions that may be thrown in the IO monad.

Many of the constructors of IO.Error correspond to POSIX error numbers. In these cases, the documentation string lists POSIX standard error macros that correspond to the error. This list is not necessarily exhaustive, and these constructor includes a field for the underlying error number.

  • alreadyExists (filename : Option String) (osCode : UInt32) (details : String) : Error

    The operation failed because a file already exists.

    This corresponds to POSIX errors EEXIST, EINPROGRESS, and EISCONN.

  • otherError (osCode : UInt32) (details : String) : Error

    Some error not covered by the other constructors of IO.Error occurred.

    This also includes POSIX error EFAULT.

  • resourceBusy (osCode : UInt32) (details : String) : Error

    A necessary resource was busy.

    This corresponds to POSIX errors EADDRINUSE, EBUSY, EDEADLK, and ETXTBSY.

  • resourceVanished (osCode : UInt32) (details : String) : Error

    A necessary resource is no longer available.

    This corresponds to POSIX errors ECONNRESET, EIDRM, ENETDOWN, ENETRESET, ENOLINK, and EPIPE.

  • unsupportedOperation (osCode : UInt32) (details : String) : Error

    An operation was not supported.

    This corresponds to POSIX errors EADDRNOTAVAIL, EAFNOSUPPORT, ENODEV, ENOPROTOOPT ENOSYS, EOPNOTSUPP, ERANGE, ESPIPE, and EXDEV.

  • hardwareFault (osCode : UInt32) (details : String) : Error

    The operation failed due to a hardware problem, such as an I/O error.

    This corresponds to the POSIX error EIO.

  • unsatisfiedConstraints (osCode : UInt32) (details : String) : Error

    A constraint required by an operation was not satisfied (e.g. a directory was not empty).

    This corresponds to the POSIX error ENOTEMPTY.

  • illegalOperation (osCode : UInt32) (details : String) : Error

    An inappropriate I/O control operation was attempted.

    This corresponds to the POSIX error ENOTTY.

  • protocolError (osCode : UInt32) (details : String) : Error

    A protocol error occurred.

    This corresponds to the POSIX errors EPROTO, EPROTONOSUPPORT, and EPROTOTYPE.

  • timeExpired (osCode : UInt32) (details : String) : Error

    An operation timed out.

    This corresponds to the POSIX errors ETIME, and ETIMEDOUT.

  • interrupted (filename : String) (osCode : UInt32) (details : String) : Error

    The operation was interrupted.

    This corresponds to the POSIX error EINTR.

  • noFileOrDirectory (filename : String) (osCode : UInt32) (details : String) : Error

    No such file or directory.

    This corresponds to the POSIX error ENOENT.

  • invalidArgument (filename : Option String) (osCode : UInt32) (details : String) : Error

    An argument to an I/O operation was invalid.

    This corresponds to the POSIX errors ELOOP, ENAMETOOLONG, EDESTADDRREQ, EILSEQ, EINVAL, EDOM, EBADF ENOEXEC, ENOSTR, ENOTCONN, and ENOTSOCK.

  • permissionDenied (filename : Option String) (osCode : UInt32) (details : String) : Error

    An operation failed due to insufficient permissions.

    This corresponds to the POSIX errors EACCES, EROFS, ECONNABORTED, EFBIG, and EPERM.

  • resourceExhausted (filename : Option String) (osCode : UInt32) (details : String) : Error

    A resource was exhausted.

    This corresponds to the POSIX errors EMFILE, ENFILE, ENOSPC, E2BIG, EAGAIN, EMLINK, EMSGSIZE, ENOBUFS, ENOLCK, ENOMEM, and ENOSR.

  • inappropriateType (filename : Option String) (osCode : UInt32) (details : String) : Error

    An argument was the wrong type (e.g. a directory when a file was required).

    This corresponds to the POSIX errors EISDIR, EBADMSG, and ENOTDIR.

  • noSuchThing (filename : Option String) (osCode : UInt32) (details : String) : Error

    A required resource does not exist.

    This corresponds to the POSIX errors ENXIO, EHOSTUNREACH, ENETUNREACH, ECHILD, ECONNREFUSED, ENODATA, ENOMSG, and ESRCH.

  • unexpectedEof : Error

    An unexpected end-of-file marker was encountered.

  • userError (msg : String) : Error

    Some other error occurred.

Instances For
source
instance instInhabitedError :
Inhabited IO.Error
Equations
source
@[export lean_mk_io_user_error]
def IO.userError (s : String) :
Error

Constructs an IO.Error from a string.

IO.Error is the type of exceptions thrown by the IO monad.

Equations
source
instance instCoeStringError :
Coe String IO.Error
Equations
source
@[export lean_mk_io_error_already_exists_file]
def IO.Error.mkAlreadyExistsFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_eof]
def IO.Error.mkEofError :
Unit → Error
Equations
source
@[export lean_mk_io_error_inappropriate_type_file]
def IO.Error.mkInappropriateTypeFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_interrupted]
def IO.Error.mkInterrupted :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_invalid_argument_file]
def IO.Error.mkInvalidArgumentFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_no_file_or_directory]
def IO.Error.mkNoFileOrDirectory :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_no_such_thing_file]
def IO.Error.mkNoSuchThingFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_permission_denied_file]
def IO.Error.mkPermissionDeniedFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_resource_exhausted_file]
def IO.Error.mkResourceExhaustedFile :
String → UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_unsupported_operation]
def IO.Error.mkUnsupportedOperation :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_resource_exhausted]
def IO.Error.mkResourceExhausted :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_already_exists]
def IO.Error.mkAlreadyExists :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_inappropriate_type]
def IO.Error.mkInappropriateType :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_no_such_thing]
def IO.Error.mkNoSuchThing :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_resource_vanished]
def IO.Error.mkResourceVanished :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_resource_busy]
def IO.Error.mkResourceBusy :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_invalid_argument]
def IO.Error.mkInvalidArgument :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_other_error]
def IO.Error.mkOtherError :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_permission_denied]
def IO.Error.mkPermissionDenied :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_hardware_fault]
def IO.Error.mkHardwareFault :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_unsatisfied_constraints]
def IO.Error.mkUnsatisfiedConstraints :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_illegal_operation]
def IO.Error.mkIllegalOperation :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_protocol_error]
def IO.Error.mkProtocolError :
UInt32 → String → Error
Equations
source
@[export lean_mk_io_error_time_expired]
def IO.Error.mkTimeExpired :
UInt32 → String → Error
Equations
source
def IO.Error.fopenErrorToString (gist fn : String) (code : UInt32) :
Option String → String
Equations
source
def IO.Error.otherErrorToString (gist : String) (code : UInt32) :
Option String → String
Equations
source
@[export lean_io_error_to_string]
def IO.Error.toString :
Error → String

Converts an IO.Error to a descriptive string.

IO.Error.userError is converted to its embedded message. The other constructors are converted in a way that preserves structured information, such as error codes and filenames, that can help diagnose the issue.

Equations
source
instance IO.Error.instToString :
ToString Error
Equations