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.

Sign up for GitHub

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

Jump to bottom

Improving kompile's --help and --help-hidden messages using descriptors #3638

Merged
merged 5 commits into from
Sep 14, 2023
Merged

Improving kompile's --help and --help-hidden messages using descriptors #3638

merged 5 commits into from
Sep 14, 2023

Conversation

Robertorosmaninho
Copy link
Collaborator

Fixes #3619

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

Ex.:

Before

kompile --help
Usage: kompile [options] <file>
  Options:
    --backend
      Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates 
      the kompiled K definition.
      Default: llvm

Now:

kompile --help
Usage: kompile [options] <file>
  Options:
    --backend <backend>
      Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates 
      the kompiled K definition.
      Default: llvm

@Robertorosmaninho Robertorosmaninho self-assigned this Sep 13, 2023
@rv-jenkins rv-jenkins changed the base branch from master to develop September 13, 2023 19:53
radumereuta
radumereuta approved these changes Sep 13, 2023
View reviewed changes
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.

Looking nice!

radumereuta
radumereuta reviewed Sep 13, 2023
View reviewed changes
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.

Ah, there are more options for kprove and kast. Did you check those as well?

@Robertorosmaninho Robertorosmaninho marked this pull request as ready for review September 14, 2023 16:53
@Robertorosmaninho
Copy link
Collaborator Author

I'll implement these changes in kast and kprove in future PRs!

@rv-jenkins rv-jenkins merged commit 3534894 into develop Sep 14, 2023
@rv-jenkins rv-jenkins deleted the improve-kompile-help-flag-descriptors branch September 14, 2023 18:04
@Robertorosmaninho Robertorosmaninho mentioned this pull request Sep 14, 2023
Merged
rv-jenkins pushed a commit that referenced this pull request Sep 14, 2023
@Robertorosmaninho
Adding arguments to kast flags (#3642)
a042195 
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:
<!DOCTYPE html>

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 mentioned this pull request Sep 15, 2023
Merged
rv-jenkins pushed a commit that referenced this pull request Sep 15, 2023
@Robertorosmaninho
Adding arguments to kprove flags (#3648)
fe59236 
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>
@radumereuta radumereuta mentioned this pull request Oct 23, 2023
Closed
5 tasks
@Baltoli Baltoli mentioned this pull request Dec 12, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@radumereuta radumereuta radumereuta approved these changes

@dwightguth dwightguth Awaiting requested review from dwightguth

Assignees

@Robertorosmaninho Robertorosmaninho

Labels
automerge frontend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[K-Bug] Missing file argument in kompile's flag
3 participants
@Robertorosmaninho @radumereuta @rv-jenkins