Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make proof function prefix configurable #270

Open
palinatolmach opened this issue Jan 12, 2024 · 0 comments
Open

Make proof function prefix configurable #270

palinatolmach opened this issue Jan 12, 2024 · 0 comments
Labels
enhancement New feature or request

Comments

@palinatolmach
Copy link
Collaborator

palinatolmach commented Jan 12, 2024

Originally posted by @tothtamas28 in #249 (comment)

The logic for deciding what sort of KCFG to construct based on the function name (e.g., starting with test, prove, etc.) should be pulled up from the _method_to_cfg function, and is_test and failing should become parameters.

Halmos allows specifying the function name using the following argument, and we can do the same thing, introducing, e.g., --function and --fail-function as the first step:

    parser.add_argument(
        "--function",
        metavar="FUNCTION_NAME_PREFIX",
        default="check_",
        help="run tests matching the given prefix. Shortcut for `--match-test '^{PREFIX}'`. (default: '%(default)s')",
    )

On the other hand, as also noted by @tothtamas28, proof name prefix is not something that's likely to change between kontrol prove calls so we may not want to expose it on the CLI.

As a better alternative, proof_prefixes is the sort of thing that should be configurable through a configuration file. If it doesn't break Foundry we can consider adding a section to foundry.toml (e.g., [kontrol] or [symbolic]), which won't break Foundry but will throw a warning:

warning: Found unknown config section in foundry.toml: [kontrol]
This notation for profiles has been deprecated and may result in the profile not being registered in future versions.
Please use [profile.kontrol] instead or run `forge config --fix`.

Otherwise, maybe its time to introduce kontrol.toml. This would enable cleaning up the CLI a bit as well. We have this issue on our roadmap for February, but it can also be picked up earlier if we have the bandwidth.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants