diff options
| author | Pierre Roux | 2020-10-06 16:52:03 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-10-06 18:26:38 +0200 |
| commit | 6fe8c44ff828ef4ec89b49ada634ce87639f384f (patch) | |
| tree | 43642a3c3fb5bdb5817afea42cd608c527b7044c /Makefile.build | |
| parent | 6d3a9220204de22e0b81dc961d2eb269128b5c2e (diff) | |
Use OCaml floating-point operations on 64 bits arch
C functions were used for floating-point arithmetic operations, by
fear of double rounding that could happen on old x87 on 32 bits
architecture. This commit uses OCaml floating-point operations on 64
bits architectures.
The following snippet is made 17% faster by this commit.
From Coq Require Import Int63 BinPos PrimFloat.
Definition foo n :=
let eps := sub (next_up one) one in
Pos.iter (fun x => add x eps) two n.
Time Eval native_compute in foo 1000000000.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index eed3c2813a..526a8c5831 100644 --- a/Makefile.build +++ b/Makefile.build @@ -401,6 +401,12 @@ kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml rm -f $@ && cp $< $@ && chmod a-w $@ ########################################################################### +# Specific rules for Float64 +########################################################################### +kernel/float64.ml: kernel/float64_$(OCAML_INT_SIZE).ml + rm -f $@ && cp $< $@ && chmod a-w $@ + +########################################################################### # Main targets (coqtop.opt, coqtop.byte) ########################################################################### |