diff options
| author | Pierre-Marie Pédrot | 2020-08-11 18:31:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-14 10:00:41 +0200 |
| commit | bbed52c1104acfef4f897570e9cb6ba8bf42870a (patch) | |
| tree | a9c55fb77033f1603ab1fa6fba54df14301b4688 /kernel/cemitcodes.ml | |
| parent | ca47fb67a95cf291a43a68b210b9670d4461e9d6 (diff) | |
Do not precompute hint dnets eagerly.
Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.
The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.
A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions
