aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-01Merge PR #11028: Update the deprecation doc of `Shrink Obligations`Clément Pit-Claudel
2019-11-01Merge PR #10647: Expose universe processing in comInductive.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-11-01Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵Enrico Tassi
relation Reviewed-by: gares
2019-11-01Update the deprecation doc of `Shrink Obligations`Jason Gross
Now it uses `.. deprecated` like all the other deprecation notices in the manual.
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-11-01Merge PR #8642: Compiled interfaces with -vos and -vok optionsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-11-01Merge PR #11019: enforcing Ltac2 constructor name are uppercasedPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-01adding test file for Uppercase Ltac2 constructorsKenji Maillard
2019-11-01enforcing Ltac2 cosntructors name are uppercase in open typesKenji Maillard
2019-11-01Add warnings regarding the experimental nature of the vos feature in the doc.Pierre-Marie Pédrot
2019-11-01Teach coq_dune about the empty .vos produced by coqcGaëtan Gilbert
Without this the next dune command after build a vo will wipe out the vos, breaking interactive users. Also this means dune installs the .vos files.
2019-11-01[test-suite] acknowledge coq_mafile installs .vosEnrico Tassi
2019-11-01[make] install .vos along with .voEnrico Tassi
2019-11-01fix installation of vos files in coq Makefilecharguer
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall ↵charguer
that the generation of a .vo files induces the creation of an empty .vos file.)
2019-11-01fix coq_makefile and doc for vos support.charguer
2019-11-01Changelog entryMaxime Dénès
2019-11-01additional details in the doc for -voscharguer
2019-11-01Implementing support for vos/vok files.charguer
A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file.
2019-11-01Merge PR #11015: [Nix] Update reference to nixpkgsThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-01docs(gallina-extensions.rst): Say more on float literals extractionErik Martin-Dorel
2019-11-01Communicate CFLAGS to dunePierre Roux
2019-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
(as suggested by @silene)
2019-11-01Makefile.build: Fix rules of bin/votour{,.byte}Erik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Add a check for gradual underflowsPierre Roux
2019-11-01Add the IEEE-754 arch requirement in INSTALLPierre Roux
Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
2019-11-01feat: Use SSE2_MATH if available & Die if missing on x87Erik Martin-Dorel
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Fix ldshiftexpPierre Roux
* 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>
2019-11-01Add overlaysPierre Roux
2019-11-01docs: Add entry in changelogErik Martin-Dorel
2019-11-01docs: Add refman+stdlib documentationErik Martin-Dorel
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
* Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Reimplement is_floatPierre Roux
is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this.
2019-11-01Make primitive float work on x86_32Pierre Roux
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.
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
* 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.
2019-11-01Parsing primitive float constantsPierre Roux
2019-11-01Add primitive floats to checkerPierre Roux
2019-11-01Add tests for primitive floats with 'native_compute'Pierre Roux
Tests are updated to include native computations.
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
* Float added to is_value/get_value to avoid stack overflows (cf. #7646) * beware of the use of Array.map with floats (cf. comment in the makeblock function) NB: From here one, the configure option "-native-compiler no" is no longer needed.
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
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.
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas. The shift value has been increased to 2 * emax + prec because in ldexp we want to be able to transform the smallest denormalized to the biggest float value in one call.
2019-11-01Add tests for primitive floats with 'vm_compute'Guillaume Bertholon
Tests are updated to include VM computations and check for double rounding.
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
* This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM.
2019-11-01Add tests for primitive floatsGuillaume Bertholon
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 00:08:54 +0000