| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-08 | Relax conversion of constructors according to the pCuIC model | Matthieu Sozeau | |
| - Nothing to check in conversion as they have a common supertype by typing. - In inference, enforce that one is lower than the other. | |||
| 2018-03-05 | Add empty description for @raise statements to satisfy ocamldoc | mrmr1993 | |
| 2018-03-05 | Replace invalid tag @raises in ocamldoc comments with @raise | mrmr1993 | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-03-04 | Merge PR #935: Handling evars in the VM | Maxime Dénès | |
| 2018-03-04 | Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort | Maxime Dénès | |
| 2018-03-04 | Remove whd_both from the kernel. | Pierre-Marie Pédrot | |
| Now that the cache is distinct, there should be no nasty side-effects changing the value of one side while reducing the other. | |||
| 2018-03-04 | Pass the constant cache as a separate argument in kernel reduction. | Pierre-Marie Pédrot | |
| 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-03-02 | [VM] Unify Const_sorts and Const_type, and remove Vsort. | Maxime Dénès | |
| This simplifies the representation of values, and brings it closer to the ones of the native compiler. | |||
| 2018-03-01 | Fix #6878: univ undefined for [with Definition] bad instance size. | Gaëtan Gilbert | |
| 2018-02-28 | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd) | Maxime Dénès | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-24 | Merge PR #6784: New IR in VM: Clambda | Maxime Dénès | |
| 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. | |||
| 2018-02-23 | Fix map iterator on nativelambda. | Maxime Dénès | |
| 2018-02-21 | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | Maxime Dénès | |
| 2018-02-19 | Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵ | Maxime Dénès | |
| constraints. | |||
| 2018-02-16 | Extrude monomorphic universe contexts from with Definition constraints. | Pierre-Marie Pédrot | |
| We defer the computation of the universe quantification to the upper layer, outside of the kernel. | |||
| 2018-02-15 | Adding a sanity check on inductive variance subtyping. | Pierre-Marie Pédrot | |
| 2018-02-14 | Factorize the relocations in the on-disk VM representation. | Pierre-Marie Pédrot | |
| Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to. | |||
| 2018-02-14 | Use a more compact representation for bytecode relocations stored on disk. | Pierre-Marie Pédrot | |
| The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice. | |||
| 2018-02-14 | Do not use global variables for VM bytecode compilation in Cemitcodes. | Pierre-Marie Pédrot | |
| Instead we thread a buffer. | |||
| 2018-02-14 | Remove the unsafe bytes conversion function in Cemitcodes. | Pierre-Marie Pédrot | |
| This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way. | |||
| 2018-02-14 | Move the call to the computation of bytecode inside Cemitcodes. | Pierre-Marie Pédrot | |
| This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode. | |||
| 2018-02-14 | Abstract further the type of VM bytecode compilation. | Pierre-Marie Pédrot | |
| This reduces the possibility to wreak havoc while making the API nicer. | |||
| 2018-02-14 | Merge PR #6713: Fix #6677: Critical bug with VM and universes | Maxime Dénès | |
| 2018-02-13 | Merge PR #6702: [vernac] [minor] Move print effects to top-level caller. | Maxime Dénès | |
| 2018-02-12 | Merge PR #1082: Fixing Print for inductive types with let-in in parameters | Maxime Dénès | |
| 2018-02-12 | Merge PR #6128: Simplification: cumulativity information is variance ↵ | Maxime Dénès | |
| information. | |||
| 2018-02-12 | Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6674: Delay computation of lifts in the reduction machine. | Maxime Dénès | |
| 2018-02-12 | Fix #6677: Critical bug with VM and universes | Maxime Dénès | |
| This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism. | |||
| 2018-02-11 | Universe instance printer: add optional variance argument. | Gaëtan Gilbert | |
| 2018-02-11 | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert | |
| This ensures by construction that we never infer constraints outside the variance model. | |||
| 2018-02-11 | dest_{prod,lam}: no Cast case (it's removed by whd) | Gaëtan Gilbert | |
| 2018-02-10 | Simplification: cumulativity information is variance information. | Gaëtan Gilbert | |
| Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *) | |||
| 2018-02-10 | [get_cumulativity_constraints] allowing further code sharing. | Gaëtan Gilbert | |
| 2018-02-10 | Factorize code for comparing maybe-cumulative inductives. | Gaëtan Gilbert | |
| The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it. | |||
| 2018-02-10 | Fix typo in Univ.CumulativityInfo | Gaëtan Gilbert | |
| 2018-02-09 | [nit] Remove some unnecessary global `open Feedback` | Emilio Jesus Gallego Arias | |
| 2018-02-09 | [nativecomp] Remove ad-hoc handling of Dynlink exception. | Emilio Jesus Gallego Arias | |
| Instead, we properly register a printer for such exception and update the code. | |||
| 2018-02-07 | Merge PR #6685: Use whd-all on rigid-flex conversion. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | |
| 2018-02-05 | Respect the transparent state of the current conversion on strong weak-head. | Pierre-Marie Pédrot | |
| This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state. | |||
| 2018-02-05 | [native_compute] Fix handling of evars in conversion | Maxime Dénès | |
| 2018-02-05 | [native_compute] Remove useless conversion to list in reification. | Maxime Dénès | |
| 2018-02-04 | Delay computation of lifts in the reduction machine. | Pierre-Marie Pédrot | |
| This definitely qualifies as a micro-optimization, but it would not be performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml semantics, as it involves a fixpoint and changes potential non-termination. In our case it doesn't matter semantically, but it is indeed observable on computation intensive developments like UniMath. | |||
| 2018-02-02 | CClosure.unfold_projection: don't catch Not_found, assume env is ok | Gaëtan Gilbert | |
| We can do this after the parent commit (Reductionops.nf_* don't use empty env) | |||
| 2018-02-02 | kernel: cleanup projection unfolding | Gaëtan Gilbert | |
| - use Redflags.red_projection - share unfold_projection between CClosure and Reduction | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |