coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-12-02	Put all Int63 primitives in a separate file	Pierre Roux
	Following a request from Pierre-Marie Pédrot in #13258
2020-08-09	Bring Float notations in line with stdlib	Jason Gross
	This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
2020-06-08	Fix 12483	Pierre Roux

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-26	Consolidate int63-related notations	Maxime Dénès
	We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2019-11-01	Fix ldshiftexp	Pierre 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-01	docs: Add refman+stdlib documentation	Erik Martin-Dorel

2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik 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-01	Pretty-printing primitive float constants	Erik 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-01	Parsing primitive float constants	Pierre Roux

2019-11-01	Add next_{up,down} primitive float functions	Pierre Roux

2019-11-01	Implement classify on primitive float	Pierre Roux

2019-11-01	Change return type of primitive float comparison	Pierre 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-01	Put axioms on ldshiftexp and frshiftexp	Guillaume 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-01	Add Floats to standard library	Guillaume Bertholon
	All supported floating point operations are defined on specification floats. Then we register the primitive type and functions, and add conversion functions to and from the specification type. Finally we put axioms to state that primitive operations behave exactly the same as specification operations. CREDITS: Most of the code inside SpecFloat is adapted from the Flocq library. NOTE: For the moment this code will not compile if native compilation is enabled in the configuration phase. This will be resolved later when native_compute will be supported by primitive floats. So please use option "-native-compiler no" in ./configure currently.