Skip to content

Change the --extractTarget option into a command#5799

Merged
keyboardDrummer merged 2 commits into
dafny-lang:masterfrom
keyboardDrummer:touchup
Sep 30, 2024
Merged

Change the --extractTarget option into a command#5799
keyboardDrummer merged 2 commits into
dafny-lang:masterfrom
keyboardDrummer:touchup

Conversation

@keyboardDrummer

@keyboardDrummer keyboardDrummer commented Sep 30, 2024 •
edited
Loading

Copy link
Copy Markdown
Member

Touchup PR for #5621

Description

  • Change the --extractTarget option into a hidden command
  • Make --help work when used on hidden commandds

How has this been tested?

  • Manually ran make extract in DafnyCore. This feature needs some tests but I'm leaving that out of scope of this PR.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) September 30, 2024 10:56
atomb
atomb reviewed Sep 30, 2024
View reviewed changes

@atomb atomb left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

@keyboardDrummer

keyboardDrummer commented Sep 30, 2024

Copy link
Copy Markdown
Member Author

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

It's a hidden command, so I think we're free to change the name/options later without having to be backwards compatible.

@atomb

atomb commented Sep 30, 2024

Copy link
Copy Markdown
Member

I'm somewhat leaning toward making the command name or an argument more specific. What about either dafny extract-boogie file.bpl file.dfy or extract --language boogie file.bpl file.dfy with the latter case anticipating the potential for extraction to other languages, as well. What do the two of you think?

It's a hidden command, so I think we're free to change the name/options later without having to be backwards compatible.

Good point. Given that, I'm happy with this.

@keyboardDrummer keyboardDrummer merged commit 0b44740 into dafny-lang:master Sep 30, 2024
@keyboardDrummer keyboardDrummer deleted the touchup branch September 30, 2024 20:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@atomb atomb atomb approved these changes

@RustanLeino RustanLeino Awaiting requested review from RustanLeino

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@keyboardDrummer @atomb