From 5ced750ab679bcbc244a3b9304607760a7bfa9e8 Mon Sep 17 00:00:00 2001
From: Palina <polina.tolmach@gmail.com>
Date: Thu, 10 Oct 2024 18:49:25 +0800
Subject: [PATCH] TOML: use `default` profile values by default when another
 profile is active (#4657)

Follow up to https://github.com/runtimeverification/kontrol/pull/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
https://github.com/runtimeverification/kontrol/pull/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                        |  4 +++-
 .../tests/unit/test-data/pyk_toml_test.toml   |  5 ++++-
 pyk/src/tests/unit/test_toml_args.py          | 22 +++++++++++++++++++
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py
index f4a50ce32a9..077f18358a4 100644
--- a/pyk/src/pyk/cli/pyk.py
+++ b/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] = {}
diff --git a/pyk/src/tests/unit/test-data/pyk_toml_test.toml b/pyk/src/tests/unit/test-data/pyk_toml_test.toml
index 9919e16f378..a374fe73737 100644
--- a/pyk/src/tests/unit/test-data/pyk_toml_test.toml
+++ b/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"
\ No newline at end of file
diff --git a/pyk/src/tests/unit/test_toml_args.py b/pyk/src/tests/unit/test_toml_args.py
index 8f3db569e69..455e838eed3 100644
--- a/pyk/src/tests/unit/test_toml_args.py
+++ b/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()