Skip to content

Adding arguments to kprove flags#3648

Merged
rv-jenkins merged 4 commits intodevelopfrom
improve-kprove-help-flag-descriptors
Sep 15, 2023
Merged

Adding arguments to kprove flags#3648
rv-jenkins merged 4 commits intodevelopfrom
improve-kprove-help-flag-descriptors

Conversation

@Robertorosmaninho
Copy link
Copy Markdown
Collaborator

@Robertorosmaninho Robertorosmaninho commented Sep 15, 2023

Follow up of #3619, #3638, and #3642!

This PR enhances the usability of kprove --help and kprove --help-hidden by providing flag descriptors to help the user understand when an argument needs to be provided to the flag.

Ex.:

Before

Usage: kprove [options] <file>
  Options:
    --branching-allowed
      Number of branching events allowed before a forcible stop.
      Default: 2147483647

Now:

Usage: kprove [options] <file>
  Options:
    --branching-allowed <value>
      Number of branching events allowed before a forcible stop.
      Default: 2147483647

Among others, this PR introduces the following arguments to the respective parameters:

parameter argument
--branching-allowed <number>
--claims <labels>
--color <mode>
--debug-script <file>
--default-claim-type <type>
--definition <path>
--depth <number>
--emit-json-spec <file>
--exclude <labels>
--output, -o <mode>
--output-file <file>
--output-flatten <KLabels>
--output-omit <KLabels>
--output-tokast <KLabels>
--output-tokenize <KLabels>
--spec-module, -sm <name>
--trusted <labels>
--haskell-backend-command <command>
--haskell-backend-home <directory>
--smt-timeout <milliseconds>

@Robertorosmaninho Robertorosmaninho self-assigned this Sep 15, 2023
@rv-jenkins rv-jenkins changed the base branch from master to develop September 15, 2023 15:58
Copy link
Copy Markdown
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few suggestions.
Ping me again when you answered all of them and tests passed.

Comment thread kernel/src/main/java/org/kframework/kprove/KProveOptions.java
Comment thread kernel/src/main/java/org/kframework/kprove/KProveOptions.java
Comment thread kernel/src/main/java/org/kframework/kprove/KProveOptions.java
Comment thread kernel/src/main/java/org/kframework/utils/options/SMTOptions.java Outdated
@Robertorosmaninho
Copy link
Copy Markdown
Collaborator Author

@radumereuta, I've implemented your comments! However, I would appreciate a new round on the comment I didn't mark resolved!

Comment thread kernel/src/main/java/org/kframework/kprove/KProveOptions.java
@Robertorosmaninho Robertorosmaninho marked this pull request as ready for review September 15, 2023 16:42
Copy link
Copy Markdown
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

@rv-jenkins rv-jenkins merged commit fe59236 into develop Sep 15, 2023
@rv-jenkins rv-jenkins deleted the improve-kprove-help-flag-descriptors branch September 15, 2023 17:24
@Baltoli Baltoli mentioned this pull request Dec 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants