Change the --extractTarget option into a command

dafny-lang / dafny

Dafny is a verification-aware programming language

https://dafny.org

Other

2.94k stars 263 forks source link

Change the --extractTarget option into a command #5799

Closed keyboardDrummer closed 2 months ago

keyboardDrummer commented 2 months ago

Touchup PR for https://github.com/dafny-lang/dafny/pull/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 commented 2 months ago

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 commented 2 months ago

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.