Fp
Floating-point and ACL2
ACL2 supports computation that uses floating-point operations; see
df. If you are using an older Lisp, an attempt to build ACL2 may fail
with an error complaining that “feature :ieee-floating-point is
missing” [from the Lisp's *features*]. THIS ERROR INDICATES
THAT ACL2 MAY BE UNSOUND WHEN BUILT ON THAT LISP! If however you believe
that your Lisp properly supports IEEE floating-point operations even though
that feature is missing (e.g., quite possibly with older versions of CCL), you
can avoid that build-time error by setting environment variable
ACL2_FP_OK to any non-empty string. You might want to do that in a
script that invokes your Lisp.
