		Search-engine friendly clone of the ACL2 documentation.

Best-practices

File-names

Restrictions to follow for naming books, directories, and other files.

Recommendations

All file names and directory should use strictly lower-case, printable ASCII letters.
Spaces and odd punctuation characters (e.g., beyond dash, underscore, and period) should not be used.
Dashes should generally be preferred over underscores.

Rationale

These name restrictions encourage portability across different operating systems, file systems, etc. (Some file systems restrict certain characters, or differ from one another with respect to case sensitivity.)

Avoiding file names with spaces and special characters helps to makes it easier to write scripts or to write quick, one-off shell commands to process the books without worrying overly much about escaping.