coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-08-18	Rename VM-related kernel/cfoo files to kernel/vmfoo	Gaëtan Gilbert

2020-07-06	Primitive persistent arrays	Maxime Dénès
	Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-01	UIP in SProp	Gaëtan Gilbert

2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
	This corresponds more naturally to the use we make of them, as we don't need fast indexation but we instead keep pushing terms on top of them.
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-03-14	Add relevance marks on binders.	Gaëtan Gilbert
	Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
	Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-02-04	Primitive integers	Maxime Dénès
	This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2018-10-15	Correct some spelling errors	Benjamin Barenblat
	Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
2018-09-24	[kernel] Compile with almost all warnings enabled.	Emilio Jesus Gallego Arias
	This is a partial resurrection of #6423 but only for the kernel. IMHO, we pay a bit of price for this but it is a good safety measure. Only warning "4: fragile pattern matching" and "44: open hides a type" are disabled. We would like to enable 44 for sure once we do some alias cleanup.
2018-09-19	Merge PR #8447: Cleaning in the retroknowledge	Pierre-Marie Pédrot

2018-09-17	OCaml now exports the min and max non-constant tags, let's use it	Maxime Dénès

2018-09-17	[VM] Allocate a bit less in digits_from_uint	Maxime Dénès

2018-09-17	[VM] Inject structured constants in values without reallocating them.	Maxime Dénès

2018-09-17	[VM] Move structured_constant to Vmvalues	Maxime Dénès

2018-09-14	Retroknowledge: use GlobRef.t instead of Constr.t as entry	Vincent Laporte

2018-08-20	Do not inline let-bound functions in clambda optimization.	Pierre-Marie Pédrot
	This was triggering an exponential blowup in the size of the generated intermediate VM code. Fixes #8277.
2018-07-24	VM: don't duplicate projection narg information in lproj/kproj	Gaëtan Gilbert

2018-07-24	Projections use index representation	Gaëtan Gilbert
	The upper layers still need a mapping constant -> projection, which is provided by Recordops.
2018-06-28	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert
	It's a bit shorter and more direct.
2018-05-31	Reduce circular dependency constants <-> projections	Gaëtan Gilbert
	Instead of having the projection data in the constant data we have it independently in the environment.
2018-05-28	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès
	We eta-expand cofixpoints when needed, so that their call-by-need evaluation is correctly implemented by VM and native_compute.
2018-05-28	Unify pre_env and env	Maxime Dénès
	We now have only two notions of environments in the kernel: env and safe_env.
2018-05-23	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin

2018-04-02	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias
	Recent commits introduced global flags, but these should be module-specific so relocating. Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced to the truly global stuff.
2018-03-03	Handling evars in the VM.	Pierre-Marie Pédrot
	We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659.
2018-02-23	New IR in VM: Clambda.	Maxime Dénès
	This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.