| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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>
|
|
|
|
The bytecode interpreter ensures that the stack space available at some
points is above a static threshold. However, arbitrary large stack space
can be needed between two check points, leading to segmentation faults
in some cases.
We track the use of stack space at compilation time and add
an instruction to ensure greater stack capacity when required. This is
inspired from OCaml's PR#339 and PR#7168.
Patch written with Benjamin Grégoire.
|
|
|
|
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
|
|
Apparently Cysmtable.set_global_boxed is unused,
and removing it allows to get rid of a bunch of C code
concerning "boxed" things (including ACCUMULATECOND
instruction).
Still TODO: Csymtable.set_transparent_const and
Csymtable.set_opaque_const appear to be no-ops.
Should we remove them ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* a small shell script ./build to drive ocamlbuild
* rules for all the binaries (apart from coqide and coqchk)
* use of ocamlbuild's Echo instead of using shell + sed + awk
for generated files
* Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
list of things to "clean"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Part contre ces cas sont detruis dans les "Definition"
(pas dans les "Lemma") je comprends pas ou ils sont enlev'e...
Si une id'ee ...
- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.
- Meilleur compilation des coinductifs, on utilise maintenant vraimment
du lazy.
- Enfin un peu plus de doc dans le code de la vm.
Benjamin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
