aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|
* Merge PR #6800: [checker] Printer cleanup.Gravatar Maxime Dénès2018-03-09
|\
* | Update checker to reflect rule on constructors of polymorphic inductive typesGravatar Matthieu Sozeau2018-03-08
| |
| * [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
|/ | | | Makes printing rules more explicit and should close #6799.
* Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
|
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \
* \ \ Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ | | | | | | | | | | | | constraints.
* \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ \ | | | | | | | | | | | | | | | camlp4
| * | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | * | | Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |/ / / |/| | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
| | * | Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
| |/ / |/| |
* | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \
| | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| | |/
* | / Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 |= *)
| * [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
|/ | | | | | | | | | The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
* checker: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| | | | This just shares the unfold_projection between Closure and Reduction.
* checker: remove unused per-constant reduction flags.Gravatar Gaëtan Gilbert2018-02-02
|
* [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
| | | | Fixes #5747: "make validate" fails with "bad recursive trees"
* [checker] Remove duplicated functionGravatar Maxime Dénès2018-01-25
|
* [checker] Better error message for bad recursive treesGravatar Maxime Dénès2018-01-25
|
* fix space in coqchk errorGravatar Ralf Jung2018-01-24
|
* Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code.
* Actually use the strategy information in the checker.Gravatar Pierre-Marie Pédrot2018-01-14
|
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
* Add interfaces for checker and remove dead code.Gravatar Maxime Dénès2018-01-10
|
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
| | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\
* \ Merge PR #6303: Remove redundant Zcase from the checker.Gravatar Maxime Dénès2017-12-07
|\ \
* \ \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \ \
| | * | Remove redundant Zcase from the checker.Gravatar Pierre-Marie Pédrot2017-12-02
| |/ / |/| | | | | | | | | | | | | | This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now.
| | * Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
| | |
| | * Forbid implicitly relative names in the checker.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name.
| | * Mark the -I option in coqchk as deprecated and merge it with -Q.Gravatar Pierre-Marie Pédrot2017-11-29
| | | | | | | | | | | | | | | | | | It is not doing the same thing as coqtop, and the corresponding coqtop semantics is irrelevant in the checker as the latter does not rely on ML code.
| | * Add a -Q option to coqchck.Gravatar Pierre-Marie Pédrot2017-11-29
| |/ |/| | | | | | | | | It has exactly the same effect as -R, because there is no such thing as implicit relativization for object files in coqchk, contrarily to what Require does in coqtop.
* | Allow to pass physical files to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| |
* | Adding an interface file for checker/check.ml.Gravatar Pierre-Marie Pédrot2017-11-28
| |
| * Use safe demarshalling in the checker.Gravatar Pierre-Marie Pédrot2017-11-28
| | | | | | | | | | | | Instead of relying on the OCaml demarshaller, which is not resilient against ill-formed data, we reuse the safe demarshaller from votour. This ensures that garbage files do not trigger memory violations.
| * Use large arrays in the checker demarshaller.Gravatar Pierre-Marie Pédrot2017-11-28
|/ | | | | This allows to work around the size limitation of vanilla OCaml arrays on 32-bit platforms, which is rather easy to hit.
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
| | | | | | | | | | | | | | | | Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
* | Truncate strings in votour to 1024 characters.Gravatar Pierre-Marie Pédrot2017-11-23
| | | | | | | | | | Making it bigger is kind of useless, takes time and clutters the output for no real advantage.
* | Bypass int and string representation in votour when it's incorrect.Gravatar Pierre-Marie Pédrot2017-11-23
| |
* | Tail-recursive list traversal in votour.Gravatar Pierre-Marie Pédrot2017-11-23
| |
* | Implement a tail-recursive traversal of the object in votour.Gravatar Pierre-Marie Pédrot2017-11-22
|/
* Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Gravatar Maxime Dénès2017-11-13
|\
| * [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | This will allow to merge back `Names` with `API.Names`