file: File Utilities

Table of Content:

Introduction

The file: module provides utilities for manipulating file objects.

Function usages are given in the same format as in the reference doc for the builtin module.

Functions

file:close

file:close $file

Closes a file opened with open.

See also file:open.

file:open

file:open $filename

Opens a file. Currently, open only supports opening a file for reading. File must be closed with close explicitly. Example:

~> cat a.txt
This is
a file.
~> use file
~> f = (file:open a.txt)
~> cat < $f
This is
a file.
~> close $f

See also file:close.

file:pipe

file:pipe

Create a new pipe that can be used in redirections. A pipe contains a read-end and write-end. Each pipe object is a pseudo-map with fields r (the read-end file object) and w (the write-end).

When redirecting command input from a pipe with <, the read-end is used. When redirecting command output to a pipe with >, the write-end is used. Redirecting both input and output with <> to a pipe is not supported.

Pipes have an OS-dependent buffer, so writing to a pipe without an active reader does not necessarily block. Pipes must be explicitly closed with file:close.

Putting values into pipes will cause those values to be discarded.

Examples (assuming the pipe has a large enough buffer):

~> p = (file:pipe)
~> echo 'lorem ipsum' > $p
~> head -n1 < $p
lorem ipsum
~> put 'lorem ipsum' > $p
~> file:close $p[w] # close the write-end
~> head -n1 < $p # blocks unless the write-end is closed
~> file:close $p[r] # close the read-end

See also file:close.

file:truncate

file:truncate $filename $size

changes the size of the named file. If the file is a symbolic link, it changes the size of the link’s target. The size must be an integer between 0 and 2^64-1.