| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
Fixes #6699
|
|
Protect accu and coq_env against GC calls in the VM when calling
primitive integer functions on 32 bits architecture.
|
|
This serves two purposes:
1. It makes the native compiler use the same encoding and
lambda-representation as the bytecode compiler
2. It avoid relying on fragile invariants relating tags and constructor
indices. For example, previously, the mapping from indices to tags
had to be increasing.
|
|
|
|
|
|
|
|
This is a step towards unifying the higher level ILs of the native and
bytecode compilers.
See https://github.com/coq/coq/projects/17
|
|
This function seems unused.
|
|
Since e1e7888, stuck projections were not computed correctly.
Fixes #9684
|
|
skip_pattern
Reviewed-by: ppedrot
|
|
This is convenient for the bootstrap of `coqdep`
|
|
proj
Ack-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
applications
Reviewed-by: SkySkimmer
|
|
This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
This takes advantage of the mutability of the fconstr relevance mark.
|
|
|
|
Prevent errors when under annotating binders.
|
|
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
|
|
|
|
This operation is done directly in Safe_typing.register_inline and has
nothing to do with retroknowledge afaict.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
|
|
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
|
|
|
|
|
|
The strategy is to backtrack when a constant is in head
position: we first try to see if the arguments are guarded,
if not we unfold.
Since `Case` is represented as a head (rather than as a context
as the reduction machine does) we did not backtrack there
and reduce (including delta) the scrutinized in order to
fire the iota redex.
This commit adds a choice point in that specific case, and
reduces eagerly (not step by step) the scrutinized in case
of failure.
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
records
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
