Read files from the file system to a file set constant.
This macro takes as input a list of file paths, reads those files from the file system, and generates an ACL2 defconst containing a file set (see fileset) with the content of the given files. Optionally, this macro can use the preprocess-files tool to preprocess the given files prior to generating the constant, so that the constant will contain the preprocessed files.
This macro currently does not perform very thorough input validation, but we plan to improve that.
(read-files :const ... ; no default :files ... ; no default :preprocessor ... ; default nil )
Name of the generated constant that contains the file set.
This must be a symbol that is a valid name for a new named constant.
In the rest of this documentation page, let
*const* be this symbol.
List of zero or more file paths that specify the files to be read.
This must be a list of strings that are valid path names in the system. Non-absolute paths are relative to the connected book directory (see cbd).
This input to this macro is not evaluated.
Flag indicating the preprocessor to use, if any.
This must be
nil ,:auto , or a stringp.If this is a stringp, the preprocess-file tool is called on the files read at the file paths using the indicated preprocesser. If it is
:auto , we use the"cpp" preprocessor. If it isnil , we do not preprocess the files.
The named constant containing the file set obtained by reading, and optionally preprocessing, the files at the specified file paths.