aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-08-11 18:31:32 +0200
committerPierre-Marie Pédrot2020-08-14 10:00:41 +0200
commitbbed52c1104acfef4f897570e9cb6ba8bf42870a (patch)
treea9c55fb77033f1603ab1fa6fba54df14301b4688 /dev/include
parentca47fb67a95cf291a43a68b210b9670d4461e9d6 (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 'dev/include')
0 files changed, 0 insertions, 0 deletions