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.make | |
| 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.make')
| -rw-r--r-- | Makefile.make | 2 |
1 files changed, 1 insertions, 1 deletions
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 |