|
|
|---|
|
|
|
|---|
Functions for working with file types, e.g., regular files versus directories, devices, etc.
Many of these functions are just ACL2 wrappers for the Common Lisp Osicat library. Unlike the more basic file reading/writing operations (see ACL2::std/io), there is no complex logical story for reasoning about these operations. Instead, in the logic, practically everything here is just reading the oracle.
As a general rule, these functions are not entirely portable,
especially regarding special characters like
Some possibly helpful reading about file systems in general and in Lisp:
BOZO I would really like to have tests like -r, -w, and -x in Perl/Bash. It looks like osicat gives me a way to access the permissions of a file, but these seem like just the rwx bits from the "stat" structure, and I don't think that's actually tells us anything useful, unless the file happens to be owned by us---at least, not without some way to figure out what groups our user is in, etc.
The source code for Gnu's "test" utility (from coreutils) invokes the EUIDACCESS system call to figure out whether the argument is readable, writable, or executable. So that'd probably be the nicest thing to use. So maybe we could rig something up with CFFI to invoke that, but I am in way over my head here, and even if we did that, it'd probably just be a solution for Linux. Who knows how Windows or FreeBSD or Darwin or anything else do it.