| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-20 | Merge PR #6908: Move VM global tables from C to ML | Maxime Dénès | |
| 2018-04-12 | Merge PR #6972: [api] Deprecate a couple of aliases that we missed. | Maxime Dénès | |
| 2018-04-09 | Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation | Pierre-Marie Pédrot | |
| 2018-04-06 | Fix #6956: Uncaught exception in bytecode compilation | Maxime Dénès | |
| We also make the code of [compact] in kernel/univ.ml a bit clearer. | |||
| 2018-03-28 | [api] Deprecate a couple of aliases that we missed. | Emilio Jesus Gallego Arias | |
| 2018-03-27 | Expliciting and taking advantage of a representation invariant in Esubst. | Pierre-Marie Pédrot | |
| 2018-03-26 | More efficient reallocation of VM global tables. | Pierre-Marie Pédrot | |
| The previous code was mimicking what the C implementation was doing, which was a quadratic algorithm. We simply use the good old exponential reallocation strategy that is amortized O(1). | |||
| 2018-03-26 | Moving the VM global atom table to a ML reference. | Pierre-Marie Pédrot | |
| 2018-03-26 | Moving the VM global data to a ML reference. | Pierre-Marie Pédrot | |
| 2018-03-09 | Fix expected number of arguments for cumulative constructors. | Gaëtan Gilbert | |
| We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works). | |||
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6769: Split closure cache and remove whd_both | Maxime Dénès | |
| 2018-03-09 | Cumulativity: improve treatment of irrelevant universes. | Gaëtan Gilbert | |
| In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit. | |||
| 2018-03-09 | Allow using cumulativity without forcing strict constraints. | Gaëtan Gilbert | |
| Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible. | |||
| 2018-03-09 | Merge PR #6747: Relax conversion of constructors according to the pCuIC model | Maxime Dénès | |
| 2018-03-09 | Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values | Maxime Dénès | |
| 2018-03-08 | Fix SR breakage due to allowing fixpoints on non-rec values | Matthieu Sozeau | |
| We limit fixpoints to Finite inductive types, so that BiFinite inductives (non-recursive records) are excluded from fixpoint construction. This is a regression in the sense that e.g. fixpoints on unit records were allowed before. Primitive records with eta-conversion are included in the BiFinite types. Fix deprecation Fix error message, the inductive type needs to be recursive for fix to work | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |