coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-23	Normalize evars during bytecode compilation (fix #13841).	Guillaume Melquiond
	Otherwise, the interpreter sees already unified evars as accumulators rather than actual constants, thus preventing the computations from progressing. This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed evar normalization. The effect went unnoticed because the computed term is still convertible to the reduced term, except that it is the lazy machinery that ends up reducing it, rather than the bytecode one. So, performances became abysmal, seemingly at random.
2020-10-21	Same little game with Projection.	Pierre-Marie Pédrot

2020-10-08	Remove occurrences of Parray.reroot.	Guillaume Melquiond

2020-09-22	Modify bytecode representation of closures to please OCaml's GC (fix #12636).	Guillaume Melquiond
	The second field of a closure can no longer be the value of the first free variable (or another closure of a mutually recursive block) but must be an offset to the first free variable. This commit makes the bytecode compiler and interpreter agnostic to the actual representation of closures. To do so, the execution environment (variable coq_env) no longer points to the currently executed closure but to the last one. This has the following consequences: - OFFSETCLOSURE(n) now always loads the n-th closure of a recursive block (counted from last to first); - ENVACC(n) now always loads the value of the n-th free variable. These two changes make the bytecode compiler simpler, since it no longer has to track the relative position of closures and free variables. The last change makes the interpreter a bit slower, since it has to adjust coq_env when executing GRABREC. Hopefully, cache locality will make the overhead negligible.
2020-08-18	Rename VM-related kernel/cfoo files to kernel/vmfoo	Gaëtan Gilbert