Track timely Config changes #295
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR tracks changes to timely's
Configuration
type, which is nowConfig
and handles a broader class of options than before. In particular, it houses user-defined configurations, which we are attempting with this PR. Rather than specifyDIFFERENTIAL_EAGER_MERGE
in the environment, a user can add anisize
value with keydifferential/idle_merge_effort
toworker.config()
which is then read out by the worker at arrangement construction time. This is a similar idiom to user-specific logging channels, which seems to have worked well enough.The main downside here is that it was super casual to just screw around with your environment. Now, interested programs must solicit this value somehow, and explicitly set it as part of the configuration. That is more work (and in particular isn't magically done for existing DD programs). This is I suppose the downside of DD not having an execution prelude in the same way that timely has the
execute
method.cc: @benesch, @ryzhyk