[racket] Automating a program run in ACL2

Hey all.

I am required to periodically run a ACL2 program provided to me. Currently,
I open it up in DrRacket and just hit the run button, but I was hoping there
was some method of automating this process. (It's terribly slow)

I attempted to run the file through racket, but I get:

"default-load-handler: expected a `module' declaration for `main', found:
something else in: #<path:/home/nils/Dropbox/code/SE1/PSP/main.lisp>

 === context ===
standard-module-name-resolver"

I attempted to use the various flags, such as -r, -u and -f, some of which
give me an identical error, and others give me:

"reference to undefined identifier: in-package"

I attempted to also append the line "#lang ACL2" to the beginning of the
file, but it did not help.

Anyone have any advice?

Thanks, Nils

Also, here is the file:

main.lisp
"(in-package "ACL2")

(include-book "psp")

(set-state-ok t)
(main "input/" "output/" state)"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20100829/84a9b546/attachment.html>