Must-fail
A top-level assert$-like command. Ensures that a command
which returns an error-triple—e.g., defun or defthm—will not be successful.
This can be useful for adding simple unit tests of macros,
theories, etc. to your books. Basic examples:
(must-fail ;; succeeds
(defun 5)) ;; (invalid defun will indeed fail)
(must-fail ;; causes an error
(thm t)) ;; (because this thm proves fine)
(must-fail (mv nil (hard-error 'foo "MESSAGE" nil) state))
;; causes an error
;; (because hard errors propagate past
;; must-fail by default)
(must-fail (mv nil (hard-error 'foo "MESSAGE" nil) state)
:expected :hard) ;; succeeds
(must-fail ;; causes an error
(in-theory (enable floor))) ;; (because this works fine)
(must-fail ;; causes an error
(* 3 4)) ;; (doesn't return an error triple)
Must-fail is almost just like must-succeed, except that the event is
expected to fail instead of succeed. The option :expected is described
below; for everything else, please see the documentation for must-succeed
for syntax, options, and additional discussion.
Also see must-fail-with-error, must-fail-with-soft-error, and
must-fail-with-hard-error, which are essentially aliases for
must-fail with different values for the option, :expected, which we
now describe.
When the value of keyword :expected is :any, then must-fail
succeeds if and only if ACL2 causes an error during evaluation of the supplied
form. However :expected is :soft by default, in which case success
requires that the error is ``soft'', not ``hard'': hard errors are caused by
guard violations, by calls of illegal and hard-error, and by
calls of er that are not ``soft''. Finally, if :expected is
:hard, then the call of must-fail succeeds if and only if evaluation
of the form causes a hard error.
CAVEAT: If a book contains a non-local form that causes proofs to be
done, such as one of the form (must-fail (thm ...)), then it might not be
possible to include that book. That is because proofs are generally skipped
during include-book, and any thm will succeed if proofs are
skipped. One fix is to make such forms local. Another fix is to use a
wrapper must-fail! that creates a call of must-fail with
:check-expansion to t; that causes proofs to be done even when
including a book (because of the way that must-fail is implemented using
make-event).
Subtopics
- Must-fail-with-soft-error
- A specialization of must-fail to ensure that
a soft error occurs.
- Must-fail-with-hard-error
- A specialization of must-fail to ensure that
a hard error occurs.
- Must-fail-with-error
- A specialization of must-fail to ensure that an error occurs.
- Must-fail-local
- A local variant of must-fail.
