From 6fe8c44ff828ef4ec89b49ada634ce87639f384f Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 6 Oct 2020 16:52:03 +0200
Subject: 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.
---
 Makefile.build | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index eed3c2813a..526a8c5831 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -400,6 +400,12 @@ $(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_m
 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)
 ###########################################################################
-- 
cgit v1.2.3