We do not have a small reproducer, but deep updates in F* are causing a memory blow up.
Two of these patterns are:
a.coefficients[i] += 3a[i][j] += 3
These are translated into nested updates (which is correct) but chaining two such updates already uses up gigabytes of memory when typechecking with F* and adding more updates cases OOM errors in F*.
We do not have a small reproducer, but deep updates in F* are causing a memory blow up.
Two of these patterns are:
a.coefficients[i] += 3a[i][j] += 3These are translated into nested updates (which is correct) but chaining two such updates already uses up gigabytes of memory when typechecking with F* and adding more updates cases OOM errors in F*.