aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Collapse)Author
2018-03-08Update checker to reflect rule on constructors of polymorphic inductive typesMatthieu Sozeau
2018-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
Makes printing rules more explicit and should close #6799.
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Maxime Dénès
constraints.
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Maxime Dénès
camlp4
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
longer use camlp4.
2018-02-16Extrude 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-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-11dest_{prod,lam}: no Cast case (it's removed by whd)Gaëtan Gilbert
2018-02-10Simplification: 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-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
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].
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
This just shares the unfold_projection between Closure and Reduction.
2018-02-02checker: remove unused per-constant reduction flags.Gaëtan Gilbert
2018-01-25[checker] Avoid relying on canonical names.Maxime Dénès
Fixes #5747: "make validate" fails with "bad recursive trees"
2018-01-25[checker] Remove duplicated functionMaxime Dénès
2018-01-25[checker] Better error message for bad recursive treesMaxime Dénès
2018-01-24fix space in coqchk errorRalf Jung
2018-01-20Fix #6618: coqchk fails with "ill-typed term".Pierre-Marie Pédrot
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.
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
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.
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-02Remove redundant Zcase from the checker.Pierre-Marie Pédrot
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.
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-11-29Forbid implicitly relative names in the checker.Pierre-Marie Pédrot
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.
2017-11-29Mark the -I option in coqchk as deprecated and merge it with -Q.Pierre-Marie Pédrot
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.
2017-11-29Add a -Q option to coqchck.Pierre-Marie Pédrot
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.
2017-11-29Allow to pass physical files to coqchk.Pierre-Marie Pédrot
2017-11-28Adding an interface file for checker/check.ml.Pierre-Marie Pédrot
2017-11-28Use safe demarshalling in the checker.Pierre-Marie Pédrot
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.
2017-11-28Use large arrays in the checker demarshaller.Pierre-Marie Pédrot
This allows to work around the size limitation of vanilla OCaml arrays on 32-bit platforms, which is rather easy to hit.
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
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.
2017-11-23Truncate strings in votour to 1024 characters.Pierre-Marie Pédrot
Making it bigger is kind of useless, takes time and clutters the output for no real advantage.
2017-11-23Bypass int and string representation in votour when it's incorrect.Pierre-Marie Pédrot
2017-11-23Tail-recursive list traversal in votour.Pierre-Marie Pédrot
2017-11-22Implement a tail-recursive traversal of the object in votour.Pierre-Marie Pédrot
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
This will allow to merge back `Names` with `API.Names`
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
This is useful for tools such as `coqchk` or `coq_makefile` that want to handle feedback on their own.
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 15:30:57 +0000