• Top
  • Documentation
  • Books
    • Cert.pl
    • Community-books
    • Project-dir-alist
    • Bookdata
    • Uncertified-books
    • Book-hash
    • Sysfile
    • Show-books
    • Best-practices
    • Books-reference
      • Include-book
      • Certify-book
      • Cbd
      • Set-write-ACL2x
      • Book-compiled-file
      • Add-include-book-dir
      • Pathname
      • With-current-package
      • Add-include-book-dir!
      • Full-book-name
      • Delete-include-book-dir
      • With-cbd
      • Delete-include-book-dir!
      • Set-cbd
      • Certify-book-debug
    • 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

• Books

Books-reference

Reference guide for ACL2 functionality related to books, e.g., include-book, certify-book, cbd, etc.

Subtopics

Include-book

Load the events in a file

Certify-book

How to produce a certificate for a book

Cbd

Connected book directory string

Set-write-ACL2x

Cause certify-book to write out a .acl2x file

Book-compiled-file

Creating and loading of compiled and expansion files for books

Add-include-book-dir

Link keyword for :dir argument of ld and include-book

Pathname

Introduction to filename conventions in ACL2

With-current-package

To bind the current-package

Add-include-book-dir!

Non-locally link keyword for :dir argument of ld and include-book

Full-book-name

Book naming conventions assumed by ACL2

Delete-include-book-dir

Unlink keyword for :dir argument of ld and include-book

With-cbd

To bind the connected book directory

Delete-include-book-dir!

Non-locally unlink keyword for :dir argument of ld and include-book

Set-cbd

To set the connected book directory

Certify-book-debug

Some possible ways to work around certify-book failures