Oslib
Operating System Utilities Library
This is a collection of ACL2 functions that allow you to do various
basic operating-system related tasks, e.g., you can get the current PID or user
name, file listings, etc.
Almost everything here necessarily requires a trust tag, because it is
implemented in raw Lisp. We believe we have connected this functionality to
ACL2 in a sound way, using read-ACL2-oracle.
The library is far from complete since we tend to extend it only as the need
arises. Most functions are not implemented on all Lisp and operating system
combinations, and will simply fail on unsupported Lisps.
Please regard oslib as somewhat experimental. In the near future we may try
to standardize the interfaces of oslib functions to make them more
predictable.
Loading the library
You can load the full library with:
(include-book "oslib/top" :dir :system)
But you can alternately just pick out the specific books that you want to
load. The library has been arranged so that you can load only the logical
definitions without loading their associated raw Lisp code. For instance:
(include-book "oslib/argv" :dir :system)
;; -- requires a ttag, loads (argv) and its raw Lisp code
(include-book "oslib/argv-logic" :dir :system)
;; -- gets the logical definition of (argv)
;; -- no ttag, but of course the resulting (argv) won't work yet
Some users may find this to be useful, e.g., you can avoid trust tags in the
vast majority of your books, and only include the actual oslib raw Lisp code
when you're ready to run your ACL2 programs.
This paradigm is followed throughout the library. For instance, you can load
all oslib functions (without trust tags) using:
(include-book "oslib/top-logic" :dir :system)
But the resulting definitions won't work until you include the regular
top book.
Subtopics
- File-types
- Functions for working with file types, e.g., regular files versus
directories, devices, etc.
- Argv
- Get the "application level" command line arguments passed to ACL2.
- Copy
- Copy files or directories, with recoverable errors.
- Catpath
- Basic concatenation operation for paths.
- Ls
- Get a (full) directory listing.
- Universal-time
- Get the current timestamp as a natural number, specifically the
number of seconds since 00:00 January 1, 1900 GMT. Note well that this is
not the Unix epoch.
- Tempfile
- Generate a suitable name for a temporary file.
- Basename
- Remove the leading directory part from a path.
- Dirname
- Strip the non-directory suffix from a path.
- Copy!
- Copy files or directories, or cause a hard error.
- Ls-files
- Get a listing of only the regular files within a directory.
- Mkdir
- Make new directories if they don't already exist, like mkdir -p,
and return a success indicator so you can recover from errors.
- Rmtree
- Recursively delete files, like the shell command rm -rf, and
return a success indicator so you can recover from errors.
- Lisp-version
- Get a host-Lisp specific string describing the version number for
this Common Lisp implementation.
- Lisp-type
- Get a host-Lisp specific string describing what kind of Common Lisp
implementation this is.
- Ls-subdirs
- Get a listing of the subdirectories of a directory.
- Date
- Get the current datestamp, like "November 17, 2010 10:25:33".
- Getpid
- Get the current process identification (PID) number.
- Dirnames
- Strip non-directory suffixes from a list of file names.
- Basenames
- Removing leading directories from a list of paths.
- Basename!
- Remove the leading directory part of a path, or cause a hard error if
there is any problem.
- Ls-subdirs!
- Get a listing of the subdirectories of a directory, or cause a hard
error.
- Ls-files!
- Get a listing of only the regular files within a directory, or cause
a hard error.
- Dirname!
- Strip the non-directory suffix from a file name, or cause a hard
error if there is any problem.
- Ls!
- Get a (full) directory listing or cause a hard error.
- Catpaths
- Extend a base directory with many file names.
- Mkdir!
- Make new directories if they don't already exist, like mkdir -p,
or cause a hard error if there is any problem.
- Rmtree!
- Recursively delete files, like the shell command rm -rf, causing
a hard error on any failure.
- Remove-nonstrings
