| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.
|
|
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
Reviewed-by: maximedenes
|
|
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
|
|
|
|
|
|
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
specification
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
|
|
There are three implementations of this primitive:
* one in OCaml on 63 bits integer in kernel/uint63_amd64.ml
* one in OCaml on Int64 in kernel/uint63_x86.ml
* one in C on unsigned 64 bit integers in kernel/byterun/coq_uint63_native.h
Its specification is the axiom `diveucl_21_spec` in
theories/Numbers/Cyclic/Int63/Int63.v
* comment the implementations with loop invariants to enable an easy
pen&paper proof of correctness (note to reviewers: the one in
uint63_amd64.ml might be the easiest to read)
* make sure the three implementations are equivalent
* fix the specification in Int63.v
(only the lowest part of the result is actually returned)
* make a little optimisation in div21 enabled by the proof of correctness
(cmp is computed at the end of the first loop rather than at the beginning,
potentially saving one loop iteration while remaining correct)
* update the proofs in Int63.v and Cyclic63.v to take into account the
new specifiation of div21
* add a test
|
|
|
|
Reviewed-by: ppedrot
|
|
Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
|
|
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.
|
|
|
