Skip to content

Deep updates in F* blows up memory. #1098

@karthikbhargavan

Description

@karthikbhargavan

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] += 3
  • a[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

No one assigned

    Labels

    engineIssue in the enginef*F* backendworkaroundThis bug has a workaround

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions