#lang scribble/doc
@(require scribble/manual scribble/eval "evaluator.ss"
          (for-label "../language/dracula.scm"))

@title[#:tag "include-book" #:style 'toc]{Books and Teachpacks}

@defform*[#:id include-book
          #:literals (:dir :system :teachpacks)
          [(include-book "<basename>")
           (include-book "<basename>" :dir :system)
           (include-book "<basename>" :dir :teachpacks)]]{

The @scheme[include-book] form imports definitions from a file called a
@deftech{book}.  Dracula supports three variants.

@schemeblock[(include-book "my-path/my-book")]
Without a @scheme[:dir] option, Dracula adds a ".lisp" extension to the base
name and attempts to load a file relative to the current directory.  In the case
above, the program must reside in a directory with a "my-path" subdirectory
containing a book named "my-book.lisp".

Books must be valid Dracula programs; they must start with
@scheme[(in-package "ACL2")]; and they must contain only events, no top-level
expressions.

@schemeblock[(include-book "my-path/my-book" :dir :system)]
This variant loads a book from the system directory included with an ACL2
installation.  Dracula simulates only a couple of the definitions from these
books, but allows other books to be included for theorem proving purposes.  See
below for the supported books.

@schemeblock[(include-book "my-path/my-book" :dir :teachpack)]
The third variant loads one of the books provided with Dracula, called
teachpacks.  These books make use of DrScheme features such as interactive
animations and other i/o, and are also reflected in the ACL2 logic.

}

@local-table-of-contents[]

@include-section["books.scrbl"]
@include-section["teachpacks.scrbl"]