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.make | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.make')

diff --git a/Makefile.make b/Makefile.make
index 51d6d1c3c1..34f5707ae8 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
 GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?
 
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml
 GENMLIFILES:=$(GRAMMLIFILES)
 GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
-- 
cgit v1.2.3