Greetings! I just thought I'd post on the resolution of this old
thread.
In summary, GCL 2.7.0 chose option 1) as previously described, namely
NaNs are floats and do not trigger errors unless trapping is explicitly
set. For posterity, option 2) was unworkable as if NaNs were not floats
and not numbers, one could not get them to traverse the typecases
correctly when one wished to disable the error.
(/= x x) and the like will be optimized away if and only if the compiler
can determine the value is not a NaN, see below. This is identical
behavior for gcc.
I had to rework the type system a bit to accommodate unordered floats. In
sum, (or (long-float 0) (long-float * 0)) is a subtype of, but not equal
to, long-float. As NaNs were not envisioned in the spec (apparently),
I've taken the liberty of defining (long-float si::unordered) to refer
to the and of the latter and the not of the former. The interested soul
can experiment with NaNs in types passed to 'si::resolve-type to their
heart's content to see how this works out.
This was the last obstacle for GCL 2.7.0 release. AFAICS GCL master
supports current master of ACL2, maxima, axiom, fricas, and hol88 and is
ready for release. If anyone has any extremely minor suggestions in the
next week or so please send them my way. No unicode changes made it
into this release.
If anyone has access to gcc-15, it would be helpful if they could
confirm that GCL master builds with -std=gnu17 passed to CFLAGS. I do
not yet have access to this compiler for testing, but it is coming and it would
be
great if GCL worked out of the box.
Separately there are some improvements to the maxima build procedure
available via the new function si::do-recomp to avoid recompiling the
whole tree twice. I will try to commit a patch soon.
Take care,
=============================================================================
(disassemble '(lambda (x y) (declare ((float 0 ) x y)) (/= x x)))
;; Compiling /tmp/gazonk_890403_0.lsp.
;; When compiling (DEFUN CMP-ANON)
INTERNAL-SIMPLE-STYLE-WARNING: The variable Y is not used.
;; End of Pass 1.
;; End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
;; Finished compiling /tmp/gazonk_890403_0.o.
#include "gazonk_890403_0.h"
void init_code(){do_init((void *)VV);}
/* local entry for function COMPILER::CMP-ANON */
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
{ VMB1 VMS1 VMV1
{object V5 = Cnil;
VMR1(V5);}
}
(1 (MAPC 'EVAL *COMPILER-COMPILE-DATA*))
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
;
#define VMB1
#define VMS1
#define VMV1
#define VMRV1(a_,b_) return((object )a_);
#define VMR1(a_) VMRV1(a_,0);
#define VM1 0
static void * VVi[1]={
#define Cdata VV[0]
(void *)(LI1__CMP_ANON___gazonk_890403_0)
};
#define VV (VVi)
NIL
COMPILER>(disassemble '(lambda (x y) (declare ((float ) x y)) (/= x x)))
;; Compiling /tmp/gazonk_890403_0.lsp.
;; When compiling (DEFUN CMP-ANON)
INTERNAL-SIMPLE-STYLE-WARNING: The variable Y is not used.
;; End of Pass 1.
;; End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
;; Finished compiling /tmp/gazonk_890403_0.o.
#include "gazonk_890403_0.h"
void init_code(){do_init((void *)VV);}
/* local entry for function COMPILER::CMP-ANON */
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
{ VMB1 VMS1 VMV1
{object V5 = (immnum_ne((V3),(V3))?Ct:Cnil);
VMR1(V5);}
}
(1 (MAPC 'EVAL *COMPILER-COMPILE-DATA*))
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
;
#define VMB1
#define VMS1
#define VMV1
#define VMRV1(a_,b_) return((object )a_);
#define VMR1(a_) VMRV1(a_,0);
#define VM1 0
static void * VVi[1]={
#define Cdata VV[0]
(void *)(LI1__CMP_ANON___gazonk_890403_0)
};
#define VV (VVi)
NIL
COMPILER>(disassemble '(lambda (x y) (declare ((short-float ) x y)) (/= x x)))
;; Compiling /tmp/gazonk_890403_0.lsp.
;; When compiling (DEFUN CMP-ANON)
INTERNAL-SIMPLE-STYLE-WARNING: The variable Y is not used.
;; End of Pass 1.
;; End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
;; Finished compiling /tmp/gazonk_890403_0.o.
#include "gazonk_890403_0.h"
void init_code(){do_init((void *)VV);}
/* local entry for function COMPILER::CMP-ANON */
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
{ VMB1 VMS1 VMV1
{object V5 = ((sf(V3))!=(sf(V3))?Ct:Cnil);
VMR1(V5);}
}
(1 (MAPC 'EVAL *COMPILER-COMPILE-DATA*))
static object LI1__CMP_ANON___gazonk_890403_0(object V3,object V4)
;
#define VMB1
#define VMS1
#define VMV1
#define VMRV1(a_,b_) return((object )a_);
#define VMR1(a_) VMRV1(a_,0);
#define VM1 0
static void * VVi[1]={
#define Cdata VV[0]
(void *)(LI1__CMP_ANON___gazonk_890403_0)
};
#define VV (VVi)
NIL
COMPILER>=============================================================================
Camm Maguire <c...@maguirefamily.org> writes:
> Greetings!
>
> Matt Kaufmann <kaufm...@cs.utexas.edu> writes:
>
>> Hi Camm,
>>
>> Excellent. ACL2 will evaluate the following at start-up.
>>
>> (fpe:break-on-floating-point-exceptions
>> :floating-point-overflow t
>> :division-by-zero t ; not sure this is actually needed
>> :floating-point-invalid-operation t)
>>
>
> Sounds good, but you might want to consider adding the other two with a
> setting of nil so your behavior is immune to GCL changes in its default
> configuration. I don't plan on enabling traps by default at the moment
> as it appears controversial, but that could change.
>
>
>> That said, consider the following from the Common Lisp Hyperspec,
>> Section 12.1.4.4 (Rule of Float Precision Contagion).
>>
>> The result of a numerical function is a float of the largest format
>> among all the floating-point arguments to the function.
>>
>> This seems to argue for proposal 1), since when a NaN results from the
>> application of a numerical function to double-float arguments, that
>> NaN would apparently need to be of type double-float.
>
> Yeah, I think 1) is the way to go for now, but the reading of this
> section depends to my mind on whether NaN is a valid return, in which
> case it is a number/float/long-float, or an error indicator, which can
> be trapped or not. Conceptually you might as well replace the NaN with
> a common-lisp condition akin to
>
>
>>(arithmetic-error-operands (make-condition 'floating-point-invalid-operation
>>:operands (list compiler::nan 1.0)))
>
> (#<nan> 1.0)
>
> and return this when not trapping, but defining some additional cell
> containing the NaN result for use in subsequent processing. The chief
> argument against this appears to be performance.
>
> Take care,
--
Camm Maguire c...@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
