Jean-Christophe Léchenet

> Btw, there is something to be checked about RISC-V, related to the linearization_params. The code was copied from arm, and it should work. But if I'm not mistaken, there...

> I also have to rebase on branch risc-v, and to undo the commit adding ra to the callee_saved registers (even if that could make sense, ra contains the return...

Indeed, stack alloc assumes that every function argument is a variable, and badly fails otherwise. During typing, we reject most programs where it is not the case (`r = f(42)`...

In general, do you think that we should remove everything not strictly related to typing from pretyping and put it in that pass?

Note that there is a file testing this feature, namely `tests/success/pointers/x86-64/test_spill_loop.jazz` and it does not need the trick of using a subarray, but I think it is because of the...

``` compilation error: register allocation: conflicting variables “pstate.12972” and “a.9970” must be merged due to: ... ```

Before the call to `greedy_allocation`, there are multiple `collect_conflict` functions (opn, intra-procedural, return address, inter-procedural, syscalls). If it fails in one of these functions, the liveness info is not printed.

opam strikes back. You used a feature (symmetry of disequality) that is not available before Coq 8.18 (cf. https://github.com/coq/coq/pull/17025), and opam tests 8.16. The stupid fix is to call a...

Other issues with `#copy`: - we cannot use subarrays in general (`#copy(a[0:1])` does not assert false, but fail nonetheless) - we cannot choose between for and while loops (is this...

I guess there will be a release with the deprecated interface? Or was it decided that it was simpler to just remove it?