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

Inconsistent style across :set option names #656

Closed
brianhuffman opened this issue Oct 28, 2019 · 1 comment · Fixed by #1073
Closed

Inconsistent style across :set option names #656

brianhuffman opened this issue Oct 28, 2019 · 1 comment · Fixed by #1073
Assignees
Labels
command-line-repl Related to Cryptol's text-based UI
Milestone

Comments

@brianhuffman
Copy link
Contributor

Here are the names of all the settable options in the Cryptol REPL, as shown by tab completion:

Cryptol> :set
ascii            debug            prover           satNum           tc-debug         warnDefaulting
base             infLength        prover-stats     show-examples    tc-solver        warnShadowing
core-lint        mono-binds       prover-validate  smtfile          tests

Some are hyphenated, and some use camelCase. We should choose a single convention and use it consistently.

@yav yav added the command-line-repl Related to Cryptol's text-based UI label Jan 21, 2020
@robdockins
Copy link
Contributor

This has bothered me several times now since this ticket was filed.

I suggest we choose a convention and switch to it for the release following 2.10. In addition, let's allow settings to be changed by the old names for at least one release (and issue a warning that the old names are deprecated), but not show the alternate names in documentation, etc.

I suggest we go with camel case, as it fits more nicely with idiomatic cryptol naming, as - is not a valid identifier character.

@robdockins robdockins added this to the 2.11.0 milestone Jan 15, 2021
@robdockins robdockins self-assigned this Feb 10, 2021
robdockins added a commit that referenced this issue Feb 11, 2021
Options are now all named in camelCase style.  However, multiword
options may still be set using the old hypenated names as aliases,
so interaction scripts and the test suite do not have to be
changed. In addition, option lookup is altered to be case insensitive.

Thus, the canonical option name for the output SMT file when
an offline prover is selected is `smtFile`, which is what will
show up when running `:set` with no arguments, and what will be
suggested for tab-completion.  However, the option may be set
using the strings `smtfile` `SMTFile`, `smt-file`, `SMT-file`, etc.

Fixes #656
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
command-line-repl Related to Cryptol's text-based UI
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants