Xavier Leroy
Xavier Leroy
Thanks for the report. You're right that `align_blockcopy` is inconsistent with the reduced alignments for int64 and double of the IA32 ABI. In old versions of CompCert, int64 and double...
However, the "Initial state undefined" error is unrelated to `align_blockcopy` and is due to `Memdata.align_chunk` returning 8 for 64-bit integers. There was a reason for this choice, and the incompatibility...
It turns out that the CompCert memory model requires 64-bit integer accesses to be 8-aligned, otherwise they could not be reliably turned into two 32-bit integer accesses (see e.g. `Memory.load_int64_split`)....
See #557 for a tentative implementation of IBT.
I'm late on the next release of CompCert and #557 is not as ready to be merged as I would like. As a temporary measure, I added `-z nobtcfi` to...
> Would it be enoough to express the number of cores the test needs, for instance? Normally, parallel tests should adapt to the number of cores available, see https://github.com/ocaml/ocaml/blob/trunk/testsuite/HACKING.adoc#dimensioning-the-tests ....
A `make parallel` that executes the sequential tests in parallel using GNU `parallel` and the parallel tests in sequence would be a great improvement already.
The Caml Consortium special licensing scheme is still there, and is the main reason why the Consortium still exists. However, we'd prefer industrial users of OCaml to join the Foundation...
It would be considerate to discuss this proposal. I'm of two minds: on the one hand, OCaml has pairs but also triples, quadruples, etc, and it feels odd to favor...
Cherry-picked to 5.3. @Octachron I'l let you decide whether to backport this one to 5.2.