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

Adding arguments to kast flags #3642

Merged
merged 2 commits into from
Sep 14, 2023
Merged

Conversation

Robertorosmaninho
Copy link
Collaborator

Follow up of #3619 and #3638!

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

Ex.:

Before

kast --help
Usage: kast [options] <file>
  Options:
    --color
      Use colors in output. Default is on.
      Possible Values: [OFF, ON, EXTENDED]

Now:

Usage: kast [options] <file>
  Options:
    --color <mode>
      Use colors in output.
      Default: ON
      Possible Values: [OFF, ON, EXTENDED]

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

parameter argument
--color <mode>
--expression, -e <expression>
--input, -i <mode>
--module, -m <module>
--output, -o <mode>
--output-file <file>
--output-flatten <KLabels>
--output-omit <KLabels>
--output-tokast <KLabels>
--output-tokenize <KLabels>
--sort, -s <sort>
--steps <steps>
--definition <path>
--directory, -d <path>

@Robertorosmaninho Robertorosmaninho self-assigned this Sep 14, 2023
@rv-jenkins rv-jenkins changed the base branch from master to develop September 14, 2023 18:46
Copy link
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.

PR lgtm but there are some failing tests

private ColorSetting color;
@Parameter(names = "--color", description = "Use colors in output.", descriptionKey = "mode",
converter=ColorModeConverter.class)
private ColorSetting color = ColorSetting.ON;
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

That's funny, it seems that the error is from this modification. The help message says that the default is color=ON, but when I really implemented it, it raised the error on max-fail-spec.k

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Notice that the output also changed depending on --color ON and --color OFF:

With color:

  <T>
    <k>
      .
    </k>
    <state>
      a |-> A:Int
      b |-> B:Int
      max |-> B:Int
    </state>
  </T>
#And
  #Not ( {
      A
    #Equals
      B
    }
  #And
    {
      true
    #Equals
      B >=Int B
    } )
#And
  {
    true
  #Equals
    A <=Int B
  }

Without color:

  #Not ( {
      A
    #Equals
      B
    }
  #And
    {
      true
    #Equals
      B >=Int B
    } )
#And
  <T>
    <k>
      .
    </k>
    <state>
      a |-> A:Int
      b |-> B:Int
      max |-> B:Int
    </state>
  </T>
#And
  {
    true
  #Equals
    A

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've just filled an issue to track it: #3643

@rv-jenkins rv-jenkins merged commit a042195 into develop Sep 14, 2023
@rv-jenkins rv-jenkins deleted the improve-kast-help-flag-descriptors branch September 14, 2023 21:42
rv-jenkins pushed a commit that referenced this pull request 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>
@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