Hard-error
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.
ACL2 !>
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.
Summary
Form: ( DEFUN F ...)
Rules: ((:TYPE-PRESCRIPTION ILLEGAL))
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
? (defun run-f ()
(let ((*hard-error-is-error* t))
(handler-case
(f 3)
(error (condition)
(format t "Got the following error: ~a~%" condition)))))
RUN-F
? (run-f)
Got the following error: HARD ACL2 ERROR in F: F got bad input 3.
NIL
?
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.
Function: hard-error
(defun hard-error (ctx str alist)
(declare (xargs :guard t))
(declare (ignore ctx str alist))
nil)
