Print files to a file set constant from a translation unit ensemble constant.
This macro takes as input the name of a named constant whose value is a translation unit ensemble (see transunit-ensemble), uses the printer to print the translation unit ensemble, which is the abstract syntax representation of a file set, to a file set (see fileset), and generates an ACL2 defconst with the file set.
This macro can be used before write-files, which writes a named constant containing a file set to files at the paths in the file set.
This macro currently does not perform very thorough input validation, but we plan to improve that.
(print-files :const-fileset ... ; no default :const-transunits ... ; no default )
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-fileset* be this symbol.
Name of the existing constant that contains the translation unit ensemble.
This must be a symbol that names an existing named constant, whose value must be a translation unit ensemble.
In the rest of this documentation page, let
*const-transunits* be this symbol.
The named constant containing the file set obtained by printing the translation unit ensemble in
*const-transunits* .