coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-26	Signed primitive integers	Ana
	Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal.
2021-01-10	Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.	Guillaume Melquiond

2020-12-02	Make sure the msb is clear.	Guillaume Melquiond
	This is presumably not usable from the surface language. But an ML module could easily create a proof of false by passing a negative number to Const.mkInt.
2020-12-02	Greatly simplify the conversion functions between Z.t and Uint63.t.	Guillaume Melquiond

2020-12-01	Make the code clearer and faster by calling mask63 explicitly at the end.	Guillaume Melquiond
	Before this commit, function mask63 was called implicitly at each step.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-12-27	Add critical-bugs entry, tests-suite file, and code comment.	Guillaume Melquiond

2019-12-22	Use a more straightforward algorithm for mulc on 32-bit architectures. ↵	Guillaume Melquiond
	(Fixes #11321) It has the added advantage of performing 6 less 64-bit operations per long multiplication.
2019-12-22	Simplify equality of 63-bit integers.	Guillaume Melquiond
	The sign bit is supposed to be zero, so no need to mask it out. If it was not zero, most of the algorithms in this file would fail horribly.
2019-12-22	Do not hide constants from the compiler.	Guillaume Melquiond

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	Make primitive float work on x86_32	Pierre 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-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
	Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency.
2019-08-24	Simplify picking between uint63_63.ml and uint63_31.ml	Gaëtan Gilbert
	- remove the architecture component (we don't do anything arch-specific so it was just a rewording of int_size) - have configure tell the make build system about int_size instead of reimplementing cp As a bonus, add the copyright header to uint63.mli.