Skip to content

Commit 6ca1a65

Browse files
Fix parsing lemmas-related build options in kontrol.toml (#1009)
* Map lemmas-related `kontrol build` options to parameters names * Test `require` and `module-import` reading from `kontrol.toml`
1 parent 69e12db commit 6ca1a65

File tree

3 files changed

+14
-0
lines changed

3 files changed

+14
-0
lines changed

src/kontrol/options.py

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -846,6 +846,10 @@ def from_option_string() -> dict[str, str]:
846846
| KOptions.from_option_string()
847847
| KompileOptions.from_option_string()
848848
| KompileTargetOptions.from_option_string()
849+
| {
850+
'require': 'requires',
851+
'module-import': 'imports',
852+
}
849853
)
850854

851855
@staticmethod
@@ -856,6 +860,10 @@ def get_argument_type() -> dict[str, Callable]:
856860
| KOptions.get_argument_type()
857861
| KompileOptions.get_argument_type()
858862
| KompileTargetOptions.get_argument_type()
863+
| {
864+
'require': list_of(str),
865+
'module-import': list_of(str),
866+
}
859867
)
860868

861869
def __str__(self) -> str:

src/tests/unit/test-data/kontrol_test.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ foundry-project-root = '.'
77
verbose = false
88
debug = false
99
optimization-level = 3
10+
require = 'xor-lemmas.k'
11+
module-import = 'TestBase:XOR-LEMMAS'
1012

1113
[prove.b_profile]
1214
verbose = true

src/tests/unit/test_toml_args.py

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,10 @@ def test_toml_specific_options() -> None:
8282
args_dict = parse_toml_args(args, get_option_string_destination, get_argument_type_setter)
8383
assert 'o3' in args_dict
8484
assert args_dict['o3']
85+
assert 'requires' in args_dict
86+
assert args_dict['requires'] == ['xor-lemmas.k']
87+
assert 'imports' in args_dict
88+
assert args_dict['imports'] == ['TestBase:XOR-LEMMAS']
8589

8690

8791
def test_toml_profiles() -> None:

0 commit comments

Comments
 (0)