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)"