Print an error message and stop execution
(Hard-error ctx str alist) causes evaluation to halt with a
short message using the ``context'' ctx. An error message is first
printed using the string str and alist alist that are of the same
kind as expected by fmt. See fmt. Also see er for a
macro that provides a unified way of signaling errors.
Hard-error has a guard of t. Also see illegal for a
similar capability which however has a guard of nil that supports static
checking using guard verification, rather than using dynamic
(run-time) checking. This distinction is illustrated elsewhere: see prog2$ for examples.
Semantically, hard-error ignores its arguments and always returns
nil. But if a call (hard-error ctx str alist) is encountered during
evaluation, then the string str is printed using the association list
alist (as in fmt), after which evaluation halts immediately.
Here is a trivial, contrived example.
ACL2 !>(cons 3 (hard-error 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))))
HARD ACL2 ERROR in MY-CONTEXT: Printing 4: four
ACL2 Error in TOP-LEVEL: Evaluation aborted.
Technical note for raw Lisp programmers only. It is possible to cause hard
errors to signal actual raw Lisp errors, simply by evaluating the following
form in raw Lisp: (setq *hard-error-is-error* t). Indeed, any
non-nil value for *hard-error-is-error* will cause hard-error
or illegal — or indeed (er hard ...), (er hard! ...),
or (er hard? ...) — to produce a Lisp error whose condition, when
printed with format directive ~a, is the same error message that
ACL2 would otherwise print. Below is a sample log, closely based on an
example provided by Jared Davis.
ACL2 !>(defun f (x)
(er hard 'f "F got bad input ~x0.~%" x))
Since F is non-recursive, its admission is trivial. We observe that
the type of F is described by the theorem (EQUAL (F X) NIL). We used
the :type-prescription rule ILLEGAL.
Form: ( DEFUN F ...)
Rules: ((:TYPE-PRESCRIPTION ILLEGAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? (defun run-f ()
(let ((*hard-error-is-error* t))
(format t "Got the following error: ~a~%" condition)))))
Got the following error: HARD ACL2 ERROR in F: F got bad input 3.
Note that when a raw Lisp error occurs because *hard-error-is-error*
is non-nil, the error message will not use iprinting. The reason
is that the implementation does not make values of iprint indices available
after the message is printed; so it would be misleading or an error to read
#@i# after that return.
(defun hard-error (ctx str alist)
(declare (xargs :guard t))
(declare (ignore ctx str alist))