| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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 |= *)
|
| |/
|
|
|
|
|
|
|
|
| |
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].
|
| |
|
|
| |
This just shares the unfold_projection between Closure and Reduction.
|
| | |
|
| |
|
|
| |
Fixes #5747: "make validate" fails with "bad recursive trees"
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
| |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/
|/|
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
| |
This allows to work around the size limitation of vanilla OCaml arrays on
32-bit platforms, which is rather easy to hit.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
Making it bigger is kind of useless, takes time and clutters the output for
no real advantage.
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| | |
This will allow to merge back `Names` with `API.Names`
|
| |/
|
|
|
| |
This is useful for tools such as `coqchk` or `coq_makefile` that want
to handle feedback on their own.
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This fixes longstanding bug likely introduced in the first `pp` to
`Feedback` migration, namely the checker didn't register a feedback
printer, thus no calls to `Feedback.msg_*` were printed in the
checker.
This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587
We fix this by adding a custom printer to the checker, this is correct
as the checker owns now the full console, however a cleanup should
happen in any of these two directions:
- all the calls to feedback are removed, and the checker always uses
its own printing mechanism.
- all the calls to `Format/Printf` are removed and the checker always
uses the `Feedback` mechanism.
Currently, I have no opinion on this.
|
| |/
|
|
|
|
|
|
|
|
|
| |
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
| |\ |
|
| | |
| |
| |
| |
| | |
This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
|
| | | |
|
| |/
|
|
|
|
|
|
| |
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| |
|
|
|
|
|
|
|
|
|
| |
It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.
This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.
|
| |
|
|
|
| |
This is the followup of the previous commit, this time implementing the
correct algorithm in the checker.
|
Maxime Dénès
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Ralf Jung
Pierre-Marie Pédrot
Matej Košík