diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index 8cf02559fa57..b38949217ccf 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -7,11 +7,15 @@ module prelude -public import Init.System.IO -- for `MonoBind` instance -import all Init.Control.Except -- for `MonoBind` instance -import all Init.Control.StateRef -- for `MonoBind` instance -import all Init.Control.Option -- for `MonoBind` instance -import all Init.System.ST -- for `MonoBind` instance +public import Init.System.IO +public import Init.Control.StateRef +public import Init.Control.Option +import Init.Control.Except +import all Init.Control.StateRef +import all Init.System.ST +import Init.RCases +import Init.ByCases + public section diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean index 809db9f7599a..9e35e1dd63ff 100644 --- a/src/Init/Internal/Order/Lemmas.lean +++ b/src/Init/Internal/Order/Lemmas.lean @@ -8,10 +8,11 @@ module prelude +public import Init.Internal.Order.Basic +public import Init.Control.Lawful.Basic +public import Init.Data.List.Control import all Init.Data.List.Control -import all Init.Data.Option.Basic import all Init.Data.Array.Basic -public import Init.Internal.Order.Basic public section diff --git a/src/Init/System.lean b/src/Init/System.lean index f1bf8963c0e7..5593895be343 100644 --- a/src/Init/System.lean +++ b/src/Init/System.lean @@ -10,3 +10,4 @@ public import Init.System.IO public import Init.System.Platform public import Init.System.Uri public import Init.System.Promise +public import Init.System.Files diff --git a/src/Init/System/Files.lean b/src/Init/System/Files.lean new file mode 100644 index 000000000000..897c2ef3d057 --- /dev/null +++ b/src/Init/System/Files.lean @@ -0,0 +1,1237 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone, Henrik Böving +-/ +module + +prelude +public import Init.System.IO +public import Init.Data.Ord.UInt +public import Init.System.FilePath +import Init.Data.String.TakeDrop +import Init.Data.String.Search + +public section + +open System + +namespace IO + +/-- +Whether a file should be opened for reading, writing, creation and writing, or appending. + +At the operating system level, this translates to the mode of a file handle (i.e., a set of `open` +flags and an `fdopen` mode). + +None of the modes represented by this datatype translate line endings (i.e. `O_BINARY` on Windows). +Furthermore, they are not inherited across process creation (i.e. `O_NOINHERIT` on Windows and +`O_CLOEXEC` elsewhere). + +**Operating System Specifics:** +* Windows: + [`_open`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/open-wopen?view=msvc-170), + [`_fdopen`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fdopen-wfdopen?view=msvc-170) +* Linux: [`open`](https://linux.die.net/man/2/open), [`fdopen`](https://linux.die.net/man/3/fdopen) +-/ +inductive FS.Mode where + /-- + The file should be opened for reading. + + The read/write cursor is positioned at the beginning of the file. It is an error if the file does + not exist. + + * `open` flags: `O_RDONLY` + * `fdopen` mode: `r` + -/ + | read + /-- + The file should be opened for writing. + + If the file already exists, it is truncated to zero length. Otherwise, a new file is created. The + read/write cursor is positioned at the beginning of the file. + + * `open` flags: `O_WRONLY | O_CREAT | O_TRUNC` + * `fdopen` mode: `w` + -/ + | write + /-- + A new file should be created for writing. + + It is an error if the file already exists. A new file is created, with the read/write cursor + positioned at the start. + + * `open` flags: `O_WRONLY | O_CREAT | O_TRUNC | O_EXCL` + * `fdopen` mode: `w` + -/ + | writeNew + /-- + The file should be opened for both reading and writing. + + It is an error if the file does not already exist. The read/write cursor is positioned at the + start of the file. + + * `open` flags: `O_RDWR` + * `fdopen` mode: `r+` + -/ + | readWrite + /-- + The file should be opened for writing. + + If the file does not already exist, it is created. If the file already exists, it is opened, and + the read/write cursor is positioned at the end of the file. + + * `open` flags: `O_WRONLY | O_CREAT | O_APPEND` + * `fdopen` mode: `a` + -/ + | append + +/-- +A reference to an opened file. + +File handles wrap the underlying operating system's file descriptors. There is no explicit operation +to close a file: when the last reference to a file handle is dropped, the file is closed +automatically. + +Handles have an associated read/write cursor that determines the where reads and writes occur in the +file. +-/ +opaque FS.Handle : Type := Unit + +/-- +A pure-Lean abstraction of POSIX streams. These streams may represent an underlying POSIX stream or +be implemented by Lean code. + +Because standard input, standard output, and standard error are all `IO.FS.Stream`s that can be +overridden, Lean code may capture and redirect input and output. +-/ +structure FS.Stream where + /-- + Flushes the stream's output buffers. + -/ + flush : IO Unit + /-- + Reads up to the given number of bytes from the stream. + + If the returned array is empty, an end-of-file marker (EOF) has been reached. An EOF does not + actually close a stream, so further reads may block and return more data. + -/ + read : USize → IO ByteArray + /-- + Writes the provided bytes to the stream. + + If the stream represents a physical output device such as a file on disk, then the results may be + buffered. Call `FS.Stream.flush` to synchronize their contents. + -/ + write : ByteArray → IO Unit + /-- + Reads text up to and including the next newline from the stream. + + If the returned string is empty, an end-of-file marker (EOF) has been reached. + An EOF does not actually close a stream, so further reads may block and return more data. + -/ + getLine : IO String + /-- + Writes the provided string to the stream. + -/ + putStr : String → IO Unit + /-- Returns `true` if a stream refers to a Windows console or Unix terminal. -/ + isTty : BaseIO Bool + deriving Inhabited + +open FS + +/-- +Returns the current thread's standard input stream. + +Use `IO.setStdin` to replace the current thread's standard input stream. +-/ +@[extern "lean_get_stdin"] opaque getStdin : BaseIO FS.Stream +/-- +Returns the current thread's standard output stream. + +Use `IO.setStdout` to replace the current thread's standard output stream. +-/ +@[extern "lean_get_stdout"] opaque getStdout : BaseIO FS.Stream +/-- +Returns the current thread's standard error stream. + +Use `IO.setStderr` to replace the current thread's standard error stream. +-/ +@[extern "lean_get_stderr"] opaque getStderr : BaseIO FS.Stream + +/-- +Replaces the standard input stream of the current thread and returns its previous value. + +Use `IO.getStdin` to get the current standard input stream. +-/ +@[extern "lean_get_set_stdin"] opaque setStdin : FS.Stream → BaseIO FS.Stream +/-- +Replaces the standard output stream of the current thread and returns its previous value. + +Use `IO.getStdout` to get the current standard output stream. +-/ +@[extern "lean_get_set_stdout"] opaque setStdout : FS.Stream → BaseIO FS.Stream +/-- +Replaces the standard error stream of the current thread and returns its previous value. + +Use `IO.getStderr` to get the current standard error stream. +-/ +@[extern "lean_get_set_stderr"] opaque setStderr : FS.Stream → BaseIO FS.Stream + +/-- +Iterates an `IO` action. Starting with an initial state, the action is applied repeatedly until it +returns a final value in `Sum.inr`. Each time it returns `Sum.inl`, the returned value is treated as +a new state. +-/ +@[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do + let v ← f a + match v with + | Sum.inl a => iterate a f + | Sum.inr b => pure b + +namespace FS + +namespace Handle + +/-- +Opens the file at `fn` with the given `mode`. + +An exception is thrown if the file cannot be opened. +-/ +@[extern "lean_io_prim_handle_mk"] opaque mk (fn : @& FilePath) (mode : FS.Mode) : IO Handle + +/-- +Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary. + +Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it +works on Unix-like systems but not on Windows. +-/ +@[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit +/-- +Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will +not block if the lock cannot be acquired, but instead returns `false`. + +Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it +works on Unix-like systems but not on Windows. +-/ +@[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool +/-- +Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired. +-/ +@[extern "lean_io_prim_handle_unlock"] opaque unlock (h : @& Handle) : IO Unit + +/-- +Returns `true` if a handle refers to a Windows console or a Unix terminal. +-/ +@[extern "lean_io_prim_handle_is_tty"] opaque isTty (h : @& Handle) : BaseIO Bool + +/-- +Flushes the output buffer associated with the handle, writing any unwritten data to the associated +output device. +-/ +@[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit +/-- +Rewinds the read/write cursor to the beginning of the handle's file. +-/ +@[extern "lean_io_prim_handle_rewind"] opaque rewind (h : @& Handle) : IO Unit +/-- +Truncates the handle to its read/write cursor. + +This operation does not automatically flush output buffers, so the contents of the output device may +not reflect the change immediately. This does not usually lead to problems because the read/write +cursor includes buffered writes. However, buffered writes followed by `IO.FS.Handle.rewind`, then +`IO.FS.Handle.truncate`, and then closing the file may lead to a non-empty file. If unsure, call +`IO.FS.Handle.flush` before truncating. +-/ +@[extern "lean_io_prim_handle_truncate"] opaque truncate (h : @& Handle) : IO Unit +/-- +Reads up to the given number of bytes from the handle. If the returned array is empty, an +end-of-file marker (EOF) has been reached. + +Encountering an EOF does not close a handle. Subsequent reads may block and return more data. +-/ +@[extern "lean_io_prim_handle_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray +/-- +Writes the provided bytes to the handle. + +Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use +`IO.FS.Handle.flush` to write changes to buffers to the associated device. +-/ +@[extern "lean_io_prim_handle_write"] opaque write (h : @& Handle) (buffer : @& ByteArray) : IO Unit + +/-- +Reads UTF-8-encoded text up to and including the next line break from the handle. If the returned +string is empty, an end-of-file marker (EOF) has been reached. + +Encountering an EOF does not close a handle. Subsequent reads may block and return more data. +-/ +@[extern "lean_io_prim_handle_get_line"] opaque getLine (h : @& Handle) : IO String +/-- +Writes the provided string to the file handle using the UTF-8 encoding. + +Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use +`IO.FS.Handle.flush` to write changes to buffers to the associated device. +-/ +@[extern "lean_io_prim_handle_put_str"] opaque putStr (h : @& Handle) (s : @& String) : IO Unit + +end Handle + +/-- +Resolves a path to an absolute path that contains no '.', '..', or symbolic links. + +This function coincides with the [POSIX `realpath` +function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/realpath.html). +-/ +@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath + +/-- +Removes (deletes) a file from the filesystem. + +To remove a directory, use `IO.FS.removeDir` or `IO.FS.removeDirAll` instead. +-/ +@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit + +/-- +Removes (deletes) a directory. + +Removing a directory fails if the directory is not empty. Use `IO.FS.removeDirAll` to remove +directories along with their contents. +-/ +@[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit +/-- +Creates a directory at the specified path. The parent directory must already exist. + +Throws an exception if the directory cannot be created. +-/ +@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit + + +/-- +Moves a file or directory `old` to the new location `new`. + +This function coincides with the [POSIX `rename` +function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html). +-/ +@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit + +/-- +Creates a new hard link. + +The `link` path will be a link pointing to the `orig` path. +Note that systems often require these two paths to both be located on the same filesystem. +If `orig` names a symbolic link, it is platform-specific whether the symbolic link is followed. + +This function coincides with the [POSIX `link` +function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/link.html). +-/ +@[extern "lean_io_hard_link"] opaque hardLink (orig link : @& FilePath) : IO Unit + +/-- +Creates a temporary file in the most secure manner possible, returning both a `Handle` to the +already-opened file and its path. + +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. + +It is the caller's job to remove the file after use. Use `withTempFile` to ensure that the temporary +file is removed. +-/ +@[extern "lean_io_create_tempfile"] opaque createTempFile : IO (Handle × FilePath) + +/-- +Creates a temporary directory in the most secure manner possible, returning the new directory's +path. There are no race conditions in the directory’s creation. The directory is readable and +writable only by the creating user ID. + +It is the caller's job to remove the directory after use. Use `withTempDir` to ensure that the +temporary directory is removed. +-/ +@[extern "lean_io_create_tempdir"] opaque createTempDir : IO FilePath + +end FS + +/-- +Returns the value of the environment variable `var`, or `none` if it is not present in the +environment. +-/ +@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String) +/-- +Returns the file name of the currently-running executable. +-/ +@[extern "lean_io_app_path"] opaque appPath : IO FilePath +/-- +Returns the current working directory of the executing process. +-/ +@[extern "lean_io_current_dir"] opaque currentDir : IO FilePath + +namespace FS + +/-- +Opens the file `fn` with the specified `mode` and passes the resulting file handle to `f`. + +The file handle is closed when the last reference to it is dropped. If references escape `f`, then +the file remains open even after `IO.FS.withFile` has finished. +-/ +@[inline] +def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α := + Handle.mk fn mode >>= f + +/-- +Writes the contents of the string to the handle, followed by a newline. Uses UTF-8. +-/ +def Handle.putStrLn (h : Handle) (s : String) : IO Unit := + h.putStr (s.push '\n') + +/-- +Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is +encountered. + +The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from +the handle may block and/or return data. +-/ +partial def Handle.readBinToEndInto (h : Handle) (buf : ByteArray) : IO ByteArray := do + let rec loop (acc : ByteArray) : IO ByteArray := do + let buf ← h.read 1024 + if buf.isEmpty then + return acc + else + loop (acc ++ buf) + loop buf + +/-- +Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is +encountered. + +The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from +the handle may block and/or return data. +-/ +def Handle.readBinToEnd (h : Handle) : IO ByteArray := do + h.readBinToEndInto .empty + +/-- +Reads the entire remaining contents of the file handle as a UTF-8-encoded string. An exception is +thrown if the contents are not valid UTF-8. + +The underlying file is not automatically closed, and subsequent reads from the handle may block +and/or return data. +-/ +def Handle.readToEnd (h : Handle) : IO String := do + let data ← h.readBinToEnd + match String.fromUTF8? data with + | some s => return s + | none => throw <| .userError s!"Tried to read from handle containing non UTF-8 data." + +/-- +Reads the entire remaining contents of the file handle as a UTF-8-encoded array of lines. + +Newline markers are not included in the lines. + +The underlying file is not automatically closed, and subsequent reads from the handle may block +and/or return data. +-/ +partial def Handle.lines (h : Handle) : IO (Array String) := do + let rec read (lines : Array String) := do + let line ← h.getLine + if line.length == 0 then + pure lines + else if line.back == '\n' then + let line := line.dropEnd 1 |>.copy + let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line + read <| lines.push line + else + pure <| lines.push line + read #[] + +/-- +Returns the contents of a UTF-8-encoded text file as an array of lines. + +Newline markers are not included in the lines. +-/ +def lines (fname : FilePath) : IO (Array String) := do + let h ← Handle.mk fname Mode.read + h.lines + +/-- +Write the provided bytes to a binary file at the specified path. +-/ +def writeBinFile (fname : FilePath) (content : ByteArray) : IO Unit := do + let h ← Handle.mk fname Mode.write + h.write content + +/-- +Write contents of a string to a file at the specified path using UTF-8 encoding. +-/ +def writeFile (fname : FilePath) (content : String) : IO Unit := do + let h ← Handle.mk fname Mode.write + h.putStr content + + +/-- +Writes the contents of the string to the stream, followed by a newline. +-/ +def Stream.putStrLn (strm : FS.Stream) (s : String) : IO Unit := + strm.putStr (s.push '\n') + +/-- An entry in a directory on a filesystem. -/ +structure DirEntry where + /-- The directory in which the entry is found. -/ + root : System.FilePath + /-- The name of the entry. -/ + fileName : String + deriving Repr + +/-- The path of the file indicated by the directory entry. -/ +def DirEntry.path (entry : DirEntry) : System.FilePath := + entry.root / entry.fileName + +/-- Types of files that may be found on a filesystem. -/ +inductive FileType where + /-- Directories don't have contents, but may contain other files. -/ + | dir + /-- Ordinary files that have contents and are not directories. -/ + | file + /-- + Symbolic links that are pointers to other named files. Note that `System.FilePath.metadata` never + indicates this type as it follows symlinks; use `System.FilePath.symlinkMetadata` instead. + -/ + | symlink + /-- Files that are neither ordinary files, directories, or symbolic links. -/ + | other + deriving Repr, BEq + +/-- +Low-level system time, tracked in whole seconds and additional nanoseconds. +-/ +structure SystemTime where + /-- The number of whole seconds. -/ + sec : Int + /-- The number of additional nanoseconds. -/ + nsec : UInt32 + deriving Repr, BEq, Ord, Inhabited + +instance : LT SystemTime := ltOfOrd +instance : LE SystemTime := leOfOrd + +/-- +File metadata. + +The metadata for a file can be accessed with `System.FilePath.metadata`/ +`System.FilePath.symlinkMetadata`. +-/ +structure Metadata where + --permissions : ... + /-- File access time. -/ + accessed : SystemTime + /-- File modification time. -/ + modified : SystemTime + /-- The size of the file in bytes. -/ + byteSize : UInt64 + /-- + Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file. + -/ + type : FileType + deriving Repr + +end FS +end IO + +namespace System.FilePath +open IO + +/-- +Returns the contents of the indicated directory. Throws an exception if the file does not exist or +is not a directory. +-/ +@[extern "lean_io_read_dir"] +opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry) + +/-- +Returns metadata for the indicated file, following symlinks. Throws an exception if the file does +not exist or the metadata cannot be accessed. +-/ +@[extern "lean_io_metadata"] +opaque metadata : @& FilePath → IO IO.FS.Metadata + +/-- +Returns metadata for the indicated file without following symlinks. Throws an exception if the file +does not exist or the metadata cannot be accessed. +-/ +@[extern "lean_io_symlink_metadata"] +opaque symlinkMetadata : @& FilePath → IO IO.FS.Metadata + +/-- +Checks whether the indicated path can be read and is a directory. This function will traverse +symlinks. +-/ +def isDir (p : FilePath) : BaseIO Bool := do + match (← p.metadata.toBaseIO) with + | Except.ok m => return m.type == IO.FS.FileType.dir + | Except.error _ => return false + +/-- +Checks whether the indicated path points to a file that exists. This function will traverse +symlinks. +-/ +def pathExists (p : FilePath) : BaseIO Bool := + return (← p.metadata.toBaseIO).toBool + +/-- +Traverses a filesystem starting at the path `p` and exploring directories that satisfy `enter`, +returning the paths visited. + +The traversal is a preorder traversal, in which parent directories occur prior to any of their +children. Symbolic links are followed. +-/ +partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) : IO (Array FilePath) := + Prod.snd <$> StateT.run (go p) #[] +where + go p := do + if !(← enter p) then + return () + for d in (← p.readDir) do + modify (·.push d.path) + match (← d.path.metadata.toBaseIO) with + | .ok { type := .symlink, .. } => + let p' ← FS.realPath d.path + if (← p'.isDir) then + -- do not call `enter` on a non-directory symlink + if (← enter p) then + go p' + | .ok { type := .dir, .. } => go d.path + | .ok _ => pure () + -- entry vanished, ignore + | .error (.noFileOrDirectory ..) => pure () + | .error e => throw e + +end System.FilePath + +namespace IO + +namespace FS + +/-- +Reads the entire contents of the binary file at the given path as an array of bytes. +-/ +def readBinFile (fname : FilePath) : IO ByteArray := do + -- Requires metadata so defined after metadata + let mdata ← fname.metadata + let size := mdata.byteSize.toUSize + let handle ← IO.FS.Handle.mk fname .read + let buf ← + if size > 0 then + handle.read mdata.byteSize.toUSize + else + pure <| ByteArray.emptyWithCapacity 0 + handle.readBinToEndInto buf + +/-- +Reads the entire contents of the UTF-8-encoded file at the given path as a `String`. + +An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to +exceptions that may always be thrown as a result of failing to read files. +-/ +def readFile (fname : FilePath) : IO String := do + let data ← readBinFile fname + match String.fromUTF8? data with + | some s => return s + | none => throw <| .userError s!"Tried to read file '{fname}' containing non UTF-8 data." + +end FS + +/-- +Runs an action with the specified stream `h` as standard input, restoring the original standard +input stream afterwards. +-/ +def withStdin [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do + let prev ← setStdin h + try x finally discard <| setStdin prev + +/-- +Runs an action with the specified stream `h` as standard output, restoring the original standard +output stream afterwards. +-/ +def withStdout [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do + let prev ← setStdout h + try + x + finally + discard <| setStdout prev + +/-- +Runs an action with the specified stream `h` as standard error, restoring the original standard +error stream afterwards. +-/ +def withStderr [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do + let prev ← setStderr h + try x finally discard <| setStderr prev + +/-- +Converts `s` to a string using its `ToString α` instance, and prints it to the current standard +output (as determined by `IO.getStdout`). +-/ +def print [ToString α] (s : α) : IO Unit := do + let out ← getStdout + out.putStr <| toString s + +/-- +Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to +the current standard output (as determined by `IO.getStdout`). +-/ +def println [ToString α] (s : α) : IO Unit := + print ((toString s).push '\n') + +/-- +Converts `s` to a string using its `ToString α` instance, and prints it to the current standard +error (as determined by `IO.getStderr`). +-/ +def eprint [ToString α] (s : α) : IO Unit := do + let out ← getStderr + out.putStr <| toString s + +/-- +Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to +the current standard error (as determined by `IO.getStderr`). +-/ +def eprintln [ToString α] (s : α) : IO Unit := + eprint <| toString s |>.push '\n' + +@[export lean_io_eprint] +private def eprintAux (s : String) : IO Unit := + eprint s + +@[export lean_io_eprintln] +private def eprintlnAux (s : String) : IO Unit := + eprintln s + +/-- +Returns the directory that the current executable is located in. +-/ +def appDir : IO FilePath := do + let p ← appPath + let some p ← pure p.parent + | throw <| IO.userError s!"IO.appDir: unexpected filename '{p}'" + FS.realPath p + +namespace FS + +/-- +Creates a directory at the specified path, creating all missing parents as directories. +-/ +partial def createDirAll (p : FilePath) : IO Unit := do + if ← p.isDir then + return () + if let some parent := p.parent then + createDirAll parent + try + createDir p + catch + | e => + if ← p.isDir then + pure () -- I guess someone else was faster + else + throw e + +/-- +Fully remove given directory by deleting all contained files and directories in an unspecified order. +Symlinks are deleted but not followed. Fails if any contained entry cannot be deleted or was newly +created during execution. +-/ +partial def removeDirAll (p : FilePath) : IO Unit := do + for ent in (← p.readDir) do + -- Do not follow symlinks + if (← ent.path.symlinkMetadata).type == .dir then + removeDirAll ent.path + else + removeFile ent.path + removeDir p + +/-- +Creates a temporary file in the most secure manner possible and calls `f` with both a `Handle` to +the already-opened file and its path. Afterwards, the temporary file is deleted. + +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. + +Use `IO.FS.createTempFile` to avoid the automatic deletion of the temporary file. +-/ +def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) : + m α := do + let (handle, path) ← createTempFile + try + f handle path + finally + removeFile path + +/-- +Creates a temporary directory in the most secure manner possible, providing a its path to an `IO` +action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how +or when they were created. + +There are no race conditions in the directory’s creation. The directory is readable and writable +only by the creating user ID. Use `IO.FS.createTempDir` to avoid the automatic deletion of the +directory's contents. +-/ +def withTempDir [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) : + m α := do + let path ← createTempDir + try + f path + finally + removeDirAll path + +end FS + +namespace Process + +/-- Returns the current working directory of the calling process. -/ +@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath + +/-- Sets the current working directory of the calling process. -/ +@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit + +/-- Returns the process ID of the calling process. -/ +@[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32 + +/-- +Whether the standard input, output, and error handles of a child process should be attached to +pipes, inherited from the parent, or null. + +If the stream is a pipe, then the parent process can use it to communicate with the child. +-/ +inductive Stdio where + /-- The stream should be attached to a pipe. -/ + | piped + /-- The stream should be inherited from the parent process. -/ + | inherit + /-- The stream should be empty. -/ + | null + +/-- +The type of handles that can be used to communicate with a child process on its standard input, +output, or error streams. + +For `IO.Process.Stdio.piped`, this type is `IO.FS.Handle`. Otherwise, it is `Unit`, because no +communication is possible. +-/ +@[expose] def Stdio.toHandleType : Stdio → Type + | Stdio.piped => FS.Handle + | Stdio.inherit => Unit + | Stdio.null => Unit + +/-- +Configuration for the standard input, output, and error handles of a child process. +-/ +structure StdioConfig where + /-- Configuration for the process' stdin handle. -/ + stdin := Stdio.inherit + /-- Configuration for the process' stdout handle. -/ + stdout := Stdio.inherit + /-- Configuration for the process' stderr handle. -/ + stderr := Stdio.inherit + +/-- +Configuration for a child process to be spawned. + +Use `IO.Process.spawn` to start the child process. `IO.Process.output` and `IO.Process.run` can be +used when the child process should be run to completion, with its output and/or error code captured. +-/ +structure SpawnArgs extends StdioConfig where + /-- Command name. -/ + cmd : String + /-- Arguments for the command. -/ + args : Array String := #[] + /-- The child process's working directory. Inherited from the parent current process if `none`. -/ + cwd : Option FilePath := none + /-- + Add or remove environment variables for the child process. + + The child process inherits the parent's environment, as modified by `env`. Keys in the array are + the names of environment variables. A `none`, causes the entry to be removed from the environment, + and `some` sets the variable to the new value, adding it if necessary. Variables are processed from left to right. + -/ + env : Array (String × Option String) := #[] + /-- Inherit environment variables from the spawning process. -/ + inheritEnv : Bool := true + /-- + Starts the child process in a new session and process group using `setsid`. Currently a no-op on + non-POSIX platforms. + -/ + setsid : Bool := false + +/-- +A child process that was spawned with configuration `cfg`. + +The configuration determines whether the child process's standard input, standard output, and +standard error are `IO.FS.Handle`s or `Unit`. +-/ +structure Child (cfg : StdioConfig) where private mk :: + /-- + The child process's standard input handle, if it was configured as `IO.Process.Stdio.piped`, or + `()` otherwise. + -/ + stdin : cfg.stdin.toHandleType + /-- + The child process's standard output handle, if it was configured as `IO.Process.Stdio.piped`, or + `()` otherwise. + -/ + stdout : cfg.stdout.toHandleType + /-- + The child process's standard error handle, if it was configured as `IO.Process.Stdio.piped`, or + `()` otherwise. + -/ + stderr : cfg.stderr.toHandleType + +/-- +Starts a child process with the provided configuration. The child process is spawned using operating +system primitives, and it can be written in any language. + +The child process runs in parallel with the parent. + +If the child process's standard input is a pipe, use `IO.Process.Child.takeStdin` to make it +possible to close the child's standard input before the process terminates, which provides the child with an end-of-file marker. +-/ +@[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig) + +/-- +Blocks until the child process has exited and return its exit code. +-/ +@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32 + +/-- +Checks whether the child has exited. Returns `none` if the process has not exited, or its exit code +if it has. +-/ +@[extern "lean_io_process_child_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg → + IO (Option UInt32) + +/-- +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_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit + +/-- +Extracts the `stdin` field from a `Child` object, allowing the handle to be closed while maintaining +a reference to the child process. + +File handles are closed when the last reference to them is dropped. Closing the child's standard +input causes an end-of-file marker. Because the `Child` object has a reference to the standard +input, this operation is necessary in order to close the stream while the process is running (e.g. +to extract its exit code after calling `Child.wait`). Many processes do not terminate until their +standard input is exhausted. +-/ +@[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg → + IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null }) + +/-- Returns the operating system process id of the child process. -/ +@[extern "lean_io_process_child_pid"] opaque Child.pid {cfg : @& StdioConfig} : Child cfg → UInt32 + +/-- +The result of running a process to completion. +-/ +structure Output where + /-- The process's exit code. -/ + exitCode : UInt32 + /-- Everything that was written to the process's standard output. -/ + stdout : String + /-- Everything that was written to the process's standard error. -/ + stderr : String + +/-- +Runs a process to completion and captures its output and exit code. +The child process is run with a null standard input or the specified input if provided, +and the current process blocks until it has run to completion. + +The specifications of standard input, output, and error handles in `args` are ignored. +-/ +def output (args : SpawnArgs) (input? : Option String := none) : IO Output := do + let child ← + if let some input := input? then + let (stdin, child) ← (← spawn { args with stdout := .piped, stderr := .piped, stdin := .piped }).takeStdin + stdin.putStr input + stdin.flush + pure child + else + spawn { args with stdout := .piped, stderr := .piped, stdin := .null } + let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated + let stderr ← child.stderr.readToEnd + let exitCode ← child.wait + let stdout ← IO.ofExcept stdout.get + pure { exitCode := exitCode, stdout := stdout, stderr := stderr } + +/-- +Runs a process to completion, blocking until it terminates. +The child process is run with a null standard input or the specified input if provided, +If the child process terminates successfully with exit code 0, its standard output is returned. +An exception is thrown if it terminates with any other exit code. + +The specifications of standard input, output, and error handles in `args` are ignored. +-/ +def run (args : SpawnArgs) (input? : Option String := none) : IO String := do + let out ← output args input? + if out.exitCode != 0 then + throw <| IO.userError s!"process '{args.cmd}' exited with code {out.exitCode}\ + \nstderr:\ + \n{out.stderr}" + pure out.stdout + +/-- +Terminates the current process with the provided exit code. `0` indicates success, all other values +indicate failure. +-/ +@[extern "lean_io_exit"] opaque exit : UInt8 → IO α + +/-- +Terminates the current process with the provided exit code. `0` indicates success, all other values +indicate failure. + +Calling this function is equivalent to calling +[`std::_Exit`](https://en.cppreference.com/w/cpp/utility/program/_Exit.html). +-/ +@[extern "lean_io_force_exit"] opaque forceExit : UInt8 → IO α + +end Process + +/-- Returns the thread ID of the calling thread. -/ +@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64 + +/-- +POSIX-style file permissions. + +The `FileRight` structure describes these permissions for a file's owner, members of it's designated +group, and all others. +-/ +structure AccessRight where + /-- The file can be read. -/ + read : Bool := false + /-- The file can be written to. -/ + write : Bool := false + /-- The file can be executed. -/ + execution : Bool := false + +/-- +Converts individual POSIX-style file permissions to their conventional three-bit representation. + +This is the bitwise `or` of the following: + * If the file can be read, `0x4`, otherwise `0`. + * If the file can be written, `0x2`, otherwise `0`. + * If the file can be executed, `0x1`, otherwise `0`. + +Examples: + * `{read := true : AccessRight}.flags = 4` + * `{read := true, write := true : AccessRight}.flags = 6` + * `{read := true, execution := true : AccessRight}.flags = 5` +-/ +def AccessRight.flags (acc : AccessRight) : UInt32 := + let r : UInt32 := if acc.read then 0x4 else 0 + let w : UInt32 := if acc.write then 0x2 else 0 + let x : UInt32 := if acc.execution then 0x1 else 0 + r.lor <| w.lor x + +/-- +POSIX-style file permissions that describe access rights for a file's owner, members of its +assigned group, and all others. +-/ +structure FileRight where + /-- The owner's permissions to access the file. -/ + user : AccessRight := {} + /-- The assigned group's permissions to access the file. -/ + group : AccessRight := {} + /-- The permissions that all others have to access the file. -/ + other : AccessRight := {} + +/-- +Converts POSIX-style file permissions to their numeric representation, with three bits each for the +owner's permissions, the group's permissions, and others' permissions. +-/ +def FileRight.flags (acc : FileRight) : UInt32 := + let u : UInt32 := acc.user.flags.shiftLeft 6 + let g : UInt32 := acc.group.flags.shiftLeft 3 + let o : UInt32 := acc.other.flags + u.lor <| g.lor o + +@[extern "lean_chmod"] opaque Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit + +/-- +Sets the POSIX-style permissions for a file. +-/ +def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit := + Prim.setAccessRights filename mode.flags + +/-- +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. +-/ +structure CancelToken where + private ref : IO.Ref Bool +deriving Nonempty + +namespace CancelToken + +/-- Creates a new cancellation token. -/ +def new : BaseIO CancelToken := + CancelToken.mk <$> IO.mkRef false + +/-- Activates a cancellation token. Idempotent. -/ +def set (tk : CancelToken) : BaseIO Unit := + tk.ref.set true + +/-- Checks whether the cancellation token has been activated. -/ +def isSet (tk : CancelToken) : BaseIO Bool := + tk.ref.get + +-- separate definition as otherwise no unboxed version is generated +@[export lean_io_cancel_token_is_set] +private def isSetExport := @isSet + +end CancelToken + +namespace FS +namespace Stream + +/-- +Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding +file handle operation. +-/ +@[export lean_stream_of_handle] +def ofHandle (h : Handle) : Stream where + flush := Handle.flush h + read := Handle.read h + write := Handle.write h + getLine := Handle.getLine h + putStr := Handle.putStr h + isTty := Handle.isTty h + +/-- +A byte buffer that can simulate a file in memory. + +Use `IO.FS.Stream.ofBuffer` to create a stream from a buffer. +-/ +structure Buffer where + /-- The contents of the buffer. -/ + data : ByteArray := ByteArray.empty + /-- The read/write cursor's position in the buffer. -/ + pos : Nat := 0 + +/-- +Creates a stream from a mutable reference to a buffer. + +The resulting stream simulates a file, mutating the contents of the reference in response to writes +and reading from it in response to reads. These streams can be used with `IO.withStdin`, +`IO.setStdin`, and the corresponding operators for standard output and standard error to redirect +input and output. +-/ +def ofBuffer (r : Ref Buffer) : Stream where + flush := pure () + read := fun n => r.modifyGet fun b => + let data := b.data.extract b.pos (b.pos + n.toNat) + (data, { b with pos := b.pos + data.size }) + write := fun data => r.modify fun b => + -- set `exact` to `false` so that repeatedly writing to the stream does not impose quadratic run time + { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size } + getLine := do + let buf ← r.modifyGet fun b => + let pos := match b.data.findIdx? (start := b.pos) fun u => u == 0 || u = '\n'.toNat.toUInt8 with + -- include '\n', but not '\0' + | some pos => if b.data.get! pos == 0 then pos else pos + 1 + | none => b.data.size + (b.data.extract b.pos pos, { b with pos := pos }) + match String.fromUTF8? buf with + | some str => pure str + | none => throw (.userError "invalid UTF-8") + putStr := fun s => r.modify fun b => + let data := s.toUTF8 + { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size } + isTty := pure false + +/-- +Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is +encountered. + +The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from +the stream may block and/or return data. +-/ +partial def readBinToEndInto (s : Stream) (buf : ByteArray) : IO ByteArray := do + let rec loop (acc : ByteArray) : IO ByteArray := do + let buf ← s.read 1024 + if buf.isEmpty then + return acc + else + loop (acc ++ buf) + loop buf + +/-- +Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is +encountered. + +The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from +the stream may block and/or return data. +-/ +def readBinToEnd (s : Stream) : IO ByteArray := do + s.readBinToEndInto .empty + +/-- +Reads the entire remaining contents of the stream as a UTF-8-encoded string. An exception is +thrown if the contents are not valid UTF-8. + +The underlying stream is not automatically closed, and subsequent reads from the stream may block +and/or return data. +-/ +def readToEnd (s : Stream) : IO String := do + let data ← s.readBinToEnd + match String.fromUTF8? data with + | some s => return s + | none => throw <| .userError s!"Tried to read from stream containing non UTF-8 data." + +/-- +Reads the entire remaining contents of the stream as a UTF-8-encoded array of lines. + +Newline markers are not included in the lines. + +The underlying stream is not automatically closed, and subsequent reads from the stream may block +and/or return data. +-/ +partial def lines (s : Stream) : IO (Array String) := do + let rec read (lines : Array String) := do + let line ← s.getLine + if line.length == 0 then + pure lines + else if line.back == '\n' then + let line := line.dropEnd 1 |>.copy + let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line + read <| lines.push line + else + pure <| lines.push line + read #[] + +end Stream + +/-- +Runs an action with `stdin` emptied and `stdout` and `stderr` captured into a `String`. If +`isolateStderr` is `false`, only `stdout` is captured. +-/ +def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α) + (isolateStderr := true) : m (String × α) := do + let bIn ← mkRef { : Stream.Buffer } + let bOut ← mkRef { : Stream.Buffer } + let r ← withStdin (Stream.ofBuffer bIn) <| + withStdout (Stream.ofBuffer bOut) <| + (if isolateStderr then withStderr (Stream.ofBuffer bOut) else id) <| + x + let bOut ← liftM (m := BaseIO) bOut.get + let out := String.fromUTF8! bOut.data + pure (out, r) + +end FS +end IO + +syntax "println! " (interpolatedStr(term) <|> term) : term + +macro_rules + | `(println! $msg:interpolatedStr) => `((IO.println (s! $msg) : IO Unit)) + | `(println! $msg:term) => `((IO.println $msg : IO Unit)) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 6d6b1ddb83d0..79bc2cd887bf 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -7,10 +7,9 @@ module prelude public import Init.System.IOError -public import Init.System.FilePath -public import Init.Data.Ord.UInt -import Init.Data.String.TakeDrop -import Init.Data.String.Search +public import Init.System.ST +public import Init.Data.Ord.Basic +import Init.Data.List.MapIdx public section @@ -399,6 +398,24 @@ Creates an IO action that will invoke `fn` if and when it is executed, returning def lazyPure (fn : Unit → α) : IO α := pure (fn ()) +/-- +Mutable reference cells that contain values of type `α`. These cells can read from and mutated in +the `IO` monad. +-/ +abbrev Ref (α : Type) := ST.Ref IO.RealWorld α + +instance : MonadLift (ST IO.RealWorld) BaseIO where + monadLift mx := fun s => + match mx s with + | .mk s a => .mk s a + +/-- +Creates a new mutable reference cell that contains `a`. +-/ +def mkRef (a : α) : BaseIO (IO.Ref α) := + ST.mkRef a + + /-- Monotonically increasing time since an unspecified past point in milliseconds. There is no relation to wall clock time. @@ -602,1241 +619,8 @@ def addHeartbeats (count : Nat) : BaseIO Unit := do let n ← getNumHeartbeats setNumHeartbeats (n + count) -/-- -Whether a file should be opened for reading, writing, creation and writing, or appending. - -At the operating system level, this translates to the mode of a file handle (i.e., a set of `open` -flags and an `fdopen` mode). - -None of the modes represented by this datatype translate line endings (i.e. `O_BINARY` on Windows). -Furthermore, they are not inherited across process creation (i.e. `O_NOINHERIT` on Windows and -`O_CLOEXEC` elsewhere). - -**Operating System Specifics:** -* Windows: - [`_open`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/open-wopen?view=msvc-170), - [`_fdopen`](https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fdopen-wfdopen?view=msvc-170) -* Linux: [`open`](https://linux.die.net/man/2/open), [`fdopen`](https://linux.die.net/man/3/fdopen) --/ -inductive FS.Mode where - /-- - The file should be opened for reading. - - The read/write cursor is positioned at the beginning of the file. It is an error if the file does - not exist. - - * `open` flags: `O_RDONLY` - * `fdopen` mode: `r` - -/ - | read - /-- - The file should be opened for writing. - - If the file already exists, it is truncated to zero length. Otherwise, a new file is created. The - read/write cursor is positioned at the beginning of the file. - - * `open` flags: `O_WRONLY | O_CREAT | O_TRUNC` - * `fdopen` mode: `w` - -/ - | write - /-- - A new file should be created for writing. - - It is an error if the file already exists. A new file is created, with the read/write cursor - positioned at the start. - - * `open` flags: `O_WRONLY | O_CREAT | O_TRUNC | O_EXCL` - * `fdopen` mode: `w` - -/ - | writeNew - /-- - The file should be opened for both reading and writing. - - It is an error if the file does not already exist. The read/write cursor is positioned at the - start of the file. - - * `open` flags: `O_RDWR` - * `fdopen` mode: `r+` - -/ - | readWrite - /-- - The file should be opened for writing. - - If the file does not already exist, it is created. If the file already exists, it is opened, and - the read/write cursor is positioned at the end of the file. - - * `open` flags: `O_WRONLY | O_CREAT | O_APPEND` - * `fdopen` mode: `a` - -/ - | append - -/-- -A reference to an opened file. - -File handles wrap the underlying operating system's file descriptors. There is no explicit operation -to close a file: when the last reference to a file handle is dropped, the file is closed -automatically. - -Handles have an associated read/write cursor that determines the where reads and writes occur in the -file. --/ -opaque FS.Handle : Type := Unit - -/-- -A pure-Lean abstraction of POSIX streams. These streams may represent an underlying POSIX stream or -be implemented by Lean code. - -Because standard input, standard output, and standard error are all `IO.FS.Stream`s that can be -overridden, Lean code may capture and redirect input and output. --/ -structure FS.Stream where - /-- - Flushes the stream's output buffers. - -/ - flush : IO Unit - /-- - Reads up to the given number of bytes from the stream. - - If the returned array is empty, an end-of-file marker (EOF) has been reached. An EOF does not - actually close a stream, so further reads may block and return more data. - -/ - read : USize → IO ByteArray - /-- - Writes the provided bytes to the stream. - - If the stream represents a physical output device such as a file on disk, then the results may be - buffered. Call `FS.Stream.flush` to synchronize their contents. - -/ - write : ByteArray → IO Unit - /-- - Reads text up to and including the next newline from the stream. - - If the returned string is empty, an end-of-file marker (EOF) has been reached. - An EOF does not actually close a stream, so further reads may block and return more data. - -/ - getLine : IO String - /-- - Writes the provided string to the stream. - -/ - putStr : String → IO Unit - /-- Returns `true` if a stream refers to a Windows console or Unix terminal. -/ - isTty : BaseIO Bool - deriving Inhabited - -open FS - -/-- -Returns the current thread's standard input stream. - -Use `IO.setStdin` to replace the current thread's standard input stream. --/ -@[extern "lean_get_stdin"] opaque getStdin : BaseIO FS.Stream -/-- -Returns the current thread's standard output stream. - -Use `IO.setStdout` to replace the current thread's standard output stream. --/ -@[extern "lean_get_stdout"] opaque getStdout : BaseIO FS.Stream -/-- -Returns the current thread's standard error stream. - -Use `IO.setStderr` to replace the current thread's standard error stream. --/ -@[extern "lean_get_stderr"] opaque getStderr : BaseIO FS.Stream - -/-- -Replaces the standard input stream of the current thread and returns its previous value. - -Use `IO.getStdin` to get the current standard input stream. --/ -@[extern "lean_get_set_stdin"] opaque setStdin : FS.Stream → BaseIO FS.Stream -/-- -Replaces the standard output stream of the current thread and returns its previous value. - -Use `IO.getStdout` to get the current standard output stream. --/ -@[extern "lean_get_set_stdout"] opaque setStdout : FS.Stream → BaseIO FS.Stream -/-- -Replaces the standard error stream of the current thread and returns its previous value. - -Use `IO.getStderr` to get the current standard error stream. --/ -@[extern "lean_get_set_stderr"] opaque setStderr : FS.Stream → BaseIO FS.Stream - -/-- -Iterates an `IO` action. Starting with an initial state, the action is applied repeatedly until it -returns a final value in `Sum.inr`. Each time it returns `Sum.inl`, the returned value is treated as -a new state. --/ -@[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do - let v ← f a - match v with - | Sum.inl a => iterate a f - | Sum.inr b => pure b - -namespace FS - -namespace Handle - -/-- -Opens the file at `fn` with the given `mode`. - -An exception is thrown if the file cannot be opened. --/ -@[extern "lean_io_prim_handle_mk"] opaque mk (fn : @& FilePath) (mode : FS.Mode) : IO Handle - -/-- -Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary. - -Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it -works on Unix-like systems but not on Windows. --/ -@[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit -/-- -Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will -not block if the lock cannot be acquired, but instead returns `false`. - -Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it -works on Unix-like systems but not on Windows. --/ -@[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool -/-- -Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired. --/ -@[extern "lean_io_prim_handle_unlock"] opaque unlock (h : @& Handle) : IO Unit - -/-- -Returns `true` if a handle refers to a Windows console or a Unix terminal. --/ -@[extern "lean_io_prim_handle_is_tty"] opaque isTty (h : @& Handle) : BaseIO Bool - -/-- -Flushes the output buffer associated with the handle, writing any unwritten data to the associated -output device. --/ -@[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit -/-- -Rewinds the read/write cursor to the beginning of the handle's file. --/ -@[extern "lean_io_prim_handle_rewind"] opaque rewind (h : @& Handle) : IO Unit -/-- -Truncates the handle to its read/write cursor. - -This operation does not automatically flush output buffers, so the contents of the output device may -not reflect the change immediately. This does not usually lead to problems because the read/write -cursor includes buffered writes. However, buffered writes followed by `IO.FS.Handle.rewind`, then -`IO.FS.Handle.truncate`, and then closing the file may lead to a non-empty file. If unsure, call -`IO.FS.Handle.flush` before truncating. --/ -@[extern "lean_io_prim_handle_truncate"] opaque truncate (h : @& Handle) : IO Unit -/-- -Reads up to the given number of bytes from the handle. If the returned array is empty, an -end-of-file marker (EOF) has been reached. - -Encountering an EOF does not close a handle. Subsequent reads may block and return more data. --/ -@[extern "lean_io_prim_handle_read"] opaque read (h : @& Handle) (bytes : USize) : IO ByteArray -/-- -Writes the provided bytes to the handle. - -Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use -`IO.FS.Handle.flush` to write changes to buffers to the associated device. --/ -@[extern "lean_io_prim_handle_write"] opaque write (h : @& Handle) (buffer : @& ByteArray) : IO Unit - -/-- -Reads UTF-8-encoded text up to and including the next line break from the handle. If the returned -string is empty, an end-of-file marker (EOF) has been reached. - -Encountering an EOF does not close a handle. Subsequent reads may block and return more data. --/ -@[extern "lean_io_prim_handle_get_line"] opaque getLine (h : @& Handle) : IO String -/-- -Writes the provided string to the file handle using the UTF-8 encoding. - -Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use -`IO.FS.Handle.flush` to write changes to buffers to the associated device. --/ -@[extern "lean_io_prim_handle_put_str"] opaque putStr (h : @& Handle) (s : @& String) : IO Unit - -end Handle - -/-- -Resolves a path to an absolute path that contains no '.', '..', or symbolic links. - -This function coincides with the [POSIX `realpath` -function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/realpath.html). --/ -@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath - -/-- -Removes (deletes) a file from the filesystem. - -To remove a directory, use `IO.FS.removeDir` or `IO.FS.removeDirAll` instead. --/ -@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit - -/-- -Removes (deletes) a directory. - -Removing a directory fails if the directory is not empty. Use `IO.FS.removeDirAll` to remove -directories along with their contents. --/ -@[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit -/-- -Creates a directory at the specified path. The parent directory must already exist. - -Throws an exception if the directory cannot be created. --/ -@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit - - -/-- -Moves a file or directory `old` to the new location `new`. - -This function coincides with the [POSIX `rename` -function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html). --/ -@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit - -/-- -Creates a new hard link. - -The `link` path will be a link pointing to the `orig` path. -Note that systems often require these two paths to both be located on the same filesystem. -If `orig` names a symbolic link, it is platform-specific whether the symbolic link is followed. - -This function coincides with the [POSIX `link` -function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/link.html). --/ -@[extern "lean_io_hard_link"] opaque hardLink (orig link : @& FilePath) : IO Unit - -/-- -Creates a temporary file in the most secure manner possible, returning both a `Handle` to the -already-opened file and its path. - -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. - -It is the caller's job to remove the file after use. Use `withTempFile` to ensure that the temporary -file is removed. --/ -@[extern "lean_io_create_tempfile"] opaque createTempFile : IO (Handle × FilePath) - -/-- -Creates a temporary directory in the most secure manner possible, returning the new directory's -path. There are no race conditions in the directory’s creation. The directory is readable and -writable only by the creating user ID. - -It is the caller's job to remove the directory after use. Use `withTempDir` to ensure that the -temporary directory is removed. --/ -@[extern "lean_io_create_tempdir"] opaque createTempDir : IO FilePath - -end FS - -/-- -Returns the value of the environment variable `var`, or `none` if it is not present in the -environment. --/ -@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String) -/-- -Returns the file name of the currently-running executable. --/ -@[extern "lean_io_app_path"] opaque appPath : IO FilePath -/-- -Returns the current working directory of the executing process. --/ -@[extern "lean_io_current_dir"] opaque currentDir : IO FilePath - -namespace FS - -/-- -Opens the file `fn` with the specified `mode` and passes the resulting file handle to `f`. - -The file handle is closed when the last reference to it is dropped. If references escape `f`, then -the file remains open even after `IO.FS.withFile` has finished. --/ -@[inline] -def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α := - Handle.mk fn mode >>= f - -/-- -Writes the contents of the string to the handle, followed by a newline. Uses UTF-8. --/ -def Handle.putStrLn (h : Handle) (s : String) : IO Unit := - h.putStr (s.push '\n') - -/-- -Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is -encountered. - -The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from -the handle may block and/or return data. --/ -partial def Handle.readBinToEndInto (h : Handle) (buf : ByteArray) : IO ByteArray := do - let rec loop (acc : ByteArray) : IO ByteArray := do - let buf ← h.read 1024 - if buf.isEmpty then - return acc - else - loop (acc ++ buf) - loop buf - -/-- -Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is -encountered. - -The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from -the handle may block and/or return data. --/ -def Handle.readBinToEnd (h : Handle) : IO ByteArray := do - h.readBinToEndInto .empty - -/-- -Reads the entire remaining contents of the file handle as a UTF-8-encoded string. An exception is -thrown if the contents are not valid UTF-8. - -The underlying file is not automatically closed, and subsequent reads from the handle may block -and/or return data. --/ -def Handle.readToEnd (h : Handle) : IO String := do - let data ← h.readBinToEnd - match String.fromUTF8? data with - | some s => return s - | none => throw <| .userError s!"Tried to read from handle containing non UTF-8 data." - -/-- -Reads the entire remaining contents of the file handle as a UTF-8-encoded array of lines. - -Newline markers are not included in the lines. - -The underlying file is not automatically closed, and subsequent reads from the handle may block -and/or return data. --/ -partial def Handle.lines (h : Handle) : IO (Array String) := do - let rec read (lines : Array String) := do - let line ← h.getLine - if line.length == 0 then - pure lines - else if line.back == '\n' then - let line := line.dropEnd 1 |>.copy - let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line - read <| lines.push line - else - pure <| lines.push line - read #[] - -/-- -Returns the contents of a UTF-8-encoded text file as an array of lines. - -Newline markers are not included in the lines. --/ -def lines (fname : FilePath) : IO (Array String) := do - let h ← Handle.mk fname Mode.read - h.lines - -/-- -Write the provided bytes to a binary file at the specified path. --/ -def writeBinFile (fname : FilePath) (content : ByteArray) : IO Unit := do - let h ← Handle.mk fname Mode.write - h.write content - -/-- -Write contents of a string to a file at the specified path using UTF-8 encoding. --/ -def writeFile (fname : FilePath) (content : String) : IO Unit := do - let h ← Handle.mk fname Mode.write - h.putStr content - - -/-- -Writes the contents of the string to the stream, followed by a newline. --/ -def Stream.putStrLn (strm : FS.Stream) (s : String) : IO Unit := - strm.putStr (s.push '\n') - -/-- An entry in a directory on a filesystem. -/ -structure DirEntry where - /-- The directory in which the entry is found. -/ - root : FilePath - /-- The name of the entry. -/ - fileName : String - deriving Repr - -/-- The path of the file indicated by the directory entry. -/ -def DirEntry.path (entry : DirEntry) : FilePath := - entry.root / entry.fileName - -/-- Types of files that may be found on a filesystem. -/ -inductive FileType where - /-- Directories don't have contents, but may contain other files. -/ - | dir - /-- Ordinary files that have contents and are not directories. -/ - | file - /-- - Symbolic links that are pointers to other named files. Note that `System.FilePath.metadata` never - indicates this type as it follows symlinks; use `System.FilePath.symlinkMetadata` instead. - -/ - | symlink - /-- Files that are neither ordinary files, directories, or symbolic links. -/ - | other - deriving Repr, BEq - -/-- -Low-level system time, tracked in whole seconds and additional nanoseconds. --/ -structure SystemTime where - /-- The number of whole seconds. -/ - sec : Int - /-- The number of additional nanoseconds. -/ - nsec : UInt32 - deriving Repr, BEq, Ord, Inhabited - -instance : LT SystemTime := ltOfOrd -instance : LE SystemTime := leOfOrd - -/-- -File metadata. - -The metadata for a file can be accessed with `System.FilePath.metadata`/ -`System.FilePath.symlinkMetadata`. --/ -structure Metadata where - --permissions : ... - /-- File access time. -/ - accessed : SystemTime - /-- File modification time. -/ - modified : SystemTime - /-- The size of the file in bytes. -/ - byteSize : UInt64 - /-- - Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file. - -/ - type : FileType - deriving Repr - -end FS end IO -namespace System.FilePath -open IO - -/-- -Returns the contents of the indicated directory. Throws an exception if the file does not exist or -is not a directory. --/ -@[extern "lean_io_read_dir"] -opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry) - -/-- -Returns metadata for the indicated file, following symlinks. Throws an exception if the file does -not exist or the metadata cannot be accessed. --/ -@[extern "lean_io_metadata"] -opaque metadata : @& FilePath → IO IO.FS.Metadata - -/-- -Returns metadata for the indicated file without following symlinks. Throws an exception if the file -does not exist or the metadata cannot be accessed. --/ -@[extern "lean_io_symlink_metadata"] -opaque symlinkMetadata : @& FilePath → IO IO.FS.Metadata - -/-- -Checks whether the indicated path can be read and is a directory. This function will traverse -symlinks. --/ -def isDir (p : FilePath) : BaseIO Bool := do - match (← p.metadata.toBaseIO) with - | Except.ok m => return m.type == IO.FS.FileType.dir - | Except.error _ => return false - -/-- -Checks whether the indicated path points to a file that exists. This function will traverse -symlinks. --/ -def pathExists (p : FilePath) : BaseIO Bool := - return (← p.metadata.toBaseIO).toBool - -/-- -Traverses a filesystem starting at the path `p` and exploring directories that satisfy `enter`, -returning the paths visited. - -The traversal is a preorder traversal, in which parent directories occur prior to any of their -children. Symbolic links are followed. --/ -partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) : IO (Array FilePath) := - Prod.snd <$> StateT.run (go p) #[] -where - go p := do - if !(← enter p) then - return () - for d in (← p.readDir) do - modify (·.push d.path) - match (← d.path.metadata.toBaseIO) with - | .ok { type := .symlink, .. } => - let p' ← FS.realPath d.path - if (← p'.isDir) then - -- do not call `enter` on a non-directory symlink - if (← enter p) then - go p' - | .ok { type := .dir, .. } => go d.path - | .ok _ => pure () - -- entry vanished, ignore - | .error (.noFileOrDirectory ..) => pure () - | .error e => throw e - -end System.FilePath - -namespace IO - -namespace FS - -/-- -Reads the entire contents of the binary file at the given path as an array of bytes. --/ -def readBinFile (fname : FilePath) : IO ByteArray := do - -- Requires metadata so defined after metadata - let mdata ← fname.metadata - let size := mdata.byteSize.toUSize - let handle ← IO.FS.Handle.mk fname .read - let buf ← - if size > 0 then - handle.read mdata.byteSize.toUSize - else - pure <| ByteArray.emptyWithCapacity 0 - handle.readBinToEndInto buf - -/-- -Reads the entire contents of the UTF-8-encoded file at the given path as a `String`. - -An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to -exceptions that may always be thrown as a result of failing to read files. --/ -def readFile (fname : FilePath) : IO String := do - let data ← readBinFile fname - match String.fromUTF8? data with - | some s => return s - | none => throw <| .userError s!"Tried to read file '{fname}' containing non UTF-8 data." - -end FS - -/-- -Runs an action with the specified stream `h` as standard input, restoring the original standard -input stream afterwards. --/ -def withStdin [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do - let prev ← setStdin h - try x finally discard <| setStdin prev - -/-- -Runs an action with the specified stream `h` as standard output, restoring the original standard -output stream afterwards. --/ -def withStdout [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do - let prev ← setStdout h - try - x - finally - discard <| setStdout prev - -/-- -Runs an action with the specified stream `h` as standard error, restoring the original standard -error stream afterwards. --/ -def withStderr [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : FS.Stream) (x : m α) : m α := do - let prev ← setStderr h - try x finally discard <| setStderr prev - -/-- -Converts `s` to a string using its `ToString α` instance, and prints it to the current standard -output (as determined by `IO.getStdout`). --/ -def print [ToString α] (s : α) : IO Unit := do - let out ← getStdout - out.putStr <| toString s - -/-- -Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to -the current standard output (as determined by `IO.getStdout`). --/ -def println [ToString α] (s : α) : IO Unit := - print ((toString s).push '\n') - -/-- -Converts `s` to a string using its `ToString α` instance, and prints it to the current standard -error (as determined by `IO.getStderr`). --/ -def eprint [ToString α] (s : α) : IO Unit := do - let out ← getStderr - out.putStr <| toString s - -/-- -Converts `s` to a string using its `ToString α` instance, and prints it with a trailing newline to -the current standard error (as determined by `IO.getStderr`). --/ -def eprintln [ToString α] (s : α) : IO Unit := - eprint <| toString s |>.push '\n' - -@[export lean_io_eprint] -private def eprintAux (s : String) : IO Unit := - eprint s - -@[export lean_io_eprintln] -private def eprintlnAux (s : String) : IO Unit := - eprintln s - -/-- -Returns the directory that the current executable is located in. --/ -def appDir : IO FilePath := do - let p ← appPath - let some p ← pure p.parent - | throw <| IO.userError s!"IO.appDir: unexpected filename '{p}'" - FS.realPath p - -namespace FS - -/-- -Creates a directory at the specified path, creating all missing parents as directories. --/ -partial def createDirAll (p : FilePath) : IO Unit := do - if ← p.isDir then - return () - if let some parent := p.parent then - createDirAll parent - try - createDir p - catch - | e => - if ← p.isDir then - pure () -- I guess someone else was faster - else - throw e - -/-- -Fully remove given directory by deleting all contained files and directories in an unspecified order. -Symlinks are deleted but not followed. Fails if any contained entry cannot be deleted or was newly -created during execution. --/ -partial def removeDirAll (p : FilePath) : IO Unit := do - for ent in (← p.readDir) do - -- Do not follow symlinks - if (← ent.path.symlinkMetadata).type == .dir then - removeDirAll ent.path - else - removeFile ent.path - removeDir p - -/-- -Creates a temporary file in the most secure manner possible and calls `f` with both a `Handle` to -the already-opened file and its path. Afterwards, the temporary file is deleted. - -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. - -Use `IO.FS.createTempFile` to avoid the automatic deletion of the temporary file. --/ -def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → FilePath → m α) : - m α := do - let (handle, path) ← createTempFile - try - f handle path - finally - removeFile path - -/-- -Creates a temporary directory in the most secure manner possible, providing a its path to an `IO` -action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how -or when they were created. - -There are no race conditions in the directory’s creation. The directory is readable and writable -only by the creating user ID. Use `IO.FS.createTempDir` to avoid the automatic deletion of the -directory's contents. --/ -def withTempDir [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : FilePath → m α) : - m α := do - let path ← createTempDir - try - f path - finally - removeDirAll path - -end FS - -namespace Process - -/-- Returns the current working directory of the calling process. -/ -@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath - -/-- Sets the current working directory of the calling process. -/ -@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit - -/-- Returns the process ID of the calling process. -/ -@[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32 - -/-- -Whether the standard input, output, and error handles of a child process should be attached to -pipes, inherited from the parent, or null. - -If the stream is a pipe, then the parent process can use it to communicate with the child. --/ -inductive Stdio where - /-- The stream should be attached to a pipe. -/ - | piped - /-- The stream should be inherited from the parent process. -/ - | inherit - /-- The stream should be empty. -/ - | null - -/-- -The type of handles that can be used to communicate with a child process on its standard input, -output, or error streams. - -For `IO.Process.Stdio.piped`, this type is `IO.FS.Handle`. Otherwise, it is `Unit`, because no -communication is possible. --/ -@[expose] def Stdio.toHandleType : Stdio → Type - | Stdio.piped => FS.Handle - | Stdio.inherit => Unit - | Stdio.null => Unit - -/-- -Configuration for the standard input, output, and error handles of a child process. --/ -structure StdioConfig where - /-- Configuration for the process' stdin handle. -/ - stdin := Stdio.inherit - /-- Configuration for the process' stdout handle. -/ - stdout := Stdio.inherit - /-- Configuration for the process' stderr handle. -/ - stderr := Stdio.inherit - -/-- -Configuration for a child process to be spawned. - -Use `IO.Process.spawn` to start the child process. `IO.Process.output` and `IO.Process.run` can be -used when the child process should be run to completion, with its output and/or error code captured. --/ -structure SpawnArgs extends StdioConfig where - /-- Command name. -/ - cmd : String - /-- Arguments for the command. -/ - args : Array String := #[] - /-- The child process's working directory. Inherited from the parent current process if `none`. -/ - cwd : Option FilePath := none - /-- - Add or remove environment variables for the child process. - - The child process inherits the parent's environment, as modified by `env`. Keys in the array are - the names of environment variables. A `none`, causes the entry to be removed from the environment, - and `some` sets the variable to the new value, adding it if necessary. Variables are processed from left to right. - -/ - env : Array (String × Option String) := #[] - /-- Inherit environment variables from the spawning process. -/ - inheritEnv : Bool := true - /-- - Starts the child process in a new session and process group using `setsid`. Currently a no-op on - non-POSIX platforms. - -/ - setsid : Bool := false - -/-- -A child process that was spawned with configuration `cfg`. - -The configuration determines whether the child process's standard input, standard output, and -standard error are `IO.FS.Handle`s or `Unit`. --/ -structure Child (cfg : StdioConfig) where private mk :: - /-- - The child process's standard input handle, if it was configured as `IO.Process.Stdio.piped`, or - `()` otherwise. - -/ - stdin : cfg.stdin.toHandleType - /-- - The child process's standard output handle, if it was configured as `IO.Process.Stdio.piped`, or - `()` otherwise. - -/ - stdout : cfg.stdout.toHandleType - /-- - The child process's standard error handle, if it was configured as `IO.Process.Stdio.piped`, or - `()` otherwise. - -/ - stderr : cfg.stderr.toHandleType - -/-- -Starts a child process with the provided configuration. The child process is spawned using operating -system primitives, and it can be written in any language. - -The child process runs in parallel with the parent. - -If the child process's standard input is a pipe, use `IO.Process.Child.takeStdin` to make it -possible to close the child's standard input before the process terminates, which provides the child with an end-of-file marker. --/ -@[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig) - -/-- -Blocks until the child process has exited and return its exit code. --/ -@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32 - -/-- -Checks whether the child has exited. Returns `none` if the process has not exited, or its exit code -if it has. --/ -@[extern "lean_io_process_child_try_wait"] opaque Child.tryWait {cfg : @& StdioConfig} : @& Child cfg → - IO (Option UInt32) - -/-- -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_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit - -/-- -Extracts the `stdin` field from a `Child` object, allowing the handle to be closed while maintaining -a reference to the child process. - -File handles are closed when the last reference to them is dropped. Closing the child's standard -input causes an end-of-file marker. Because the `Child` object has a reference to the standard -input, this operation is necessary in order to close the stream while the process is running (e.g. -to extract its exit code after calling `Child.wait`). Many processes do not terminate until their -standard input is exhausted. --/ -@[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg → - IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null }) - -/-- Returns the operating system process id of the child process. -/ -@[extern "lean_io_process_child_pid"] opaque Child.pid {cfg : @& StdioConfig} : Child cfg → UInt32 - -/-- -The result of running a process to completion. --/ -structure Output where - /-- The process's exit code. -/ - exitCode : UInt32 - /-- Everything that was written to the process's standard output. -/ - stdout : String - /-- Everything that was written to the process's standard error. -/ - stderr : String - -/-- -Runs a process to completion and captures its output and exit code. -The child process is run with a null standard input or the specified input if provided, -and the current process blocks until it has run to completion. - -The specifications of standard input, output, and error handles in `args` are ignored. --/ -def output (args : SpawnArgs) (input? : Option String := none) : IO Output := do - let child ← - if let some input := input? then - let (stdin, child) ← (← spawn { args with stdout := .piped, stderr := .piped, stdin := .piped }).takeStdin - stdin.putStr input - stdin.flush - pure child - else - spawn { args with stdout := .piped, stderr := .piped, stdin := .null } - let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated - let stderr ← child.stderr.readToEnd - let exitCode ← child.wait - let stdout ← IO.ofExcept stdout.get - pure { exitCode := exitCode, stdout := stdout, stderr := stderr } - -/-- -Runs a process to completion, blocking until it terminates. -The child process is run with a null standard input or the specified input if provided, -If the child process terminates successfully with exit code 0, its standard output is returned. -An exception is thrown if it terminates with any other exit code. - -The specifications of standard input, output, and error handles in `args` are ignored. --/ -def run (args : SpawnArgs) (input? : Option String := none) : IO String := do - let out ← output args input? - if out.exitCode != 0 then - throw <| IO.userError s!"process '{args.cmd}' exited with code {out.exitCode}\ - \nstderr:\ - \n{out.stderr}" - pure out.stdout - -/-- -Terminates the current process with the provided exit code. `0` indicates success, all other values -indicate failure. --/ -@[extern "lean_io_exit"] opaque exit : UInt8 → IO α - -/-- -Terminates the current process with the provided exit code. `0` indicates success, all other values -indicate failure. - -Calling this function is equivalent to calling -[`std::_Exit`](https://en.cppreference.com/w/cpp/utility/program/_Exit.html). --/ -@[extern "lean_io_force_exit"] opaque forceExit : UInt8 → IO α - -end Process - -/-- Returns the thread ID of the calling thread. -/ -@[extern "lean_io_get_tid"] opaque getTID : BaseIO UInt64 - -/-- -POSIX-style file permissions. - -The `FileRight` structure describes these permissions for a file's owner, members of it's designated -group, and all others. --/ -structure AccessRight where - /-- The file can be read. -/ - read : Bool := false - /-- The file can be written to. -/ - write : Bool := false - /-- The file can be executed. -/ - execution : Bool := false - -/-- -Converts individual POSIX-style file permissions to their conventional three-bit representation. - -This is the bitwise `or` of the following: - * If the file can be read, `0x4`, otherwise `0`. - * If the file can be written, `0x2`, otherwise `0`. - * If the file can be executed, `0x1`, otherwise `0`. - -Examples: - * `{read := true : AccessRight}.flags = 4` - * `{read := true, write := true : AccessRight}.flags = 6` - * `{read := true, execution := true : AccessRight}.flags = 5` --/ -def AccessRight.flags (acc : AccessRight) : UInt32 := - let r : UInt32 := if acc.read then 0x4 else 0 - let w : UInt32 := if acc.write then 0x2 else 0 - let x : UInt32 := if acc.execution then 0x1 else 0 - r.lor <| w.lor x - -/-- -POSIX-style file permissions that describe access rights for a file's owner, members of its -assigned group, and all others. --/ -structure FileRight where - /-- The owner's permissions to access the file. -/ - user : AccessRight := {} - /-- The assigned group's permissions to access the file. -/ - group : AccessRight := {} - /-- The permissions that all others have to access the file. -/ - other : AccessRight := {} - -/-- -Converts POSIX-style file permissions to their numeric representation, with three bits each for the -owner's permissions, the group's permissions, and others' permissions. --/ -def FileRight.flags (acc : FileRight) : UInt32 := - let u : UInt32 := acc.user.flags.shiftLeft 6 - let g : UInt32 := acc.group.flags.shiftLeft 3 - let o : UInt32 := acc.other.flags - u.lor <| g.lor o - -@[extern "lean_chmod"] opaque Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit - -/-- -Sets the POSIX-style permissions for a file. --/ -def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit := - Prim.setAccessRights filename mode.flags - -/-- -Mutable reference cells that contain values of type `α`. These cells can read from and mutated in -the `IO` monad. --/ -abbrev Ref (α : Type) := ST.Ref IO.RealWorld α - -instance : MonadLift (ST IO.RealWorld) BaseIO where - monadLift mx := fun s => - match mx s with - | .mk s a => .mk s a - -/-- -Creates a new mutable reference cell that contains `a`. --/ -def mkRef (a : α) : BaseIO (IO.Ref α) := - ST.mkRef a - -/-- -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. --/ -structure CancelToken where - private ref : IO.Ref Bool -deriving Nonempty - -namespace CancelToken - -/-- Creates a new cancellation token. -/ -def new : BaseIO CancelToken := - CancelToken.mk <$> IO.mkRef false - -/-- Activates a cancellation token. Idempotent. -/ -def set (tk : CancelToken) : BaseIO Unit := - tk.ref.set true - -/-- Checks whether the cancellation token has been activated. -/ -def isSet (tk : CancelToken) : BaseIO Bool := - tk.ref.get - --- separate definition as otherwise no unboxed version is generated -@[export lean_io_cancel_token_is_set] -private def isSetExport := @isSet - -end CancelToken - -namespace FS -namespace Stream - -/-- -Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding -file handle operation. --/ -@[export lean_stream_of_handle] -def ofHandle (h : Handle) : Stream where - flush := Handle.flush h - read := Handle.read h - write := Handle.write h - getLine := Handle.getLine h - putStr := Handle.putStr h - isTty := Handle.isTty h - -/-- -A byte buffer that can simulate a file in memory. - -Use `IO.FS.Stream.ofBuffer` to create a stream from a buffer. --/ -structure Buffer where - /-- The contents of the buffer. -/ - data : ByteArray := ByteArray.empty - /-- The read/write cursor's position in the buffer. -/ - pos : Nat := 0 - -/-- -Creates a stream from a mutable reference to a buffer. - -The resulting stream simulates a file, mutating the contents of the reference in response to writes -and reading from it in response to reads. These streams can be used with `IO.withStdin`, -`IO.setStdin`, and the corresponding operators for standard output and standard error to redirect -input and output. --/ -def ofBuffer (r : Ref Buffer) : Stream where - flush := pure () - read := fun n => r.modifyGet fun b => - let data := b.data.extract b.pos (b.pos + n.toNat) - (data, { b with pos := b.pos + data.size }) - write := fun data => r.modify fun b => - -- set `exact` to `false` so that repeatedly writing to the stream does not impose quadratic run time - { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size } - getLine := do - let buf ← r.modifyGet fun b => - let pos := match b.data.findIdx? (start := b.pos) fun u => u == 0 || u = '\n'.toNat.toUInt8 with - -- include '\n', but not '\0' - | some pos => if b.data.get! pos == 0 then pos else pos + 1 - | none => b.data.size - (b.data.extract b.pos pos, { b with pos := pos }) - match String.fromUTF8? buf with - | some str => pure str - | none => throw (.userError "invalid UTF-8") - putStr := fun s => r.modify fun b => - let data := s.toUTF8 - { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size } - isTty := pure false - -/-- -Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is -encountered. - -The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from -the stream may block and/or return data. --/ -partial def readBinToEndInto (s : Stream) (buf : ByteArray) : IO ByteArray := do - let rec loop (acc : ByteArray) : IO ByteArray := do - let buf ← s.read 1024 - if buf.isEmpty then - return acc - else - loop (acc ++ buf) - loop buf - -/-- -Reads the entire remaining contents of the stream until an end-of-file marker (EOF) is -encountered. - -The underlying stream is not automatically closed upon encountering an EOF, and subsequent reads from -the stream may block and/or return data. --/ -def readBinToEnd (s : Stream) : IO ByteArray := do - s.readBinToEndInto .empty - -/-- -Reads the entire remaining contents of the stream as a UTF-8-encoded string. An exception is -thrown if the contents are not valid UTF-8. - -The underlying stream is not automatically closed, and subsequent reads from the stream may block -and/or return data. --/ -def readToEnd (s : Stream) : IO String := do - let data ← s.readBinToEnd - match String.fromUTF8? data with - | some s => return s - | none => throw <| .userError s!"Tried to read from stream containing non UTF-8 data." - -/-- -Reads the entire remaining contents of the stream as a UTF-8-encoded array of lines. - -Newline markers are not included in the lines. - -The underlying stream is not automatically closed, and subsequent reads from the stream may block -and/or return data. --/ -partial def lines (s : Stream) : IO (Array String) := do - let rec read (lines : Array String) := do - let line ← s.getLine - if line.length == 0 then - pure lines - else if line.back == '\n' then - let line := line.dropEnd 1 |>.copy - let line := if line.back == '\r' then line.dropEnd 1 |>.copy else line - read <| lines.push line - else - pure <| lines.push line - read #[] - -end Stream - -/-- -Runs an action with `stdin` emptied and `stdout` and `stderr` captured into a `String`. If -`isolateStderr` is `false`, only `stdout` is captured. --/ -def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α) - (isolateStderr := true) : m (String × α) := do - let bIn ← mkRef { : Stream.Buffer } - let bOut ← mkRef { : Stream.Buffer } - let r ← withStdin (Stream.ofBuffer bIn) <| - withStdout (Stream.ofBuffer bOut) <| - (if isolateStderr then withStderr (Stream.ofBuffer bOut) else id) <| - x - let bOut ← liftM (m := BaseIO) bOut.get - let out := String.fromUTF8! bOut.data - pure (out, r) - -end FS -end IO - -syntax "println! " (interpolatedStr(term) <|> term) : term - -macro_rules - | `(println! $msg:interpolatedStr) => `((IO.println (s! $msg) : IO Unit)) - | `(println! $msg:term) => `((IO.println $msg : IO Unit)) - /-- Marks given value and its object graph closure as multi-threaded if currently marked single-threaded. This will make reference counter updates atomic and diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean index bb96623da6e0..ec9e3bc4d890 100644 --- a/src/Lean/Compiler/IR/LLVMBindings.lean +++ b/src/Lean/Compiler/IR/LLVMBindings.lean @@ -7,6 +7,7 @@ module prelude public import Init.System.IO +import Init.Data.Ord.UInt public section diff --git a/src/Lean/Data/Json/FromToJson/Basic.lean b/src/Lean/Data/Json/FromToJson/Basic.lean index 6c2de035748e..aafd099cc419 100644 --- a/src/Lean/Data/Json/FromToJson/Basic.lean +++ b/src/Lean/Data/Json/FromToJson/Basic.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Data.Json.Printer +public import Init.System.Files public section diff --git a/src/Lean/Data/Json/Stream.lean b/src/Lean/Data/Json/Stream.lean index d8ed241a6190..a35b9db5ba9d 100644 --- a/src/Lean/Data/Json/Stream.lean +++ b/src/Lean/Data/Json/Stream.lean @@ -9,6 +9,7 @@ module prelude public import Lean.Data.Json.Parser public import Lean.Data.Json.Printer +public import Init.System.Files public section diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 90889ade1fb3..8e888e6a9a2d 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -7,6 +7,7 @@ module prelude public import Lean.Expr +import Init.Data.Ord.UInt public section diff --git a/src/Lean/DocString/Links.lean b/src/Lean/DocString/Links.lean index f68c6131edbd..758ebb6a4cf5 100644 --- a/src/Lean/DocString/Links.lean +++ b/src/Lean/DocString/Links.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Syntax +public import Init.System.Files import Init.Data.String.TakeDrop import Init.Data.String.Search diff --git a/src/Lean/LoadDynlib.lean b/src/Lean/LoadDynlib.lean index ee648f1fe7a8..e120c5279805 100644 --- a/src/Lean/LoadDynlib.lean +++ b/src/Lean/LoadDynlib.lean @@ -6,7 +6,7 @@ Authors: Mac Malone module prelude -public import Init.System.IO +public import Init.System.Files import Init.Data.String.TakeDrop public section diff --git a/src/Lean/Server/ServerTask.lean b/src/Lean/Server/ServerTask.lean index d755c14b39e3..9a7492ec4052 100644 --- a/src/Lean/Server/ServerTask.lean +++ b/src/Lean/Server/ServerTask.lean @@ -7,6 +7,7 @@ module prelude public import Init.Task +public import Init.System.Files public section diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean index 6c461d4e84cf..414b8bd88cea 100644 --- a/src/Lean/ToExpr.lean +++ b/src/Lean/ToExpr.lean @@ -7,6 +7,7 @@ module prelude public import Lean.ToLevel public import Init.Data.Rat.Basic +public import Init.System.FilePath public section universe u namespace Lean diff --git a/src/Lean/Util/LakePath.lean b/src/Lean/Util/LakePath.lean index e361d1a9c2df..6748f7302919 100644 --- a/src/Lean/Util/LakePath.lean +++ b/src/Lean/Util/LakePath.lean @@ -7,7 +7,7 @@ Authors: Sebastian Ullrich module prelude -public import Init.System.IO +public import Init.System.Files public section diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean index f4b17e80977a..d446728f41d4 100644 --- a/src/Lean/Util/Path.lean +++ b/src/Lean/Util/Path.lean @@ -11,7 +11,7 @@ with a directory `A/`. `import A` resolves to `path/A.olean`. module prelude -public import Init.System.IO +public import Init.System.Files import Init.Data.ToString.Name import Init.Data.String.TakeDrop diff --git a/src/Leanc.lean b/src/Leanc.lean index da517a3bf8a1..51c84d060e10 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ import Lean.Compiler.FFI +import Init.System.Files open Lean.Compiler.FFI diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index 0734c92a6c4b..a6e4ad71c9e3 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -7,6 +7,7 @@ module prelude public import Init.System.Promise +public import Init.System.Files public section diff --git a/src/Std/Sync/Basic.lean b/src/Std/Sync/Basic.lean index 5ab335875a87..00d4c5bc50d2 100644 --- a/src/Std/Sync/Basic.lean +++ b/src/Std/Sync/Basic.lean @@ -7,6 +7,7 @@ module prelude public import Init.System.IO +public import Init.Control.StateRef @[expose] public section diff --git a/src/Std/Tactic/BVDecide/LRAT/Parser.lean b/src/Std/Tactic/BVDecide/LRAT/Parser.lean index 0d5060217482..27bd637f9d39 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Parser.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Parser.lean @@ -6,7 +6,7 @@ Authors: Henrik Böving module prelude -public import Init.System.IO +public import Init.System.Files public import Std.Tactic.BVDecide.LRAT.Actions public import Std.Internal.Parsec diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index a523f3e0b202..7c554aa1cb42 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -7,6 +7,7 @@ module prelude public import Std.Time.Zoned.Database.Basic +public import Init.System.Files import Init.Data.String.TakeDrop public section diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean index 65214e61f570..d177eb3ef250 100644 --- a/src/lake/Lake/Util/IO.lean +++ b/src/lake/Lake/Util/IO.lean @@ -6,7 +6,7 @@ Authors: Mac Malone module prelude -public import Init.System.IO +public import Init.System.Files open System diff --git a/src/lake/Lake/Util/Lift.lean b/src/lake/Lake/Util/Lift.lean index 6b08b0b87671..03d40ac06ee7 100644 --- a/src/lake/Lake/Util/Lift.lean +++ b/src/lake/Lake/Util/Lift.lean @@ -7,6 +7,7 @@ module prelude public import Init.System.IO +public import Init.Control.Option namespace Lake diff --git a/src/lake/Lake/Util/Lock.lean b/src/lake/Lake/Util/Lock.lean index 3add8744d094..48fcdb27608b 100644 --- a/src/lake/Lake/Util/Lock.lean +++ b/src/lake/Lake/Util/Lock.lean @@ -6,7 +6,7 @@ Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich module prelude -public import Init.System.IO +public import Init.System.Files /-! # Lock File Utilities diff --git a/src/lake/Lake/Util/NativeLib.lean b/src/lake/Lake/Util/NativeLib.lean index 0582848a1154..087990617e5c 100644 --- a/src/lake/Lake/Util/NativeLib.lean +++ b/src/lake/Lake/Util/NativeLib.lean @@ -6,7 +6,7 @@ Authors: Mac Malone module prelude -public import Init.System.IO +public import Init.System.Files open System namespace Lake diff --git a/tests/lean/file_not_found.lean b/tests/lean/file_not_found.lean index 4f0666e9bbdb..e7da7cc89657 100644 --- a/tests/lean/file_not_found.lean +++ b/tests/lean/file_not_found.lean @@ -1,5 +1,5 @@ prelude -import Init.System.IO +import Init.System.Files open IO.FS def usingIO {α} (x : IO α) : IO α := x diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean index 392758906033..b254ebbc8621 100644 --- a/tests/lean/run/IO_test.lean +++ b/tests/lean/run/IO_test.lean @@ -1,5 +1,5 @@ prelude -import Init.System.IO +import Init.System.Files import Init.Data.List.Control import Init.Data.ToString