-
Notifications
You must be signed in to change notification settings - Fork 40
Open
Labels
engineIssue in the engineIssue in the enginef*F* backendF* backendworkaroundThis bug has a workaroundThis bug has a workaround
Description
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*.
Metadata
Metadata
Assignees
Labels
engineIssue in the engineIssue in the enginef*F* backendF* backendworkaroundThis bug has a workaroundThis bug has a workaround