Gabriel Scherer

@garrigue I think that you are talking about something slightly different. In the current code, for a pattern of the form `K((p1|p2|p3), q)`, we only use the "dependent mode" where...

> This is still tricky because dependencies can appear both by the sharing of type parameters, and through type arguments that contain already some sharing. I am not sure I...

Here is maybe an idea to check `K(p, q)`, with the goal to avoid a product combination when there is no dependency between the arguments. - when we type-check GADTs,...

I wonder about the performance impact of the more-expensive OCaml-C boundary. If there is an easy way to run Sandmark benchmarks on a arm64 machine, it would be interesting to...

If the branch after load is for ordering with future stores to the same location, we may be able to avoid it for immutable locations? This is probably harder than...

We don't need to have the exact same notion of immutability as the optimizer needs, only to propagate information that assigns one or the other scheme to each memory operation,...

Nice! It is surprisingly easy to implement this optimization. Could you maybe update the original comment, which gives a very nice overview of the design (thanks!), to also distinguish mutable...

I think it would still be interesting to look at the results of the run for the first version, if you have them. This can give an understanding of the...

What we can read on these pictures is that there is a small code-size increase as you reported, that programs that are dominated by writes can benefit greatly (but there...

I have a non-expert question about the hybrid C/OCaml scenario: > The problematic case is the mix of C and OCaml. Consider the case when there is a non-atomic load...