TOML: use default profile values by default when another profile is active
#4657
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
palinatolmach
force-pushed
the
always-use-default-toml-profile
branch
from
ef3f58f
to
1dab690
Compare
palinatolmach
force-pushed
the
always-use-default-toml-profile
branch
from
1dab690
to
0b0189c
Compare
anvacaru
approved these changes
Oct 9, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Follow up to runtimeverification/kontrol#825.
In Foundry, when parsing TOML config files, values set in a default profile (e.g.,
[prove.default]inkontrol.toml) are inherited by other profiles unless they are explicitly overridden in those profiles, which helps avoid redefining shared configuration settings between profiles (Foundry docs). We'd like to support the same behavior inkontrol.toml.Similarly to a change made in runtimeverification/kontrol#825 to the
foundry.tomlparsing, this PR enforces reading the values set in both active anddefaultprofiles and using the default ones for values that are not set in the active profile. This PR also adds atest_prove_legacy_profilestest that ensures that bothdefaultand active profile's values are used.I do realise, however, that this behavior (other profiles inheriting from
default) is non-standard, so I'd appreciate any feedback on this PR. Maybe it'd be better if I added another parameter inget_profilethat would enable this behavior only if the function is called by Kontrol?