| Age | Commit message (Collapse) | Author |
|---|
|
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
* Fix the implementations and add tests
* Change shift from int63 to Z (was always used as a Z)
* Update FloatLemmas.v accordingly
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
|
|
* Add a related test-suite in compare.v (generated by a bash script)
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
|
|
|
|
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.
|
|
* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function
Namely:
let to_string_raw f = Printf.sprintf "%.17g" f
let to_string f = if is_nan f then "nan" else to_string_raw f
Summary:
* printing a binary64 float in 17 decimal places and parsing it again
will yield the same float, e.g.:
let f1 = 1. +. (0x1p-53 +. 0x1p-105)
let f2 = float_of_string (to_string f1)
f1 = f2
* OCaml's string_of_float gives a sign to nan values which shouldn't be
displayed as all NaNs are considered equal here.
|
|
|
|
Tests are updated to include native computations.
|
|
|
|
|
|
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
|
|
Tests are updated to include VM computations and check for double
rounding.
|
|
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.
Also move primitive integer tests to place all primitive tests in the
same directory.
|
|
Ack-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: ppedrot
|
|
Noticed by coverage, test code by Gäetan Gilbert.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
|
|
Close #4502
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
|
|
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
|
|
We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.
|
|
|
|
extensionality
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
|
|
|
|
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
the Ltac-substituted environment
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
dune-compiled Coq
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
More precisely: The equivalent in #7288 (4dab4fc) to the former call
to ltac_interp_name_env was not done anymore when interpreting
uconstr's.
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This lets the checker verify that we didn't produce nonsense.
|
|
Reviewed-by: herbelin
|
|
|
|
This is the dual of #10344.
|
|
Fixes #9428. (Again.)
This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.
(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
AFAICT there is no reason to use interp_open_constr
I used Evd.from_ctx to keep passing evar maps around but maybe we
should be passing ustates instead?
|
|
i.e. you can do
~~~
make -f Makefile.dune world
make -C test-suite success
~~~
to make just the success tests, then modify Coq sources and retest
just the ones you want
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82
|
