TOML: use default profile values by default when another profile is…

… active (#4657)

Follow up to runtimeverification/kontrol#825.

In Foundry, when parsing TOML config files, values set in a default
profile (e.g., `[prove.default]` in `kontrol.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](https://book.getfoundry.sh/config/)). We'd like
to support the same behavior in `kontrol.toml`.

Similarly to a change made in
runtimeverification/kontrol#825 to the
`foundry.toml` parsing, this PR enforces reading the values set in both
active and `default` profiles and using the default ones for values that
are not set in the active profile. This PR also adds a
`test_prove_legacy_profiles` test that ensures that both `default` and
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 in `get_profile`
that would enable this behavior only if the function is called by
Kontrol?

pyk/src/pyk/cli/pyk.py

@@ -579,7 +579,9 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s
         if len(profile_list) == 0 or profile_list[0] not in toml_profile:
             return {k: v for k, v in toml_profile.items() if type(v) is not dict}
         elif len(profile_list) == 1:
-            return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict}
+            active_profile = {k: v for k, v in toml_profile.get(profile_list[0], {}).items() if type(v) is not dict}
+            default_profile = {k: v for k, v in toml_profile.get('default', {}).items() if type(v) is not dict}
+            return {**default_profile, **active_profile}
         return get_profile(toml_profile[profile_list[0]], profile_list[1:])
 
     toml_args: dict[str, Any] = {}

pyk/src/tests/unit/test-data/pyk_toml_test.toml

@@ -6,9 +6,12 @@ definition = "/tmp"
 input = "kast-json"
 no-minimize = true
 
-[prove-legacy]
+[prove-legacy.default]
 kArgs = ["arg 1","args 2"]
 
+[prove-legacy.verbose]
+verbose = true
+
 [coverage.a_profile]
 verbose = true
 output = "a-profile-file"

pyk/src/tests/unit/test_toml_args.py

@@ -62,6 +62,28 @@ def test_prove_legacy_kargs() -> None:
     assert len(args_dict['k_args']) == 2
 
 
+def test_prove_legacy_profiles() -> None:
+    parser = create_argument_parser()
+    cmd_args = [
+        'prove-legacy',
+        '--config-file',
+        str(TEST_TOML),
+        '--config-profile',
+        'verbose',
+        tempfile.gettempdir(),
+        str(TEST_TOML),
+        str(TEST_TOML),
+        'spec-module',
+        'cmd_args',
+    ]
+    args = parser.parse_args(cmd_args)
+    args_dict = parse_toml_args(args)
+    assert len(args_dict['k_args']) == 2
+    assert hasattr(args, 'verbose')
+    assert 'verbose' in args_dict
+    assert args_dict['verbose']
+
+
 def test_toml_read() -> None:
     change_in_toml('definition = "(.*)"', f'definition = "{tempfile.gettempdir()}"')
     parser = create_argument_parser()