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 /kernel/dune | |
| 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 'kernel/dune')
| -rw-r--r-- | kernel/dune | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/dune b/kernel/dune index ce6fdc03df..bd663974da 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63)) (libraries lib byterun dynlink)) (executable @@ -19,6 +19,11 @@ (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) +(rule + (targets float64.ml) + (deps (:gen-file float64_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) + (documentation (package coq)) |