Xavier Leroy
Xavier Leroy
ocamljava fails with "Error: Cannot compile goto_table_4081 (Java method is too long: 94429 bytes)" The function in question is generated by Menhir into Coq, then extracted into OCaml, so I...
When running the test https://github.com/ocaml/ocaml/blob/trunk/testsuite/tests/tool-ocamlopt-save-ir/start_from_emit.ml , a temporary asm file /tmp/camlasmXXXX.s is not removed. This is a mild problem for CI machines (where /tmp gets cluttered by temp files eventually),...
`Declare Scope` makes it possible to declare a new notation scope before adding notations to it. This construct has been available since Coq 8.12, and is recommended, to the point...
By popular demand. The tail call optimization pass performed later in CompCert will not turn a call into a tail call if the function has stack-allocated data, because this might...
Allocate the initializing float block statically and outside the heap, rather than dynamically at first use. Not only it's more efficient, but it also avoids the race condition reported in...
When run in "memory cleanup at exit" mode (`OCAMLRUNPARAM=c=1`), the current trunk exhibits memory leaks: ``` Direct leak of 6840 byte(s) in 1 object(s) allocated from: #0 0x4a12fd in malloc...
This is a follow-up to ed89275cb. With the Clang/LLVM linker and loader, "const" variables initialized with symbol addresses which may need relocation cannot go in a readonly section and must...
Some packages for CamlIDL include findlib support, sometimes with issues: https://caml.inria.fr/mantis/view.php?id=7125 . Consider adding findlib support to the master sources.
As reported in #35, some of the C files in this library (e.g. src/poly1305-donna.c) are also present in other libraries, causing name collisions for the functions they export. This commit...
Many of our tests use the `ocamlrunparam` directive to specify OCaml runtime parameters such as `b=1` (to get backtraces) or `l=100000` (to reduce the max stack size) or `s=512` (to...