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

Expand "Compiler Args" to "Compiler Arguments" #219

Open
RustanLeino opened this issue Jul 21, 2022 · 3 comments · May be fixed by #509
Open

Expand "Compiler Args" to "Compiler Arguments" #219

RustanLeino opened this issue Jul 21, 2022 · 3 comments · May be fixed by #509
Labels
enhancement New feature or request

Comments

@RustanLeino
Copy link
Contributor

One of the Dafny settings in the IDE is called "Compiler Args". I think the "Args" is an unnecessary abbreviation that is better spelled out as "Arguments".

Also, it says compiler arguments. The explanatory text also mentions the compiler, but it could be nice if the message would say something along the lines of "These arguments are used when you ask to compile your code. These settings are not used by the background verifier." For example, I wasn't sure if perhaps "compiler" referred to the entire tool, so I had tried to use /functionSyntax:4. I then discovered this does not work. But then it would be nice to know if or how I could add options to the verifier. Even saying "(Sorry, there's no way to give arbitrary options to the verifier.)" would be nice, I think.
@MikaelMayer MikaelMayer added the enhancement New feature or request label Jul 25, 2022
@MikaelMayer
Copy link
Member

For the second part, we split the arguments into two, one for running and one for the background verifier. That means you can have --function-syntax:4 for both now !

For the first part, although I agree it would be an improvement, renaming the option would be disrupting for users who were already relying on it. But perhaps it's fine. If @keyboardDrummer agrees with the renaming, then I can perform it.

@keyboardDrummer
Copy link
Member

I'm wholly convinced by the presented Arguments.

@RustanLeino
Copy link
Contributor Author

I just looked at this again. I no longer see the "Compiler Args", but I see

  • Dafny: Language Server Launch Args
  • Dafny: Run Args

It would be nice to expand "Args" in both of these cases. In fact, more text would be help, along the lines of "Arguments pass to Dafny when running the program".

@keyboardDrummer keyboardDrummer linked a pull request Nov 7, 2024 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Update option names keyboardDrummer/ide-vscode
3 participants
@keyboardDrummer @MikaelMayer @RustanLeino