Reporting Bugs
Use the built-in bug-reporting feature of DrScheme. Under the Help menu, choose Submit Bug Report. Fill in all of the requested information and then click Submit.
Use the built-in bug-reporting feature of DrScheme. Under the Help menu, choose Submit Bug Report. Fill in all of the requested information and then click Submit.
We support all of the documented primitive procedures of ACL2, and we support a limited subset of the events / special forms.
For details, search Help Desk for acl2 and follow the first link under the ACL2 Language collection. Scroll down to the Supported Forms section.
If you find that we have omitted or restricted a feature that you cannot do without, then please submit a Bug Report and we will do our best to accommodate your request. Also, note that the code ships with the distribution -- contributions are welcome!
Scheme-side reader understands numbers like 0.42 and 3+2i, but ACL2 does not.
The functions from the World teachpack are not defined in ACL2, but they are constrained (using encapsulate). You can therefore use ACL2 to reason about code that uses the world teachpack. Note though that the specification currently exposed doesn't allow one to state anything interesting about functions that manipulate images.
As a corollary of the above, ACL2 cannot cope with code like (defconst *an-image* (empty-scene 0 0)) because it cannot execute (empty-scene 0 0). The error message that occurs when this kind of code is present is somewhat confusing.
The workaround is simple: instead of defconst, use defun to define a constant function:
(defun (an-image) (empty-scene 0 0))