Skip to content

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented Aug 13, 2025

I want to measure this across more files, but here's the improvement on the repro from #3800.

Before:

Stats:
                   key     calls      tree     point       exn
             norm_term   1471862  43374 ms  43374 ms      0 ms
           tc_one_file         8  60415 ms   8859 ms      0 ms
             norm_comp         4   8179 ms   8179 ms      0 ms
    Parser.Dep.collect         1      4 ms      3 ms      0 ms
                 parse         2      1 ms      1 ms      0 ms
           simplify_vc      1290  33070 ms      0 ms      0 ms
         desugar_decls         1      0 ms      0 ms      0 ms
      deep_compress_se        15      0 ms      0 ms      0 ms
      hash_dependences         7      0 ms      0 ms      0 ms
ramon: group.total          60.918s
ramon: group.mempeak        10874MiB

After:

Stats:
                   key     calls      tree     point       exn
             norm_term   1471862  38437 ms  38437 ms      0 ms
           tc_one_file         8  54074 ms   9224 ms      0 ms
             norm_comp         4   6410 ms   6410 ms      0 ms
    Parser.Dep.collect         1      5 ms      4 ms      0 ms
                 parse         2      1 ms      1 ms      0 ms
           simplify_vc      1290  27164 ms      0 ms      0 ms
         desugar_decls         1      0 ms      0 ms      0 ms
      deep_compress_se        15      0 ms      0 ms      0 ms
      hash_dependences         7      0 ms      0 ms      0 ms
ramon: group.total          54.406s
ramon: group.mempeak        6880MiB

So reducing RAM usage by 1/3.

https://github.com/mtzguido/FStar/actions/runs/16949854112

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant