must-fail

(in-package "ACL2")

(defxdoc must-fail
  :parents (std/testing errors)
  :short "A top-level @(see assert$)-like command.  Ensures that a command
which returns an @(see error-triple)—e.g., @(see defun) or @(see
defthm)—will not be successful."
  :long "<p>This can be useful for adding simple unit tests of macros,
theories, etc. to your books.  Basic examples:</p>

@({
    (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)
})

<p>Must-fail is almost just like @(see 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.</p>

<p>Also see @(see must-fail-with-error), @(see must-fail-with-soft-error), and
@(see must-fail-with-hard-error), which are essentially aliases for
@('must-fail') with different values for the option, @(':expected'), which we
now describe.</p>

<p>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 @(tsee illegal) and @(tsee hard-error), and by
calls of @(tsee 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.</p>

<p>CAVEAT: If a book contains a non-@(see 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 @(tsee include-book), and any @('thm') will succeed if proofs are
skipped.  One fix is to make such forms @(see local).  Another fix is to use a
wrapper @(tsee 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
@(tsee make-event)).</p>")