AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
https://aeneasverif.github.io/charon/charon_lib/index.html
Apache License 2.0
103 stars 17 forks source link

Cache `Name` computation #310

Closed Nadrieril closed 3 months ago

Nadrieril commented 3 months ago

We compute names a lot (e.g. every time we translate a type, to check if it refers to a built-in). This makes a significant difference in debug mode (~30% speedup when running make generate-ml), not so much when charon is compiled in release mode.

sonmarcho commented 3 months ago

Oh wow, I hadn't realized it was that expensive :scream: