• Top
    • Documentation
    • Books
      • Cert.pl
        • Cert_param
        • Preliminaries
        • Using-extended-ACL2-images
        • Distributed-builds
        • Certifying-simple-books
        • Pre-certify-book-commands
        • ACL2-system-feature-dependencies
        • Static-makefiles
        • Optimizing-build-time
        • Raw-lisp-and-other-dependencies
        • Custom-certify-book-commands
        • Include-events
          • Ifdef
          • Ifdef-define
          • Ifndef
          • Ifdef-undefine
          • Ifdef-undefine!
          • Ifdef-define!
          • Include-src-events
        • Community-books
        • Project-dir-alist
        • Bookdata
        • Uncertified-books
        • Book-hash
        • Sysfile
        • Show-books
        • Best-practices
        • Books-reference
        • Where-do-i-place-my-book
        • Books-tour
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Cert.pl

    Include-events

    A build-system-supported mechanism to include the events from a book as a progn or encapsulate.

    Include-events reads the forms from a source file, which must begin with an in-package form, and submits those forms as a progn or encapsulate.

    Usage:

    (include-book "build/include-events" :dir :system) ;; prerequisite
    
    (include-events "book-name" :dir :system :encapsulate nil)

    The :dir argument works just like it does in include-book. The :encapsulate argument says whether to submit the forms contained in the book as a progn (if nil) or encapsulate nil (if t).

    The name of the actual file to be loaded will be the filename argument with ".lisp" appended. The related include-src-events does the same thing without adding the extension.

    The events read from the file are run in the current book's context. Among other things, this means that the connected book directory (see cbd) remains the directory of the current book, not that of the loaded file, unless it is the same directory. Include-event tries to compensate for this by rewriting include-book, include-event, and include-src-events forms to correct the filenames.

    The cert.pl build system supports this in that if this form is in a book, it creates dependencies from that book on the source file that is included as well as any additional dependencies found in that source file.

    If a library has a book "top" that only includes other books, then "top" could be included via include-events rather than include-book to save certification time.