diff options
| author | Pierre Roux | 2019-04-04 00:14:47 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:03 +0100 |
| commit | dca0135a263717b3a1a1d7c4f054f039dc08109e (patch) | |
| tree | 3f2ab5ea79e084a9c72e1376d5399ad4a62cb771 /Makefile.build | |
| parent | 3e0db1b645a8653c62b8b5a4978e6d8fbbe9a9cc (diff) | |
Make primitive float work on x86_32
Flag -fexcess-precision=standard is not enough on x86_32
where -msse2 -mfpmath=sse is required (-msse is not enough)
to avoid double rounding issues in the VM.
Most floating-point operation are now implemented in C because OCaml
is suffering double rounding issues on x86_32 with 80 bits extended
precision registers used for floating-point values, causing double
rounding making floating-point arithmetic incorrect with respect to
its specification.
Add a runtime test for double roundings.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index f9286c9635..90b3408d79 100644 --- a/Makefile.build +++ b/Makefile.build @@ -568,13 +568,13 @@ $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE) VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo kernel/float64.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo -bin/votour: $(call bestobj, $(VOTOURCMO)) +bin/votour: $(call bestobj, $(VOTOURCMO)) $(LIBCOQRUN) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I checker) + $(HIDE)$(call bestocaml, -I checker -cclib -lcoqrun) $(VMBYTEFLAGS) -bin/votour.byte: $(VOTOURCMO) +bin/votour.byte: $(VOTOURCMO) $(LIBCOQRUN) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(call ocamlbyte, -I checker) + $(HIDE)$(call ocamlbyte, -I checker -cclib -lcoqrun) $(VMBYTEFLAGS) ########################################################################### # Csdp to micromega special targets |