• Top
    • Documentation
    • Books
      • Cert.pl
      • Community-books
      • Project-dir-alist
      • Bookdata
      • Book-hash
      • Uncertified-books
      • Sysfile
      • Show-books
      • Best-practices
        • Working-with-packages
        • Theory-management
        • Naming-rewrite-rules
        • Conventional-normal-forms
        • Where-do-i-place-my-book
        • File-names
        • File-extensions
          • Remove-whitespace
          • Finite-reasoning
        • Books-reference
        • Where-do-i-place-my-book
        • Books-tour
      • Recursion-and-induction
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Best-practices

    File-extensions

    Conventions to follow for choosing file extensions like .lisp, .lsp, and .acl2 files.

    Recommendations

    1. Certifiable books should use the extension .lisp
    2. Certification commands ("portcullis" stuff) should use the extension .acl2
    3. Other Lisp files (package definitions, raw lisp code) should that are not certifiable books should use .lsp

    Rationale

    These conventions allow build systems like build::cert.pl to automatically distinguish between what should be certified and what should not.

    Once a user is familiar with these conventions, they act as a signal about what files are likely to be of interest.